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)

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 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)

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