{o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
  (F : Functor C D) (ff : is-fully-faithful F)

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 ≑ β†’ from w ≑
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 ≑ β†’ 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 _