open import Cat.Functor.Base
open import Cat.Prelude hiding (injective)

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning

module
  Cat.Functor.Reasoning.FullyFaithful
  {o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
  (F : Functor C D) (ff : is-fully-faithful F)
  where

Reasoning for ff FunctorsπŸ”—

This module contains a few short combinators for reasoning about the actions of fully faithful functors on morphisms and isomorphisms.

from-id : w ≑ D.id β†’ from w ≑ C.id
from-id p = injectiveβ‚‚ (Ξ΅ _ βˆ™ p) F-id

from-∘ : from (w D.∘ x) ≑ from w C.∘ from x
from-∘ = injective (Ξ΅ _ βˆ™ sym (F-∘ _ _ βˆ™ apβ‚‚ D._∘_ (Ξ΅ _) (Ξ΅ _)))

ipushr : x D.∘ F₁ g ≑ xβ€² β†’ from (w D.∘ x) C.∘ g ≑ from (w D.∘ xβ€²)
ipushr p = injective (F-∘ _ _ Β·Β· apβ‚‚ D._∘_ (Ξ΅ _) refl Β·Β· D.pullr p βˆ™ sym (Ξ΅ _))

Ξ΅-lswizzle : w D.∘ x ≑ D.id β†’ w D.∘ F₁ (from (x D.∘ y)) ≑ y
Ξ΅-lswizzle = D.lswizzle (Ξ΅ _)

Ξ΅-expand : w D.∘ x ≑ y β†’ F₁ (from w C.∘ from x) ≑ y
Ξ΅-expand p = F-∘ _ _ Β·Β· apβ‚‚ D._∘_ (Ξ΅ _) (Ξ΅ _) Β·Β· p

Ξ΅-twist : F₁ f D.∘ x ≑ y D.∘ F₁ g β†’ f C.∘ from x ≑ from y C.∘ g
Ξ΅-twist {f = f} {g = g} p = injective $ swap $
  ap (F₁ f D.∘_) (Ξ΅ _) Β·Β· p Β·Β· ap (D._∘ F₁ g) (sym (Ξ΅ _))

inv∘l : x D.∘ F₁ f ≑ y β†’ from x C.∘ f ≑ from y
inv∘l x = sym (Ξ΅-twist (D.eliml F-id βˆ™ sym x)) βˆ™ C.idl _