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

invertible-equiv
  : ∀ {a b} {f : C.Hom a b}
  → C.is-invertible f ≃ D.is-invertible (F₁ f)
invertible-equiv {f = f} =
  prop-ext! F-map-invertible (is-ff→is-conservative F ff f)

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 invertible {a} {b} {f : C.Hom a b} =
  Equiv (invertible-equiv {f = f})

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

fromn't : w ≡ F₁ f → from w ≡ f
fromn't p = ap from p ∙ η _

from-id : (w ≡ D.id) ≃ (from w ≡ C.id)
from-id = ap-equiv ((F₁ , ff) e⁻¹) ∙e ∙-post-equiv (injective₂ (ε D.id) F-id)

to-id : (f ≡ C.id) ≃ (F₁ f ≡ D.id)
to-id = ap-equiv (F₁ , ff) ∙e id-equivr

module from-id {α} {w : D.Hom (F₀ α) (F₀ α)} = Equiv (from-id {w = w})
module to-id {a} {f : C.Hom a a} = Equiv (to-id {f = f})

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.to refl)

whackr : F₁ f D.∘ x ≡ F₁ g → f C.∘ from x ≡ g
whackr p = ε-twist (p ∙ sym (D.idl _)) ∙ C.eliml (from-id.to refl)

pouncer : F₁ f D.∘ x ≡ z → f C.∘ from x ≡ from z
pouncer p = ε-twist (p ∙ intror refl) ∙ C.idr _

η-expand : f C.∘ g ≡ h → from (F₁ f D.∘ F₁ g) ≡ h
η-expand p = from-∘ ∙∙ ap₂ C._∘_ (η _) (η _) ∙∙ p

η-twist : from x C.∘ f ≡ g C.∘ from y → x D.∘ F₁ f ≡ F₁ g D.∘ y
η-twist {x = x} {f = f} {g = g} {y = y} p =
 x D.∘ F₁ f                  ≡˘⟨ ε-expand refl      ⟩
 F₁ (from x C.∘ from (F₁ f)) ≡⟨  ⟨ C.refl⟩∘⟨ η _ ⟩  ⟩
 F₁ (from x C.∘ f)           ≡⟨  ⟨ p             ⟩  ⟩
 F₁ (g C.∘ from y)           ≡˘⟨ ⟨ η _ C.⟩∘⟨refl ⟩  ⟩
 F₁ (from (F₁ g) C.∘ from y) ≡⟨  ε-expand refl      ⟩
 F₁ g D.∘ y                  ∎

unwhackr : f C.∘ from w ≡ g → F₁ f D.∘ w ≡ F₁ g
unwhackr {f = f} {w = w} p = sym (η-twist $ C.idr _ ∙∙ η _ ∙∙ sym p) ∙ elimr refl

Lifting Shapes🔗

module _ {f : C.Hom b c} {g : C.Hom a b} {h : C.Hom a c} where

  triangle-equivl : (F₁ f D.∘ F₁ g ≡ F₁ h) ≃ (f C.∘ g ≡ h)
  triangle-equivl =
    F₁ f D.∘ F₁ g ≡ F₁ h
      ≃˘⟨ ∙-pre-equiv (sym (F-∘ f g)) ⟩
    F₁ (f C.∘ g) ≡ F₁ h
      ≃˘⟨ ap-equiv (F₁ , ff) ⟩
    f C.∘ g ≡ h ≃∎

  module triangle-equivl = Equiv triangle-equivl