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 _

whackl : x D.∘ F₁ f ≑ F₁ g β†’ from x C.∘ f ≑ g
whackl p = sym (Ξ΅-twist (D.idr _ βˆ™ sym p)) βˆ™ C.elimr (from-id refl)

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