open import Cat.Functor.Properties
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.

open Fr F public
private
module C = Cat.Reasoning C
module D = Cat.Reasoning D

private variable
a b c d : C.Ob
Ξ± Ξ² Ξ³ Ξ΄ : D.Ob
f g g' h i : C.Hom a b
w x x' y z : D.Hom Ξ± Ξ²

module _ {a} {b} where
open Equiv (Fβ {a} {b} , ff) public

iso-equiv : β {a b} β (a C.β b) β (Fβ a D.β Fβ b)
iso-equiv {a} {b} = (F-map-iso {x = a} {b} , is-ffβF-map-iso-is-equiv {F = F} ff)

module iso {a} {b} =
Equiv (F-map-iso {x = a} {b} , is-ffβF-map-iso-is-equiv {F = F} ff)

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 _