{-# OPTIONS --safe --lossy-unification #-}

module Cubical.Categories.Functor.ComposeProperty where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Functions.Embedding

open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation as Prop

open import Cubical.Categories.Category
open import Cubical.Categories.Isomorphism
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Equivalence
open import Cubical.Categories.Equivalence.WeakEquivalence

open import Cubical.Categories.Instances.Functors


open Category
open Functor
open NatTrans
open isIso
open isWeakEquivalence

-- Composition by functor with special properties

module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
  {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (E : Category ℓE ℓE')
  (F : Functor C D)
  where

  -- If F is essential surjective, (- ∘ F) is faithful.

  isEssSurj→isFaithfulPrecomp : isEssentiallySurj F → isFaithful (precomposeF E F)
  isEssSurj→isFaithfulPrecomp surj A B α β p =
    makeNatTransPath
      (λ i x → Prop.rec (E .isSetHom _ _)
      (λ (c , f) →
          ⋆InvLMove (F-Iso {F = A} f) (α .N-hom (f .fst))
        ∙ (λ i → F-Iso {F = A} f .snd .inv ⋆⟨ E ⟩ (p i .N-ob c ⋆⟨ E ⟩ B .F-hom (f .fst)))
        ∙ sym (⋆InvLMove (F-Iso {F = A} f) (β .N-hom (f .fst))))
      (surj x) i)


  -- If F is essential surjective and full, (- ∘ F) is full.

  isEssSurj+Full→isFullPrecomp : isEssentiallySurj F → isFull F → isFull (precomposeF E F)
  isEssSurj+Full→isFullPrecomp surj full A B α = ∣ ext , ext≡ ∣₁
    where
    Mor : (d : D .ob) → Type _
    Mor d =
      Σ[ g ∈ E [ A .F-ob d , B .F-ob d ] ]
        ((c : C .ob)(f : CatIso D (F .F-ob c) d)
        → α .N-ob c ≡ A .F-hom (f .fst) ⋆⟨ E ⟩ g ⋆⟨ E ⟩ B .F-hom (f .snd .inv))

    isPropMor : (d : D .ob) → isProp (Mor d)
    isPropMor d x y = Σ≡Prop (λ _ → isPropΠ2 (λ _ _ → E .isSetHom _ _)) path
      where
      path : x .fst ≡ y .fst
      path = Prop.rec (E .isSetHom _ _)
        (λ (c , f) →
          ⋆CancelL (F-Iso {F = A} f) (⋆CancelR (invIso (F-Iso {F = B} f))
            (sym (x .snd c f) ∙ y .snd c f)))
        (surj d)

    isContrMor : (d : D .ob) → isContr (Mor d)
    isContrMor d = inhProp→isContr inhab (isPropMor d)
      where
      inhab : Mor d
      inhab = Prop.rec (isPropMor d)
        (λ (a , h) →
          A .F-hom (h .snd .inv) ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ B .F-hom (h .fst) ,
          λ c f →
            Prop.rec (E .isSetHom _ _)
            (λ (k , p) →
              let isom-path = subst-filler (isIso D) (sym p) (⋆Iso f (invIso h) .snd) in
                ⋆InvRMove (F-Iso {F = B} (_ , isom-path i1)) (sym (α .N-hom k))
              ∙ (λ i → A .F-hom (p i) ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ F-Iso {F = B} (p i , isom-path (~ i)) .snd .inv)
              ∙ (λ i → A .F-seq (f .fst) (h .snd .inv) i ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ F-Iso-Pres⋆ {F = B} h (invIso f) i .fst)
              ∙ sym (E .⋆Assoc _ _ _)
              ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _)
              ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _))
            (full _ _ (f .fst ⋆⟨ D ⟩ h .snd .inv)))
        (surj d)

    mor-eq : (d : D .ob)(c : C .ob)(f : CatIso D (F .F-ob c) d)
      → isContrMor d .fst .fst ≡ A .F-hom (f .snd .inv) ⋆⟨ E ⟩ α .N-ob c ⋆⟨ E ⟩ B .F-hom (f .fst)
    mor-eq d c f =
        ⋆InvLMove (F-Iso {F = A} f) (⋆InvRMove (invIso (F-Iso {F = B} f)) (sym (isContrMor d .fst .snd c f)))
      ∙ sym (E .⋆Assoc _ _ _)

    F-seq3 : (F : Functor D E) {x y z w : D .ob}
      → {f : D [ x , y ]}{g : D [ y , z ]}{h : D [ z , w ]}
      → F .F-hom (f ⋆⟨ D ⟩ g ⋆⟨ D ⟩ h) ≡ F .F-hom f ⋆⟨ E ⟩ F .F-hom g ⋆⟨ E ⟩ F .F-hom h
    F-seq3 F = F .F-seq _ _ ∙ cong (λ x → x ⋆⟨ E ⟩ _) (F .F-seq _ _)

    ext : NatTrans A B
    ext .N-ob d = isContrMor d .fst .fst
    ext .N-hom {x = d} {y = d'} f = Prop.rec2 (E .isSetHom _ _)
        (λ (c , h) (c' , h') → Prop.rec (E .isSetHom _ _)
        (λ (k , p) →
            (λ i → A .F-hom f ⋆⟨ E ⟩ mor-eq d' c' h' i)
          ∙ cong (λ x → A .F-hom f ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _)
          ∙ sym (E .⋆Assoc _ _ _) ∙ sym (E .⋆Assoc _ _ _)
          ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆IdL _))
          ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-Iso {F = A} h .snd .sec))
          ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _)
          ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _))
          ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-seq3 A))
          ∙ cong (λ x → A .F-hom (invIso h .fst) ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (cong (A .F-hom) p))
          ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _)
          ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _) (α .N-hom k)
          ∙ cong (λ x → x ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _))
          ∙ E .⋆Assoc _ _ _
          ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (x ⋆⟨ E ⟩ B .F-hom (h' .fst))) (cong (B .F-hom) p)
          ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (x ⋆⟨ E ⟩ B .F-hom (h' .fst))) (F-seq3 B)
          ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _)
          ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (_ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x)) (F-Iso {F = B} h' .snd .sec)
          ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x) (E .⋆IdR _)
          ∙ sym (E .⋆Assoc _ _ _)
          ∙ (λ i → mor-eq d c h (~ i) ⋆⟨ E ⟩ B .F-hom f))
        (full _ _ (h .fst ⋆⟨ D ⟩ f ⋆⟨ D ⟩ h' .snd .inv)))
        (surj d) (surj d')

    ext≡ : precomposeF E F .F-hom ext ≡ α
    ext≡ = makeNatTransPath (λ i c →
        (mor-eq _ c idCatIso
      ∙ (λ i → A .F-id i ⋆⟨ E ⟩ α .N-ob c ⋆⟨ E ⟩ B .F-id i)
      ∙ E .⋆IdR _ ∙ E .⋆IdL _) i)


  -- As a corollary, if F is essential surjective and full, (- ∘ F) is fully faithfull.

  isEssSurj+Full→isFullyFaithfulPrecomp : isEssentiallySurj F → isFull F → isFullyFaithful (precomposeF E F)
  isEssSurj+Full→isFullyFaithfulPrecomp surj full =
    isFull+Faithful→isFullyFaithful {F = precomposeF E F}
      (isEssSurj+Full→isFullPrecomp surj full) (isEssSurj→isFaithfulPrecomp surj)


module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
  {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
  {E : Category ℓE ℓE'} (isUnivE : isUnivalent E)
  (F : Functor C D)
  where
  open isUnivalent isUnivE

  -- If F is weak equivalence and the target category is univalent, (- ∘ F) is essentially surjective.

  isWeakEquiv→isEssSurjPrecomp : isWeakEquivalence F → isEssentiallySurj (precomposeF E F)
  isWeakEquiv→isEssSurjPrecomp w-equiv G = ∣ Ext , Ext≃ ∣₁
    where
    Obj : (d : D .ob) → Type _
    Obj d = Σ[ e ∈ E .ob ]
      Σ[ k ∈ ((c : C .ob)(h : CatIso D (F .F-ob c) d) → CatIso E (G .F-ob c) e) ]
        ((c c' : C .ob)(h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d)
          → (f : C [ c , c' ])
          → F .F-hom f ⋆⟨ D ⟩ h' .fst ≡ h .fst
          → G .F-hom f ⋆⟨ E ⟩ k c' h' .fst ≡ k c h .fst)

    module _ {d} {c c'} (h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d) where

      liftH : CatIso C c c'
      liftH = liftIso {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h'))

      liftH-eq' : F .F-hom (liftH .fst) ≡ h .fst ⋆⟨ D ⟩ h' .snd .inv
      liftH-eq' = cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h')))

      liftH-eq : F .F-hom (liftH .fst) ⋆⟨ D ⟩ h' .fst ≡ h .fst
      liftH-eq =
          cong (λ x → x ⋆⟨ D ⟩ _) liftH-eq'
        ∙ D .⋆Assoc _ _ _
        ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (h' .snd .sec)
        ∙ D .⋆IdR _

    module _ (d : D .ob)(c₀ : C .ob)(h₀ : CatIso D (F .F-ob c₀) d) where

      isContrObj' : isContr (Obj d)
      isContrObj' .fst .fst = G .F-ob c₀
      isContrObj' .fst .snd .fst c h = F-Iso {F = G} (liftH h h₀)
      isContrObj' .fst .snd .snd c c' h h' f p = sym (G .F-seq _ _) ∙ cong (G .F-hom) g-path
        where
        g-path : f ⋆⟨ C ⟩ liftH h' h₀ .fst ≡ liftH h h₀ .fst
        g-path = isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _
           (F .F-seq _ _
          ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (liftH-eq' h' h₀)
          ∙ sym (D .⋆Assoc _ _ _)
          ∙ cong (λ x → x ⋆⟨ D ⟩ invIso h₀ .fst) p
          ∙ cong fst (sym (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h₀)))))
      isContrObj' .snd (e , k , coh) i .fst = CatIsoToPath (k c₀ h₀) i
      isContrObj' .snd (e , k , coh) i .snd .fst c h =
        let isom₀ = F-Iso {F = G} (liftH h h₀) in
        hcomp (λ j → λ
          { (i = i0) → isom₀
          ; (i = i1) → CatIso≡ (⋆Iso isom₀ (k c₀ h₀)) (k c h) (coh c c₀ h h₀ (liftH h h₀ .fst) (liftH-eq h h₀)) j })
        (transportIsoToPathIso isUnivE isom₀ _ i)
      isContrObj' .snd x@(e , k , coh) i .snd .snd =
        isProp→PathP (λ i → isPropΠ6 (λ c c' h h' f _ →
          E .isSetHom
            (G .F-hom f ⋆⟨ E ⟩ isContrObj' .snd x i .snd .fst c' h' .fst)
            (isContrObj' .snd x i .snd .fst c h .fst)))
        (isContrObj' .fst .snd .snd) coh i

    isContrObj : (d : D .ob) → isContr (Obj d)
    isContrObj d = Prop.rec isPropIsContr (λ (c , h) → isContrObj' d c h) (w-equiv .esssurj d)

    Ext-ob : D .ob → E .ob
    Ext-ob d = isContrObj d .fst .fst

    k : {d : D .ob}{c : C .ob}(h : CatIso D (F .F-ob c) d) → CatIso E (G .F-ob c) (Ext-ob d)
    k = isContrObj _ .fst .snd .fst _

    k-eq : {d : D .ob}{c c' : C .ob}
      (h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d)
      → (f : C [ c , c' ])
      → F .F-hom f ⋆⟨ D ⟩ h' .fst ≡ h .fst
      → G .F-hom f ⋆⟨ E ⟩ k h' .fst ≡ k h .fst
    k-eq = isContrObj _ .fst .snd .snd _ _

    Mor : (d d' : D .ob)(f : D [ d , d' ]) → Type _
    Mor d d' f =
      Σ[ g ∈ E [ Ext-ob d , Ext-ob d' ] ]
        ((c c' : C .ob)(h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d')
          → (l : C [ c , c' ])
          → F .F-hom l ⋆⟨ D ⟩ h' .fst ≡ h .fst ⋆⟨ D ⟩ f
          → G .F-hom l ⋆⟨ E ⟩ k h' .fst ≡ k h .fst ⋆⟨ E ⟩ g)

    module _ (d d' : D .ob)(f : D [ d , d' ])
      (c₀ : C .ob)(h₀ : CatIso D (F .F-ob c₀) d )
      (c₁ : C .ob)(h₁ : CatIso D (F .F-ob c₁) d')
      (l₀ : C [ c₀ , c₁ ])(p₀ : F .F-hom l₀ ⋆⟨ D ⟩ h₁ .fst ≡ h₀ .fst ⋆⟨ D ⟩ f)
      where

      g₀ = k h₀ .snd .inv ⋆⟨ E ⟩ G .F-hom l₀ ⋆⟨ E ⟩ k h₁ .fst

      isContrMor' : isContr (Mor d d' f)
      isContrMor' .fst .fst = g₀
      isContrMor' .fst .snd c c' h h' l p =
          cong (λ x → _ ⋆⟨ E ⟩ x) (⋆InvLMove (F-Iso {F = G} m') (k-eq h₁ h' _ m'-eq))
        ∙ sym (E .⋆Assoc _ _ _)
        ∙ cong (λ x → x ⋆⟨ E ⟩ k h₁ .fst) Gm-path'
        ∙ cong (λ x → x ⋆⟨ E ⟩ G .F-hom l₀ ⋆⟨ E ⟩ k h₁ .fst) m-eq'
        ∙ E .⋆Assoc _ _ _ ∙ E .⋆Assoc _ _ _
        ∙ cong (λ x → k h .fst ⋆⟨ E ⟩ x) (sym (E .⋆Assoc _ _ _))
        where
        m = liftH h₀ h
        m-eq = liftH-eq h₀ h
        m' = liftH h₁ h'
        m'-eq = liftH-eq h₁ h'

        m-eq' : G .F-hom (m .snd .inv) ≡ k h .fst ⋆⟨ E ⟩ k h₀ .snd .inv
        m-eq' = ⋆InvRMove (k h₀) (sym (⋆InvLMove (F-Iso {F = G} m) (k-eq h₀ h _ m-eq)))

        Fm-path : F .F-hom (l₀ ⋆⟨ C ⟩ m' .fst) ≡ F .F-hom (m .fst ⋆⟨ C ⟩ l)
        Fm-path =
            F .F-seq _ _
          ∙ cong (λ x → F .F-hom l₀ ⋆⟨ D ⟩ x) (liftH-eq' h₁ h')
          ∙ sym (D .⋆Assoc _ _ _)
          ∙ cong (λ x → x ⋆⟨ D ⟩ _) p₀
          ∙ cong (λ x → x ⋆⟨ D ⟩ _ ⋆⟨ D ⟩ _) (sym (D .⋆IdR _))
          ∙ cong (λ x → _ ⋆⟨ D ⟩ x ⋆⟨ D ⟩ _ ⋆⟨ D ⟩ _) (sym (h .snd .sec))
          ∙ cong (λ x → x ⋆⟨ D ⟩ _ ⋆⟨ D ⟩ _) (sym (D .⋆Assoc _ _ _))
          ∙ cong (λ x → x ⋆⟨ D ⟩ _) (D .⋆Assoc _ _ _)
          ∙ D .⋆Assoc _ _ _
          ∙ (λ i → ⋆InvRMove h m-eq (~ i) ⋆⟨ D ⟩ ⋆InvRMove h' p (~ i))
          ∙ sym (F .F-seq _ _)

        m-path : l₀ ⋆⟨ C ⟩ m' .fst ≡ m .fst ⋆⟨ C ⟩ l
        m-path = isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ Fm-path

        Gm-path : G .F-hom l₀ ⋆⟨ E ⟩ G .F-hom (m' .fst) ≡ G .F-hom (m .fst) ⋆⟨ E ⟩ G .F-hom l
        Gm-path = sym (G .F-seq _ _) ∙ cong (G .F-hom) m-path ∙ G .F-seq _ _

        Gm-path' : G .F-hom l ⋆⟨ E ⟩ G .F-hom (m' .snd .inv) ≡ G .F-hom (m .snd .inv) ⋆⟨ E ⟩ G .F-hom l₀
        Gm-path' = ⋆InvLMove (F-Iso {F = G} m) (sym (⋆InvRMove (F-Iso {F = G} m') Gm-path ∙ E .⋆Assoc _ _ _))

      isContrMor' .snd (g₁ , coh₁) i .fst =
         (⋆InvLMove (k h₀) (sym (isContrMor' .fst .snd c₀ c₁ h₀ h₁ l₀ p₀))
        ∙ sym (⋆InvLMove (k h₀) (sym (coh₁ c₀ c₁ h₀ h₁ l₀ p₀)))) i
      isContrMor' .snd x@(g₁ , coh₁) i .snd =
        isProp→PathP (λ i → isPropΠ6 (λ c c' h h' l _ →
          E .isSetHom
            (G .F-hom l ⋆⟨ E ⟩ k h' .fst)
            (k h .fst ⋆⟨ E ⟩ isContrMor' .snd x i .fst)))
        (isContrMor' .fst .snd) coh₁ i

    module _ {c c'} {d d'}
      (f : D [ d , d' ])(h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d')
      where

      liftL : C [ c , c' ]
      liftL = invEq (_ , w-equiv .fullfaith _ _) (h .fst ⋆⟨ D ⟩ f ⋆⟨ D ⟩ h' .snd .inv)

      liftL-eq : F .F-hom liftL ⋆⟨ D ⟩ h' .fst ≡ h .fst ⋆⟨ D ⟩ f
      liftL-eq =
        sym (⋆InvRMove (invIso h')
          (sym (secEq (_ , w-equiv .fullfaith _ _) (h .fst ⋆⟨ D ⟩ f ⋆⟨ D ⟩ h' .snd .inv))))

    isContrMor : (d d' : D .ob)(f : D [ d , d' ]) → isContr (Mor d d' f)
    isContrMor d d' f = Prop.rec2 isPropIsContr
      (λ (c₀ , h₀) (c₁ , h₁) →
        isContrMor' d d' f c₀ h₀ c₁ h₁ (liftL f h₀ h₁) (liftL-eq f h₀ h₁))
      (w-equiv .esssurj d) (w-equiv .esssurj d')

    Ext-hom : {d d' : D .ob}(f : D [ d , d' ]) → E [ Ext-ob d , Ext-ob d' ]
    Ext-hom f = isContrMor _ _ f .fst .fst

    liftL⋆ : ∀ {c c' c''} {d d' d''}
      (f : D [ d , d' ])(g : D [ d' , d'' ])
      (h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d')(h'' : CatIso D (F .F-ob c'') d'')
      → liftL (f ⋆⟨ D ⟩ g) h h'' ≡ liftL f h h' ⋆⟨ C ⟩ liftL g h' h''
    liftL⋆ f g h h' h'' = isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _
      (⋆CancelR h'' path ∙ sym (F .F-seq _ _))
      where
      path : _
      path = liftL-eq (f ⋆⟨ D ⟩ g) h h''
        ∙ sym (D .⋆Assoc _ _ _)
        ∙ cong (λ x → x ⋆⟨ D ⟩ _) (sym (liftL-eq f h h'))
        ∙ D .⋆Assoc _ _ _
        ∙ cong (λ x → F .F-hom (liftL f h h') ⋆⟨ D ⟩ x) (sym (liftL-eq g h' h''))
        ∙ sym (D .⋆Assoc _ _ _)

    Ext : Functor D E
    Ext .F-ob  = Ext-ob
    Ext .F-hom = Ext-hom
    Ext .F-id {x = d} = Prop.rec (E .isSetHom _ _)
      (λ (c , h) →
        let r = isContrMor _ _ (D .id {x = d}) .fst .snd _ _ h h (C .id)
              (cong (λ x → x ⋆⟨ D ⟩ _) (F .F-id) ∙ D .⋆IdL _ ∙ sym (D .⋆IdR _))
        in  ⋆CancelL (k h) (sym r ∙ cong (λ x → x ⋆⟨ E ⟩ (k h .fst)) (G .F-id) ∙ E .⋆IdL _ ∙ sym (E .⋆IdR _)))
      (w-equiv .esssurj d)
    Ext .F-seq {x = a} {y = b} {z = c} f g =
      Prop.rec3 (E .isSetHom _ _)
      (λ (_ , ha) (_ , hb) (_ , hc) →
        let rf = isContrMor _ _ _ .fst .snd _ _ ha hb (liftL f ha hb) (liftL-eq f ha hb)
            rg = isContrMor _ _ _ .fst .snd _ _ hb hc (liftL g hb hc) (liftL-eq g hb hc)
            rfg = isContrMor _ _ _ .fst .snd _ _ ha hc (liftL (f ⋆⟨ D ⟩ g) ha hc) (liftL-eq (f ⋆⟨ D ⟩ g) ha hc)
        in  ⋆CancelL (k ha)
               (sym rfg
              ∙ cong (λ x → x ⋆⟨ E ⟩ k hc .fst) (cong (G .F-hom) (liftL⋆ f g ha hb hc) ∙ G .F-seq _ _)
              ∙ E .⋆Assoc _ _ _
              ∙ cong (λ x → G .F-hom _ ⋆⟨ E ⟩ x) rg
              ∙ sym (E .⋆Assoc _ _ _)
              ∙ cong (λ x → x ⋆⟨ E ⟩ Ext-hom g) rf
              ∙ E .⋆Assoc _ _ _))
      (w-equiv .esssurj a) (w-equiv .esssurj b) (w-equiv .esssurj c)

    objFc : (c : C .ob) → Obj (F .F-ob c)
    objFc c₀ .fst = G .F-ob c₀
    objFc c₀ .snd .fst c h = F-Iso {F = G} (liftIso {F = F} (w-equiv .fullfaith) h)
    objFc c₀ .snd .snd c c' h h' f p = sym (G .F-seq _ _)
      ∙ cong (G .F-hom) (isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ path)
      where
      path : _
      path =
          F .F-seq _ _
        ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) h'))
        ∙ p ∙ sym (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) h))

    Ext-ob≡ : (c : C .ob) → Ext-ob (F .F-ob c) ≡ G .F-ob c
    Ext-ob≡ c₀ = cong fst (isContrObj _ .snd (objFc c₀))

    Ext-hom≡ : {c c' : C .ob}(f : C [ c , c' ])
      → PathP (λ i → E [ Ext-ob≡ c i , Ext-ob≡ c' i ]) (Ext-hom (F .F-hom f)) (G .F-hom f)
    Ext-hom≡  {c = c} {c' = c'} f i =
      hcomp (λ j → λ
        { (i = i0) → isContrMor _ _ _ .snd morFf (~ j) .fst
        ; (i = i1) → G .F-hom f })
      (transpGf-filler (~ i))
      where
      transpGf-filler = transport-filler (λ i → E [ Ext-ob≡ c (~ i) , Ext-ob≡ c' (~ i) ]) (G .F-hom f)

      morFf : Mor _ _ (F .F-hom f)
      morFf .fst = transpGf-filler i1
      morFf .snd c c' h h' l p =
        transport (λ i → G .F-hom l ⋆⟨ E ⟩ isContrObj _ .snd (objFc _) (~ i) .snd .fst c' h' .fst
          ≡ isContrObj _ .snd (objFc _) (~ i) .snd .fst c h .fst ⋆⟨ E ⟩ transpGf-filler i) G-path
        where
        F-path : _
        F-path =
            F .F-seq _ _
          ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) h')) ∙ p
          ∙ cong (λ x → x ⋆⟨ D ⟩ _) (sym (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) h)))
          ∙ sym (F .F-seq _ _)

        G-path : _
        G-path =
            sym (G .F-seq _ _)
          ∙ cong (G .F-hom) (isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ F-path)
          ∙ G .F-seq _ _

    Ext≡ : precomposeF E F .F-ob Ext ≡ G
    Ext≡ = Functor≡ Ext-ob≡ Ext-hom≡

    Ext≃ : CatIso _ (precomposeF E F .F-ob Ext) G
    Ext≃ = NatIso→FUNCTORIso _ _ (pathToNatIso Ext≡)


  -- As a corollary, if F is weak equivalence and the target category is univalent, (- ∘ F) is a weak equivalence.

  isWeakEquiv→isWeakEquivPrecomp : isWeakEquivalence F → isWeakEquivalence (precomposeF E F)
  isWeakEquiv→isWeakEquivPrecomp w-equiv .fullfaith =
    isEssSurj+Full→isFullyFaithfulPrecomp E F (w-equiv .esssurj) (isFullyFaithful→Full {F = F} (w-equiv .fullfaith))
  isWeakEquiv→isWeakEquivPrecomp w-equiv .esssurj   = isWeakEquiv→isEssSurjPrecomp w-equiv

  -- Moreover, using assumption of being univalent, (- ∘ F) is actually an equivalence.

  isWeakEquiv→isEquivPrecomp : isWeakEquivalence F → isEquivalence (precomposeF E F)
  isWeakEquiv→isEquivPrecomp w-equiv =
    isWeakEquiv→isEquiv (isUnivalentFUNCTOR _ _ isUnivE) (isUnivalentFUNCTOR _ _ isUnivE)
      (isWeakEquiv→isWeakEquivPrecomp w-equiv)

module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
  {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} {E : Category ℓE ℓE'}
  {G : Functor D E}
  (isFullyFaithfulG : isFullyFaithful G)
  where

  private
    GFF : ∀ {x y} → D [ x , y ] ≃ E [ G ⟅ x ⟆ , G ⟅ y ⟆ ]
    GFF = _ , (isFullyFaithfulG _ _)

    GFaith : ∀ {x y} → (D [ x , y ]) ↪ (E [ G ⟅ x ⟆ , G ⟅ y ⟆ ])
    GFaith = _ , isEquiv→isEmbedding (GFF .snd)
    -- this would be convenient as FF.Reasoning
    G-hom⁻ : ∀ {x y} → E [ G ⟅ x ⟆ , G ⟅ y ⟆ ] → D [ x , y ]
    G-hom⁻ = invIsEq (isFullyFaithfulG _ _)


  isFullyFaithfulPostcomposeF : isFullyFaithful (postcomposeF C G)
  isFullyFaithfulPostcomposeF F F' .equiv-proof α =
    uniqueExists
      (natTrans (λ x → G-hom⁻ (α ⟦ x ⟧)) λ f →
        isEmbedding→Inj (GFaith .snd) _ _
        ( G .F-seq _ _
        ∙ cong₂ (seq' E) refl (secEq GFF _)
        ∙ α.N-hom _
        ∙ sym (cong₂ (seq' E) (secEq GFF _) refl)
        ∙ sym (G .F-seq _ _)))
      (makeNatTransPath (funExt λ c → secIsEq (isFullyFaithfulG _ _) (α ⟦ c ⟧)))
      (λ _ → isSetNatTrans _ _)
      λ β G∘β≡α → makeNatTransPath (funExt λ c →
        isEmbedding→Inj (isEquiv→isEmbedding (isFullyFaithfulG _ _)) _ _
        (secIsEq (isFullyFaithfulG _ _) _ ∙ sym (cong (_⟦ c ⟧) G∘β≡α)))

    where module α = NatTrans α