------------------------------------------------------------------------
-- 1-categories
------------------------------------------------------------------------

-- The code is based on the presentation in the HoTT book (but might
-- not follow it exactly).

{-# OPTIONS --without-K #-}

open import Equality

module Category
  {reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

open import Bijection eq as Bijection using (_↔_)
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq
  using (_≃_; ⟨_,_⟩; module _≃_; Is-equivalence)
open import Function-universe eq as F hiding (id) renaming (_∘_ to _⊚_)
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence using (module _⇔_)
import Nat eq as Nat
open import Prelude as P hiding (id; Unit)
open import Univalence-axiom eq

------------------------------------------------------------------------
-- Precategories

Precategory′ : (ℓ₁ ℓ₂ : Level)  Set (lsuc (ℓ₁  ℓ₂))
Precategory′ ℓ₁ ℓ₂ =
  -- Objects.
   λ (Obj : Set ℓ₁) 

  -- Morphisms (a /set/).
   λ (HOM : Obj  Obj  SET ℓ₂) 
  let Hom = λ X Y  proj₁ (HOM X Y) in

  -- Identity.
   λ (id :  {X}  Hom X X) 

  -- Composition.
   λ (_∙_ :  {X Y Z}  Hom Y Z  Hom X Y  Hom X Z) 

  -- Identity laws.
  (∀ {X Y} {f : Hom X Y}  (id  f)  f) ×
  (∀ {X Y} {f : Hom X Y}  (f  id)  f) ×

  -- Associativity.
  (∀ {X Y Z U} {f : Hom X Y} {g : Hom Y Z} {h : Hom Z U} 
     (h  (g  f))  ((h  g)  f))

-- A wrapper.

record Precategory (ℓ₁ ℓ₂ : Level) : Set (lsuc (ℓ₁  ℓ₂)) where
  field
    precategory : Precategory′ ℓ₁ ℓ₂

  -- Objects.

  Obj : Set ℓ₁
  Obj = proj₁ precategory

  -- Morphisms.

  HOM : Obj  Obj  SET ℓ₂
  HOM = proj₁ (proj₂ precategory)

  -- The morphism type family.

  Hom : Obj  Obj  Set ℓ₂
  Hom X Y = proj₁ (HOM X Y)

  -- The morphism types are sets.

  Hom-is-set :  {X Y}  Is-set (Hom X Y)
  Hom-is-set = proj₂ (HOM _ _)

  -- Identity.

  id :  {X}  Hom X X
  id = proj₁ (proj₂ (proj₂ precategory))

  -- Composition.

  infixr 10 _∙_

  _∙_ :  {X Y Z}  Hom Y Z  Hom X Y  Hom X Z
  _∙_ = proj₁ (proj₂ (proj₂ (proj₂ precategory)))

  -- The left identity law.

  left-identity :  {X Y} {f : Hom X Y}  id  f  f
  left-identity = proj₁ (proj₂ (proj₂ (proj₂ (proj₂ precategory))))

  -- The right identity law.

  right-identity :  {X Y} {f : Hom X Y}  f  id  f
  right-identity =
    proj₁ (proj₂ (proj₂ (proj₂ (proj₂ (proj₂ precategory)))))

  -- The associativity law.

  assoc :  {X Y Z U} {f : Hom X Y} {g : Hom Y Z} {h : Hom Z U} 
          h  (g  f)  (h  g)  f
  assoc =
    proj₂ (proj₂ (proj₂ (proj₂ (proj₂ (proj₂ precategory)))))

  -- Isomorphisms.

  Is-isomorphism :  {X Y}  Hom X Y  Set ℓ₂
  Is-isomorphism f =  λ g  (f  g  id) × (g  f  id)

  infix 4 _≅_

  _≅_ : Obj  Obj  Set ℓ₂
  X  Y =  λ (f : Hom X Y)  Is-isomorphism f

  -- Some projections.

  infix 15  _⁻¹ _¹⁻¹ _⁻¹¹

   :  {X Y}  X  Y  Hom X Y
  f ¹ = proj₁ f

  _⁻¹ :  {X Y}  X  Y  Hom Y X
  f ⁻¹ = proj₁ (proj₂ f)

  _¹⁻¹ :  {X Y} (f : X  Y)  f ¹  f ⁻¹  id
  f ¹⁻¹ = proj₁ (proj₂ (proj₂ f))

  _⁻¹¹ :  {X Y} (f : X  Y)  f ⁻¹  f ¹  id
  f ⁻¹¹ = proj₂ (proj₂ (proj₂ f))

  abstract

    -- "Is-isomorphism f" is a proposition.

    Is-isomorphism-propositional :
       {X Y} (f : Hom X Y) 
      Is-proposition (Is-isomorphism f)
    Is-isomorphism-propositional f =
      _⇔_.from propositional⇔irrelevant
        λ { (g , fg , gf) (g′ , fg′ , g′f) 
            Σ-≡,≡→≡ (g             ≡⟨ sym left-identity 
                     id  g        ≡⟨ cong  h  h  g) $ sym g′f 
                     (g′  f)  g  ≡⟨ sym assoc 
                     g′  (f  g)  ≡⟨ cong (_∙_ g′) fg 
                     g′  id       ≡⟨ right-identity ⟩∎
                     g′            )
                    (Σ-≡,≡→≡ (_⇔_.to set⇔UIP Hom-is-set _ _)
                             (_⇔_.to set⇔UIP Hom-is-set _ _)) }

    -- Isomorphism equality is equivalent to "forward morphism"
    -- equality.

    ≡≃≡¹ :  {X Y} {f g : X  Y}  (f  g)  (f ¹  g ¹)
    ≡≃≡¹ {f = f} {g} =
      (f  g)      ↔⟨ inverse $ ignore-propositional-component $ Is-isomorphism-propositional _ ⟩□
      (f ¹  g ¹)  

    -- The type of isomorphisms (between two objects) is a set.

    ≅-set :  {X Y}  Is-set (X  Y)
    ≅-set = Σ-closure 2 Hom-is-set
                       _  mono₁ 1 $ Is-isomorphism-propositional _)

  -- Identity isomorphism.

  id≅ :  {X}  X  X
  id≅ = id , id , left-identity , right-identity

  -- Composition of isomorphisms.

  infixr 10 _∙≅_

  _∙≅_ :  {X Y Z}  Y  Z  X  Y  X  Z
  f ∙≅ g = (f ¹  g ¹) , (g ⁻¹  f ⁻¹) , fg f g , gf f g
    where
    abstract
      fg :  {X Y Z} (f : Y  Z) (g : X  Y) 
           (f ¹  g ¹)  (g ⁻¹  f ⁻¹)  id
      fg f g =
        (f ¹  g ¹)  (g ⁻¹  f ⁻¹)  ≡⟨ sym assoc 
        f ¹  (g ¹  (g ⁻¹  f ⁻¹))  ≡⟨ cong (_∙_ (f ¹)) assoc 
        f ¹  ((g ¹  g ⁻¹)  f ⁻¹)  ≡⟨ cong  h  f ¹  (h  f ⁻¹)) $ g ¹⁻¹ 
        f ¹  (id  f ⁻¹)            ≡⟨ cong (_∙_ (f ¹)) left-identity 
        f ¹  f ⁻¹                   ≡⟨ f ¹⁻¹ ⟩∎
        id                           

      gf :  {X Y Z} (f : Y  Z) (g : X  Y) 
           (g ⁻¹  f ⁻¹)  (f ¹  g ¹)  id
      gf f g =
        (g ⁻¹  f ⁻¹)  (f ¹  g ¹)  ≡⟨ sym assoc 
        g ⁻¹  (f ⁻¹  (f ¹  g ¹))  ≡⟨ cong (_∙_ (g ⁻¹)) assoc 
        g ⁻¹  ((f ⁻¹  f ¹)  g ¹)  ≡⟨ cong  h  g ⁻¹  (h  g ¹)) $ f ⁻¹¹ 
        g ⁻¹  (id  g ¹)            ≡⟨ cong (_∙_ (g ⁻¹)) left-identity 
        g ⁻¹  g ¹                   ≡⟨ g ⁻¹¹ ⟩∎
        id                           

  -- The inverse of an isomorphism.

  infix 15 _⁻¹≅

  _⁻¹≅ :  {X Y}  X  Y  Y  X
  f ⁻¹≅ = f ⁻¹ , f ¹ , f ⁻¹¹ , f ¹⁻¹

  -- Isomorphisms form a precategory.

  precategory-≅ : Precategory ℓ₁ ℓ₂
  precategory-≅ = record { precategory =
    Obj ,
     X Y  (X  Y) , ≅-set) ,
    id≅ , _∙≅_ ,
    _≃_.from ≡≃≡¹ left-identity ,
    _≃_.from ≡≃≡¹ right-identity ,
    _≃_.from ≡≃≡¹ assoc }

  -- Equal objects are isomorphic.

  ≡→≅ :  {X Y}  X  Y  X  Y
  ≡→≅ = elim  {X Y} _  X  Y)  _  id≅)

  -- "Computation rule" for ≡→≅.

  ≡→≅-refl :  {X}  ≡→≅ (refl X)  id≅
  ≡→≅-refl = elim-refl  {X Y} _  X  Y) _

  -- Rearrangement lemma for ≡→≅.

  ≡→≅-¹ :
     {X Y} (X≡Y : X  Y) 
    ≡→≅ X≡Y ¹  elim  {X Y} _  Hom X Y)  _  id) X≡Y
  ≡→≅-¹ {X} = elim¹
     X≡Y  ≡→≅ X≡Y ¹ 
             elim  {X Y} _  Hom X Y)  _  id) X≡Y)
    (≡→≅ (refl X) ¹                                  ≡⟨ cong  ≡→≅-refl 
     id≅ ¹                                           ≡⟨⟩
     id                                              ≡⟨ sym $ elim-refl  {X Y} _  Hom X Y) _ ⟩∎
     elim  {X Y} _  Hom X Y)  _  id) (refl X)  )

  -- A lemma that can be used to prove that ≡→≅ is an equivalence.

  ≡→≅-equivalence-lemma :
     {X} 
    (≡≃≅ :  {Y}  (X  Y)  (X  Y)) 
    _≃_.to ≡≃≅ (refl X) ¹  id 
     {Y}  Is-equivalence (≡→≅ {X = X} {Y = Y})
  ≡→≅-equivalence-lemma {X} ≡≃≅ ≡≃≅-refl {Y} =
    Eq.respects-extensional-equality
      (elim¹  X≡Y  _≃_.to ≡≃≅ X≡Y  ≡→≅ X≡Y)
             (_≃_.to ≡≃≅ (refl X)  ≡⟨ _≃_.from ≡≃≡¹ ≡≃≅-refl 
              id≅                  ≡⟨ sym ≡→≅-refl ⟩∎
              ≡→≅ (refl X)         ))
      (_≃_.is-equivalence ≡≃≅)

-- An example: sets and functions. (Defined using extensionality.)

precategory-Set :
  ( : Level) 
  Extensionality   
  Precategory (lsuc ) 
precategory-Set  ext = record { precategory =

  -- Objects: sets.
  SET  ,

  -- Morphisms: functions.
   { (A , A-set) (B , B-set) 
       (A  B) , Π-closure ext 2  _  B-set) }) ,

  -- Identity.
  P.id ,

  -- Composition.
   f g  f  g) ,

  -- Laws.
  refl _ , refl _ , refl _ }

-- Isomorphisms in this category are equivalent to equivalences
-- (assuming extensionality).

≃≃≅-Set :
  ( : Level) (ext : Extensionality  ) 
  let open Precategory (precategory-Set  ext) in
  (X Y : Obj)  (Type X  Type Y)  (X  Y)
≃≃≅-Set  ext X Y = Eq.↔⇒≃ record
  { surjection = record
    { logical-equivalence = record
      { to   = λ X≃Y  _≃_.to X≃Y , _≃_.from X≃Y ,
                       ext (_≃_.right-inverse-of X≃Y) ,
                       ext (_≃_.left-inverse-of  X≃Y)
      ; from = λ X≅Y  Eq.↔⇒≃ record
                 { surjection = record
                   { logical-equivalence = record
                     { to   = proj₁ X≅Y
                     ; from = proj₁ (proj₂ X≅Y)
                     }
                   ; right-inverse-of = λ x 
                       cong (_$ x) $ proj₁ (proj₂ (proj₂ X≅Y))
                   }
                 ; left-inverse-of = λ x 
                     cong (_$ x) $ proj₂ (proj₂ (proj₂ X≅Y))
                 }
      }
    ; right-inverse-of = λ X≅Y 
        _≃_.from (≡≃≡¹ {X = X} {Y = Y}) (refl (proj₁ X≅Y))
    }
  ; left-inverse-of = λ X≃Y 
      Eq.lift-equality ext (refl (_≃_.to X≃Y))
  }
  where open Precategory (precategory-Set  ext) using (≡≃≡¹)

-- Equality characterisation lemma for Precategory′.

equality-characterisation-Precategory′ :
   {ℓ₁ ℓ₂} {C D : Precategory′ ℓ₁ ℓ₂} 
  Extensionality (ℓ₁  ℓ₂) (ℓ₁  lsuc ℓ₂) 
  Univalence ℓ₁ 
  Univalence ℓ₂ 
  let module C = Precategory (record { precategory = C })
      module D = Precategory (record { precategory = D })
  in
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH :  X Y  C.Hom (_≃_.from eqO X) (_≃_.from eqO Y) 
                      D.Hom X Y) 
     (∀ X  _≃_.to (eqH X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        _≃_.to (eqH X Z) (C._∙_ (_≃_.from (eqH Y Z) f)
                                (_≃_.from (eqH X Y) g)) 
        f D.∙ g))
    
  C  D
equality-characterisation-Precategory′ {ℓ₁} {ℓ₂} {C} {D}
                                       ext univ₁ univ₂ =
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH :  X Y  C.Hom (_≃_.from eqO X) (_≃_.from eqO Y) 
                      D.Hom X Y) 
     (∀ X  _≃_.to (eqH X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        _≃_.to (eqH X Z) (C._∙_ (_≃_.from (eqH Y Z) f)
                                (_≃_.from (eqH X Y) g)) 
        f D.∙ g))                                                        ↝⟨ ∃-cong  _  inverse $
                                                                              Σ-cong (Eq.∀-preserves ext₁₁₂₊ λ _ 
                                                                                      Eq.∀-preserves ext₁₂₊  λ _ 
                                                                                      ≡≃≃ univ₂)
                                                                                      _  F.id)) 
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH :  X Y  C.Hom (_≃_.from eqO X) (_≃_.from eqO Y) 
                      D.Hom X Y) 
     (∀ X  ≡⇒→ (eqH X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        ≡⇒→ (eqH X Z) (C._∙_ (≡⇒← (eqH Y Z) f) (≡⇒← (eqH X Y) g)) 
        f D.∙ g))                                                        ↝⟨ inverse $ Σ-cong (≡≃≃ univ₁)  _  F.id) 

  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH :  X Y  C.Hom (≡⇒← eqO X) (≡⇒← eqO Y)  D.Hom X Y) 
     (∀ X  ≡⇒→ (eqH X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        ≡⇒→ (eqH X Z) (C._∙_ (≡⇒← (eqH Y Z) f) (≡⇒← (eqH X Y) g)) 
        f D.∙ g))                                                        ↝⟨ ∃-cong  _  inverse $
                                                                              Σ-cong (Eq.∀-preserves ext₁₁₂₊ λ _ 
                                                                                      Eq.∀-preserves ext₁₂₊  λ _ 
                                                                                      inverse $
                                                                                      Eq.↔⇒≃ $ ignore-propositional-component $
                                                                                                 H-level-propositional ext₂₂ 2)
                                                                                      _  F.id)) 
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH :  X Y  C.HOM (≡⇒← eqO X) (≡⇒← eqO Y)  D.HOM X Y) 
     let eqH′ = λ X Y  proj₁ (Σ-≡,≡←≡ (eqH X Y))
     in
     (∀ X  ≡⇒→ (eqH′ X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        ≡⇒→ (eqH′ X Z) (C._∙_ (≡⇒← (eqH′ Y Z) f) (≡⇒← (eqH′ X Y) g)) 
        f D.∙ g))                                                        ↝⟨ ∃-cong  _  ∃-cong λ _  ≡⇒↝ _ $
                                                                              cong  (eqH′ :  _ _  _) 
                                                                                      (∀ X  ≡⇒→ (eqH′ X X) C.id  D.id) ×
                                                                                      (∀ X Y Z f g 
                                                                                         ≡⇒→ (eqH′ X Z)
                                                                                           (C._∙_ (≡⇒← (eqH′ Y Z) f) (≡⇒← (eqH′ X Y) g))  f D.∙ g))
                                                                                   (ext₁₁₂₊ λ _  ext₁₂₊ λ _  proj₁-Σ-≡,≡←≡ _)) 
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH :  X Y  C.HOM (≡⇒← eqO X) (≡⇒← eqO Y)  D.HOM X Y) 
     let eqH′ = λ X Y  cong proj₁ (eqH X Y)
     in
     (∀ X  ≡⇒→ (eqH′ X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        ≡⇒→ (eqH′ X Z) (C._∙_ (≡⇒← (eqH′ Y Z) f) (≡⇒← (eqH′ X Y) g)) 
        f D.∙ g))                                                        ↝⟨ ∃-cong  _  inverse $
                                                                               Σ-cong (Eq.∀-preserves ext₁₁₂₊ λ _ 
                                                                                       inverse $ Eq.extensionality-isomorphism ext₁₂₊)
                                                                                       _  F.id)) 
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH :  X   Y  C.HOM (≡⇒← eqO X) (≡⇒← eqO Y))  D.HOM X) 
     let eqH′ = λ X Y  cong proj₁ (ext⁻¹ (eqH X) Y)
     in
     (∀ X  ≡⇒→ (eqH′ X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        ≡⇒→ (eqH′ X Z) (C._∙_ (≡⇒← (eqH′ Y Z) f) (≡⇒← (eqH′ X Y) g)) 
        f D.∙ g))                                                        ↝⟨ ∃-cong  _  inverse $
                                                                               Σ-cong (inverse $ Eq.extensionality-isomorphism ext₁₁₂₊)
                                                                                       _  F.id)) 
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH :  X Y  C.HOM (≡⇒← eqO X) (≡⇒← eqO Y))  D.HOM) 
     let eqH′ = λ X Y  cong proj₁ (ext⁻¹ (ext⁻¹ eqH X) Y)
     in
     (∀ X  ≡⇒→ (eqH′ X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        ≡⇒→ (eqH′ X Z) (C._∙_ (≡⇒← (eqH′ Y Z) f) (≡⇒← (eqH′ X Y) g)) 
        f D.∙ g))                                                        ↝⟨ ∃-cong  eqO  inverse $
                                                                              Σ-cong (inverse $ ≡⇒↝ equivalence (HOM-lemma eqO))
                                                                                      _  F.id)) 
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH : subst  Obj  Obj  Obj  SET _) eqO C.HOM  D.HOM) 
     let eqH′ = λ X Y 
                  cong proj₁
                    (ext⁻¹ (ext⁻¹ (≡⇒← (HOM-lemma eqO) eqH) X) Y)
     in
     (∀ X  ≡⇒→ (eqH′ X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        ≡⇒→ (eqH′ X Z) (C._∙_ (≡⇒← (eqH′ Y Z) f) (≡⇒← (eqH′ X Y) g)) 
        f D.∙ g))                                                        ↝⟨ ∃-cong  eqO  ∃-cong λ eqH  ≡⇒↝ _ $
                                                                              cong  (eqH′ :  _ _  _) 
                                                                                      (∀ X  ≡⇒→ (eqH′ X X) C.id  D.id) ×
                                                                                      (∀ X Y Z f g 
                                                                                         ≡⇒→ (eqH′ X Z)
                                                                                           (C._∙_ (≡⇒← (eqH′ Y Z) f) (≡⇒← (eqH′ X Y) g))  f D.∙ g))
                                                                                   (ext₁₁₂₊ λ X  ext₁₂₊ λ Y 
      cong proj₁ (ext⁻¹ (ext⁻¹ (≡⇒← (HOM-lemma eqO) eqH) X) Y)                        ≡⟨⟩
      cong proj₁ (cong (_$ Y) (cong (_$ X) (≡⇒← (HOM-lemma eqO) eqH)))                ≡⟨ cong (cong _) $ cong-∘ _ _ _ 
      cong proj₁ (cong  f  f X Y) (≡⇒← (HOM-lemma eqO) eqH))                       ≡⟨ cong-∘ _ _ _ ⟩∎
      cong  F  Type (F X Y)) (≡⇒← (HOM-lemma eqO) eqH)                             )) 

  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH : subst  Obj  Obj  Obj  SET _) eqO C.HOM  D.HOM) 
     let eqH′ = λ X Y 
                  cong  F  Type (F X Y)) (≡⇒← (HOM-lemma eqO) eqH)
     in
     (∀ X  ≡⇒→ (eqH′ X X) C.id  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        ≡⇒→ (eqH′ X Z) (C._∙_ (≡⇒← (eqH′ Y Z) f) (≡⇒← (eqH′ X Y) g)) 
        f D.∙ g))                                                        ↔⟨ ∃-cong  eqO  ∃-cong λ eqH 
                                                                              (Eq.∀-preserves ext₁₂ λ _ 
                                                                                 ≡⇒↝ _ $ cong (_≡ _) P-lemma)
                                                                                ×-cong
                                                                              (Eq.∀-preserves ext₁₁₂ λ X 
                                                                               Eq.∀-preserves ext₁₁₂ λ Y 
                                                                               Eq.∀-preserves ext₁₂  λ Z 
                                                                               Eq.∀-preserves ext₂₂  λ f 
                                                                               Eq.∀-preserves ext₂₂  λ g 
                                                                                 ≡⇒↝ _ $ cong (_≡ _) Q-lemma)) 
  ( λ (eqO : C.Obj  D.Obj) 
    λ (eqH : subst  Obj  Obj  Obj  SET _) eqO C.HOM  D.HOM) 
     (∀ X  subst₂ (uncurry P) eqO eqH C.id {X = X}  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        subst₂ (uncurry Q) eqO eqH C._∙_ f g  f D.∙ g))                 ↝⟨ Σ-assoc 

  ( λ (eq :  λ (eqO : C.Obj  D.Obj) 
               subst  Obj  Obj  Obj  SET _) eqO C.HOM  D.HOM) 
     (∀ X  subst (uncurry P) (uncurry Σ-≡,≡→≡ eq) C.id {X = X}  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        subst (uncurry Q) (uncurry Σ-≡,≡→≡ eq) C._∙_ f g  f D.∙ g))     ↝⟨ Σ-cong Bijection.Σ-≡,≡↔≡  _  F.id) 

  ( λ (eq : (C.Obj , C.HOM)  (D.Obj , D.HOM)) 
     (∀ X  subst (uncurry P) eq C.id {X = X}  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) (g : D.Hom X Y) 
        subst (uncurry Q) eq C._∙_ f g  f D.∙ g))                       ↔⟨ ∃-cong  _  ∃-cong λ _  Eq.∀-preserves ext₁₁₂ λ _ 
                                                                              Eq.∀-preserves ext₁₁₂ λ _  Eq.∀-preserves ext₁₂ λ _ 
                                                                                Eq.∀-preserves ext₂₂ λ _ 
                                                                                  Eq.extensionality-isomorphism ext₂₂) 
  ( λ (eq : (C.Obj , C.HOM)  (D.Obj , D.HOM)) 
     (∀ X  subst (uncurry P) eq C.id {X = X}  D.id)
       ×
     (∀ X Y Z (f : D.Hom Y Z) 
        subst (uncurry Q) eq C._∙_ {X = X} f  D._∙_ f))                 ↔⟨ ∃-cong  _  ∃-cong λ _  Eq.∀-preserves ext₁₁₂ λ _ 
                                                                              Eq.∀-preserves ext₁₁₂ λ _  Eq.∀-preserves ext₁₂ λ _ 
                                                                                Eq.extensionality-isomorphism ext₂₂) 
  ( λ (eq : (C.Obj , C.HOM)  (D.Obj , D.HOM)) 
     (∀ X  subst (uncurry P) eq C.id {X = X}  D.id)
       ×
     (∀ X Y Z 
        subst (uncurry Q) eq C._∙_ {X = X} {Y = Y} {Z = Z}  D._∙_))     ↔⟨ ∃-cong  _  ∃-cong λ _ 
                                                                              Eq.∀-preserves ext₁₁₂ λ _  Eq.∀-preserves ext₁₁₂ λ _ 
                                                                                implicit-extensionality-isomorphism ext₁₂) 
  ( λ (eq : (C.Obj , C.HOM)  (D.Obj , D.HOM)) 
     (∀ X  subst (uncurry P) eq C.id {X = X}  D.id)
       ×
     (∀ X Y 
         {_}  subst (uncurry Q) eq C._∙_ {X = X} {Y = Y})  D._∙_))   ↔⟨ ∃-cong  _  ∃-cong λ _  Eq.∀-preserves ext₁₁₂ λ _ 
                                                                              implicit-extensionality-isomorphism ext₁₁₂) 
  ( λ (eq : (C.Obj , C.HOM)  (D.Obj , D.HOM)) 
     (∀ X  subst (uncurry P) eq C.id {X = X}  D.id)
       ×
     (∀ X   {_ _}  subst (uncurry Q) eq C._∙_ {X = X})  D._∙_))     ↝⟨ ∃-cong  _ 
                                                                              implicit-extensionality-isomorphism ext₁₂
                                                                                ×-cong
                                                                              implicit-extensionality-isomorphism ext₁₁₂) 
  ( λ (eq : (C.Obj , C.HOM)  (D.Obj , D.HOM)) 
      {_}  subst (uncurry P) eq  {_}  C.id)) 
      {_}  D.id)
       ×
      {_ _ _}  subst (uncurry Q) eq  {_ _ _}  C._∙_)) 
      {_ _ _}  D._∙_))                                                ↝⟨ ∃-cong  _  ≡×≡↔≡) 

  ( λ (eq : (C.Obj , C.HOM)  (D.Obj , D.HOM)) 
     (  {_}      subst (uncurry P) eq  {_}      C.id))
     ,  {_ _ _}  subst (uncurry Q) eq  {_ _ _}  C._∙_))
     ) 
     ((λ {_}  D.id) , λ {_ _ _}  D._∙_))                               ↝⟨ ∃-cong  _  ≡⇒↝ _ $ cong (_≡ _) $ sym $ push-subst-, _ _) 

  ( λ (eq : (C.Obj , C.HOM)  (D.Obj , D.HOM)) 
     subst _ eq ((λ {_}  C.id) , λ {_ _ _}  C._∙_) 
     ((λ {_}  D.id) , λ {_ _ _}  D._∙_))                               ↝⟨ Bijection.Σ-≡,≡↔≡ 

  ((C.Obj , C.HOM) ,  {_}  C.id) , λ {_ _ _}  C._∙_) 
  ((D.Obj , D.HOM) ,  {_}  D.id) , λ {_ _ _}  D._∙_)                 ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ Σ-assoc) 

  (C.Obj , C.HOM ,  {_}  C.id) , λ {_ _ _}  C._∙_) 
  (D.Obj , D.HOM ,  {_}  D.id) , λ {_ _ _}  D._∙_)                   ↝⟨ ignore-propositional-component (
                                                                              ×-closure 1 (implicit-Π-closure ext₁₁₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₁₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₂₂ 1 λ _ 
                                                                                           D.Hom-is-set _ _) $
                                                                              ×-closure 1 (implicit-Π-closure ext₁₁₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₁₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₂₂ 1 λ _ 
                                                                                           D.Hom-is-set _ _)
                                                                                          (implicit-Π-closure ext₁₁₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₁₁₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₁₁₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₁₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₂₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₂₂ 1 λ _ 
                                                                                           implicit-Π-closure ext₂₂ 1 λ _ 
                                                                                           D.Hom-is-set _ _)) 
  ((C.Obj , C.HOM ,  {_}  C.id) , λ {_ _ _}  C._∙_) , _) 
  ((D.Obj , D.HOM ,  {_}  D.id) , λ {_ _ _}  D._∙_) , _)             ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ rearrange) ⟩□

  C  D                                                                  
  where
  module C = Precategory (record { precategory = C })
  module D = Precategory (record { precategory = D })

  ext₁₁₂₊ : Extensionality ℓ₁ (ℓ₁  lsuc ℓ₂)
  ext₁₁₂₊ = lower-extensionality ℓ₂ lzero ext

  ext₁₁₂ : Extensionality ℓ₁ (ℓ₁  ℓ₂)
  ext₁₁₂ = lower-extensionality ℓ₂ (lsuc ℓ₂) ext

  ext₁₂₊ : Extensionality ℓ₁ (lsuc ℓ₂)
  ext₁₂₊ = lower-extensionality ℓ₂ ℓ₁ ext

  ext₁₂ : Extensionality ℓ₁ ℓ₂
  ext₁₂ = lower-extensionality ℓ₂ _ ext

  ext₂₂ : Extensionality ℓ₂ ℓ₂
  ext₂₂ = lower-extensionality ℓ₁ _ ext

  rearrange :
     {a b c d e}
      {A : Set a} {B : A  Set b} {C : (a : A)  B a  Set c}
      {D : (a : A) (b : B a)  C a b  Set d}
      {E : (a : A) (b : B a) (c : C a b)  D a b c  Set e} 
    ( λ (a : A)   λ (b : B a)   λ (c : C a b)   λ (d : D a b c) 
       E a b c d)
      
    ( λ (p :  λ (a : A)   λ (b : B a)   λ (c : C a b)  D a b c) 
       E (proj₁ p) (proj₁ (proj₂ p)) (proj₁ (proj₂ (proj₂ p)))
         (proj₂ (proj₂ (proj₂ p))))
  rearrange {A = A} {B} {C} {D} {E} =
    ( λ (a : A)   λ (b : B a)   λ (c : C a b)   λ (d : D a b c) 
       E a b c d)                                                         ↝⟨ ∃-cong  _  ∃-cong λ _  Σ-assoc) 

    ( λ (a : A)   λ (b : B a)   λ (p :  λ (c : C a b)  D a b c) 
       E a b (proj₁ p) (proj₂ p))                                         ↝⟨ ∃-cong  _  Σ-assoc) 

    ( λ (a : A)   λ (p :  λ (b : B a)   λ (c : C a b)  D a b c) 
       E a (proj₁ p) (proj₁ (proj₂ p)) (proj₂ (proj₂ p)))                 ↝⟨ Σ-assoc ⟩□

    ( λ (p :  λ (a : A)   λ (b : B a)   λ (c : C a b)  D a b c) 
       E (proj₁ p) (proj₁ (proj₂ p)) (proj₁ (proj₂ (proj₂ p)))
         (proj₂ (proj₂ (proj₂ p))))                                       

  ≡⇒←-subst :
    {C D : Set ℓ₁} {H : C  C  SET ℓ₂}
    (eqO : C  D) 
     X Y  H (≡⇒← eqO X) (≡⇒← eqO Y))
      
    subst  Obj  Obj  Obj  SET _) eqO H
  ≡⇒←-subst {C} {H = H} eqO =
    elim¹  eqO   X Y  H (≡⇒← eqO X) (≡⇒← eqO Y)) 
                   subst  Obj  Obj  Obj  SET _) eqO H)
          ((λ X Y  H (≡⇒← (refl C) X) (≡⇒← (refl C) Y))  ≡⟨ cong  f X Y  H (f X) (f Y)) ≡⇒←-refl 
           H                                              ≡⟨ sym $ subst-refl _ _ ⟩∎
           subst  Obj  Obj  Obj  SET _) (refl C) H   )
          eqO

  ≡⇒←-subst-refl : {C : Set ℓ₁} {H : C  C  SET ℓ₂}  _
  ≡⇒←-subst-refl {C} {H} =
    ≡⇒←-subst {H = H} (refl C)                       ≡⟨ elim¹-refl _ _ ⟩∎

    trans (cong  f X Y  H (f X) (f Y)) ≡⇒←-refl)
          (sym $ subst-refl _ _)                     

  HOM-lemma :
    (eqO : C.Obj  D.Obj) 
    ((λ X Y  C.HOM (≡⇒← eqO X) (≡⇒← eqO Y))  D.HOM)
      
    (subst  Obj  Obj  Obj  SET _) eqO C.HOM  D.HOM)
  HOM-lemma eqO = cong (_≡ _) (≡⇒←-subst eqO)

  ≡⇒→-lemma :
     {eqO eqH X Y} {f : C.Hom (≡⇒← eqO X) (≡⇒← eqO Y)}  _
  ≡⇒→-lemma {eqO} {eqH} {X} {Y} {f} =
    ≡⇒→ (cong  H  Type (H X Y)) (≡⇒← (HOM-lemma eqO) eqH)) f  ≡⟨ sym $ subst-in-terms-of-≡⇒↝ equivalence
                                                                            (≡⇒← (HOM-lemma eqO) eqH)  H  Type (H X Y)) _ 
    subst  H  Type (H X Y)) (≡⇒← (HOM-lemma eqO) eqH) f       ≡⟨ cong  eq  subst  H  Type (H X Y)) eq _) $ sym $
                                                                      subst-in-terms-of-inverse∘≡⇒↝ equivalence (≡⇒←-subst eqO) (_≡ _) _ 
    subst  H  Type (H X Y))
      (subst (_≡ _) (sym $ ≡⇒←-subst eqO) eqH) f                 ≡⟨ cong  eq  subst  H  Type (H X Y)) eq _) $
                                                                      subst-trans (≡⇒←-subst eqO) 
    subst  H  Type (H X Y)) (trans (≡⇒←-subst eqO) eqH) f     ≡⟨ sym $ subst-subst _ _ _ _ ⟩∎

    subst  H  Type (H X Y)) eqH
      (subst  H  Type (H X Y)) (≡⇒←-subst eqO) f)             

  ≡⇒←-lemma :  {eqO eqH X Y} {f : D.Hom X Y}  _
  ≡⇒←-lemma {eqO} {eqH} {X} {Y} {f} =
    ≡⇒← (cong  H  Type (H X Y)) (≡⇒← (HOM-lemma eqO) eqH)) f           ≡⟨ sym $ subst-in-terms-of-inverse∘≡⇒↝ equivalence
                                                                                     (≡⇒← (HOM-lemma eqO) eqH)  H  Type (H X Y)) _ 
    subst  H  Type (H X Y)) (sym $ ≡⇒← (HOM-lemma eqO) eqH) f          ≡⟨ cong  eq  subst  H  Type (H X Y)) (sym eq) _) $ sym $
                                                                               subst-in-terms-of-inverse∘≡⇒↝ equivalence (≡⇒←-subst eqO) (_≡ _) _ 
    subst  H  Type (H X Y))
      (sym $ subst (_≡ _) (sym $ ≡⇒←-subst eqO) eqH) f                    ≡⟨ cong  eq  subst  H  Type (H X Y)) (sym eq) _) $
                                                                               subst-trans (≡⇒←-subst eqO) 
    subst  H  Type (H X Y)) (sym $ trans (≡⇒←-subst eqO) eqH) f        ≡⟨ cong  eq  subst  H  Type (H X Y)) eq _) $
                                                                               sym-trans (≡⇒←-subst eqO) eqH 
    subst  H  Type (H X Y)) (trans (sym eqH) (sym $ ≡⇒←-subst eqO)) f  ≡⟨ sym $ subst-subst _ _ _ _ ⟩∎

    subst  H  Type (H X Y)) (sym $ ≡⇒←-subst eqO)
      (subst  H  Type (H X Y)) (sym eqH) f)                            

  expand-≡⇒←-subst :
     {C : Set ℓ₁} {X Y}
      {F G : C  C  SET ℓ₂}
      {eqH : subst  Obj  Obj  Obj  SET ℓ₂) (refl C) F  G}
      {f : Type (F (≡⇒← (refl C) X) (≡⇒← (refl C) Y))} 
    _
  expand-≡⇒←-subst {C} {X} {Y} {F} {eqH = eqH} {f} =
    subst  H  Type (H X Y)) eqH
      (subst  H  Type (H X Y)) (≡⇒←-subst (refl C)) f)   ≡⟨ cong  eq  subst  H  Type (H X Y)) eqH $ subst  H  Type (H X Y)) eq f)
                                                                 ≡⇒←-subst-refl 
    subst  H  Type (H X Y)) eqH
      (subst  H  Type (H X Y))
         (trans (cong  f X Y  F (f X) (f Y)) ≡⇒←-refl)
                (sym $ subst-refl _ _))
         f)                                                 ≡⟨ cong (subst  H  Type (H X Y)) eqH) $ sym $
                                                                 subst-subst _ _ _ _ 
    subst  H  Type (H X Y)) eqH
      (subst  H  Type (H X Y))
         (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
         (subst  H  Type (H X Y))
                (cong  f X Y  F (f X) (f Y)) ≡⇒←-refl)
                f))                                         ≡⟨ cong  f  subst  H  Type (H X Y)) eqH $
                                                                             subst  H  Type (H X Y))
                                                                               (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _) f) $ sym $
                                                                 subst-∘  H  Type (H X Y))  f X Y  F (f X) (f Y)) ≡⇒←-refl ⟩∎
    subst  H  Type (H X Y)) eqH
      (subst  H  Type (H X Y))
         (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
         (subst  f  Type (F (f X) (f Y))) ≡⇒←-refl f))   

  expand-sym-≡⇒←-subst :
     {C : Set ℓ₁} {X Y}
      {F G : C  C  SET ℓ₂}
      {eqH : subst  Obj  Obj  Obj  SET ℓ₂) (refl C) F  G}
      {f : Type (G X Y)} 
    _
  expand-sym-≡⇒←-subst {C} {X} {Y} {F} {eqH = eqH} {f} =
     subst  H  Type (H X Y)) (sym $ ≡⇒←-subst (refl C))
       (subst  H  Type (H X Y)) (sym eqH) f)                ≡⟨ cong  eq  subst  H  Type (H X Y)) (sym eq) $
                                                                                 subst  H  Type (H X Y)) (sym eqH) f)
                                                                    ≡⇒←-subst-refl 
     subst  H  Type (H X Y))
       (sym $ trans (cong  f X Y  F (f X) (f Y)) ≡⇒←-refl)
                    (sym $ subst-refl _ _))
       (subst  H  Type (H X Y)) (sym eqH) f)                ≡⟨ cong  eq  subst  H  Type (H X Y)) eq $
                                                                                 subst  H  Type (H X Y)) (sym eqH) f) $
                                                                    sym-trans (cong  f X Y  F (f X) (f Y)) ≡⇒←-refl) _ 
     subst  H  Type (H X Y))
       (trans (sym $ sym $
                 subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
              (sym $ cong  f X Y  F (f X) (f Y))
                          ≡⇒←-refl))
       (subst  H  Type (H X Y)) (sym eqH) f)                ≡⟨ cong  eq  subst  H  Type (H X Y))
                                                                                 (trans eq (sym $ cong  f X Y  F (f X) (f Y)) ≡⇒←-refl)) $
                                                                                 subst  H  Type (H X Y)) (sym eqH) f) $
                                                                    sym-sym _ 
     subst  H  Type (H X Y))
       (trans (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
              (sym $ cong  f X Y  F (f X) (f Y))
                          ≡⇒←-refl))
       (subst  H  Type (H X Y)) (sym eqH) f)                ≡⟨ sym $ subst-subst _ _ _ _ 

     subst  H  Type (H X Y))
       (sym $ cong  f X Y  F (f X) (f Y)) ≡⇒←-refl)
       (subst  H  Type (H X Y))
          (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
          (subst  H  Type (H X Y)) (sym eqH) f))            ≡⟨ cong  eq  subst  H  Type (H X Y)) eq $
                                                                                 subst  H  Type (H X Y))
                                                                                       (subst-refl  Obj  Obj  Obj  SET ℓ₂) _) $
                                                                                   subst  H  Type (H X Y)) (sym eqH) f) $ sym $
                                                                    cong-sym  f X Y  F (f X) (f Y)) ≡⇒←-refl 
     subst  H  Type (H X Y))
       (cong  f X Y  F (f X) (f Y)) $ sym ≡⇒←-refl)
       (subst  H  Type (H X Y))
          (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
          (subst  H  Type (H X Y)) (sym eqH) f))            ≡⟨ sym $ subst-∘ _ _ _ ⟩∎

     subst  f  Type (F (f X) (f Y))) (sym ≡⇒←-refl)
       (subst  H  Type (H X Y))
          (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
          (subst  H  Type (H X Y)) (sym eqH) f))            

  subst-Σ-≡,≡→≡ :
     {C : Set ℓ₁}
      {F G : C  C  SET ℓ₂}
      {eqH : subst  Obj  Obj  Obj  SET ℓ₂) (refl C) F  G}
      {P : (Obj : Set ℓ₁) (HOM : Obj  Obj  SET ℓ₂)  Set (ℓ₁  ℓ₂)} 
    _
  subst-Σ-≡,≡→≡ {C} {F} {eqH = eqH} {P} =
    subst (P C) eqH 
    subst (P C) (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) F)       ≡⟨ lower-extensionality lzero (lsuc ℓ₂) ext  _ 
                                                                             subst-subst (P C) _ _ _) 
    subst (P C) (trans (sym $ subst-refl _ _) eqH)                      ≡⟨ lower-extensionality lzero (lsuc ℓ₂) ext  _ 
                                                                             subst-∘ (uncurry P) (C ,_) _) 
    subst (uncurry P) (cong (C ,_) (trans (sym $ subst-refl _ _) eqH))  ≡⟨ cong (subst (uncurry P)) $ sym $ Σ-≡,≡→≡-reflˡ eqH ⟩∎

    subst (uncurry P) (Σ-≡,≡→≡ (refl C) eqH)                            

  P = λ Obj (HOM : Obj  Obj  SET _) 
         {X}  Type (HOM X X)

  abstract

    P-lemma :
       {eqO eqH X} 
      ≡⇒→ (cong  H  Type (H X X)) (≡⇒← (HOM-lemma eqO) eqH)) C.id 
      subst₂ (uncurry P) eqO eqH C.id {X = X}
    P-lemma {eqO} {eqH} {X} =
      ≡⇒→ (cong  H  Type (H X X)) (≡⇒← (HOM-lemma eqO) eqH)) C.id  ≡⟨ ≡⇒→-lemma 

      subst  H  Type (H X X)) eqH
        (subst  H  Type (H X X)) (≡⇒←-subst eqO)
               (C.id {X = ≡⇒← eqO X}))                                ≡⟨ elim
                                                                            eqO 
                                                                                     {X F G}
                                                                                    (eqH : subst  Obj  Obj  Obj  SET ℓ₂) eqO F  G)
                                                                                    (id :  X  Type (F X X)) 
                                                                              subst  H  Type (H X X)) eqH
                                                                                (subst  H  Type (H X X)) (≡⇒←-subst eqO) (id (≡⇒← eqO X)))
                                                                                
                                                                              subst (uncurry P) (Σ-≡,≡→≡ eqO eqH)  {X}  id X))
                                                                            C {X F G} eqH id 
          subst  H  Type (H X X)) eqH
            (subst  H  Type (H X X)) (≡⇒←-subst (refl C))
                   (id (≡⇒← (refl C) X)))                                     ≡⟨ expand-≡⇒←-subst 

          subst  H  Type (H X X)) eqH
            (subst
                H  Type (H X X))
               (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
               (subst  f  Type (F (f X) (f X)))
                      ≡⇒←-refl
                      (id (≡⇒← (refl C) X))))                                 ≡⟨ cong  f  subst  H  Type (H X X)) eqH
                                                                                               (subst
                                                                                                   H  Type (H X X))
                                                                                                  (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                                                                                                  f)) $
                                                                                   dependent-cong  f  id (f X)) ≡⇒←-refl 
          subst  H  Type (H X X)) eqH
            (subst  H  Type (H X X))
                   (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) F)
                   (id X))                                                    ≡⟨ cong (subst  H  Type (H X X)) eqH) $
                                                                                   push-subst-implicit-application _ _ 
          subst  H  Type (H X X)) eqH
            (subst (P C)
                   (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) F)
                    {X}  id X) {X = X})                                    ≡⟨ push-subst-implicit-application _ _ 

          subst (P C) eqH
            (subst (P C)
                   (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) F)
                    {X}  id X)) {X = X}                                    ≡⟨ cong  (f : P C F  P C G)  f _)
                                                                                   subst-Σ-≡,≡→≡ ⟩∎
          subst (uncurry P) (Σ-≡,≡→≡ (refl C) eqH)  {X}  id X)             )
                                                                           eqO eqH  _  C.id) 
      subst (uncurry P) (Σ-≡,≡→≡ eqO eqH)
             {X}  C.id {X = X}) {X = X}                            ≡⟨⟩

      subst₂ (uncurry P) eqO eqH C.id                                 

  Q = λ Obj (HOM : Obj  Obj  SET _) 
         {X Y Z}  Type (HOM Y Z)  Type (HOM X Y)  Type (HOM X Z)

  push-Q :
    {C : Set ℓ₁} {X Y Z : C} {F G : C  C  SET ℓ₂}
    {c : (X Y Z : C)  Type (F Y Z)  Type (F X Y)  Type (F X Z)}
    {F≡G : F  G} {f : Type (G Y Z)} {g : Type (G X Y)} 
    subst  H  Type (H X Z)) F≡G
      (c X Y Z
         (subst  H  Type (H Y Z)) (sym F≡G) f)
         (subst  H  Type (H X Y)) (sym F≡G) g)) 
    subst (Q C) F≡G (c _ _ _) f g
  push-Q {C} {X} {Y} {Z} {c = c} {F≡G} {f} {g} =
    subst  H  Type (H X Z)) F≡G
      (c X Y Z (subst  H  Type (H Y Z)) (sym F≡G) f)
               (subst  H  Type (H X Y)) (sym F≡G) g))                ≡⟨ sym subst-→ 

    subst  H  Type (H X Y)  Type (H X Z)) F≡G
      (c X Y Z (subst  H  Type (H Y Z)) (sym F≡G) f)) g              ≡⟨ cong (_$ g) $ sym subst-→ 

    subst  H  Type (H Y Z)  Type (H X Y)  Type (H X Z)) F≡G
      (c X Y Z) f g                                                     ≡⟨ cong  h  h f g) $
                                                                             push-subst-implicit-application _
                                                                                H Z  Type (H Y Z)  Type (H X Y)  Type (H X Z)) 
    subst  H   {Z}  Type (H Y Z)  Type (H X Y)  Type (H X Z))
      F≡G (c X Y _) f g                                                 ≡⟨ cong  h  h {Z = Z} f g) $
                                                                             push-subst-implicit-application F≡G
                                                                                H Y   {Z}  Type (H Y Z)  Type (H X Y)  Type (H X Z)) 
    subst  H   {Y Z}  Type (H Y Z)  Type (H X Y)  Type (H X Z))
      F≡G (c X _ _) f g                                                 ≡⟨ cong  h  h {Y = Y} {Z = Z} f g) $
                                                                             push-subst-implicit-application F≡G
                                                                                H X   {Y Z}  Type (H Y Z)  Type (H X Y)  Type (H X Z)) ⟩∎
    subst (Q C) F≡G (c _ _ _) f g                                       

  abstract

    Q-lemma :
       {eqO eqH X Y Z f g} 
      let eqH′ = λ X Y 
                   cong  H  Type (H X Y)) (≡⇒← (HOM-lemma eqO) eqH)
      in
      ≡⇒→ (eqH′ X Z) (≡⇒← (eqH′ Y Z) f C.∙ ≡⇒← (eqH′ X Y) g) 
      subst₂ (uncurry Q) eqO eqH C._∙_ f g
    Q-lemma {eqO} {eqH} {X} {Y} {Z} {f} {g} =

      let eqH′ = λ X Y 
                   cong  F  Type (F X Y)) (≡⇒← (HOM-lemma eqO) eqH)
      in

      ≡⇒→ (eqH′ X Z) (≡⇒← (eqH′ Y Z) f C.∙ ≡⇒← (eqH′ X Y) g)              ≡⟨ cong₂  f g  ≡⇒→ (eqH′ X Z) (f C.∙ g))
                                                                               ≡⇒←-lemma
                                                                               ≡⇒←-lemma 
      ≡⇒→ (eqH′ X Z)
        (subst  H  Type (H Y Z)) (sym $ ≡⇒←-subst eqO)
           (subst  H  Type (H Y Z)) (sym eqH) f)
           C.∙
         subst  H  Type (H X Y)) (sym $ ≡⇒←-subst eqO)
           (subst  H  Type (H X Y)) (sym eqH) g))                      ≡⟨ ≡⇒→-lemma 

      subst  H  Type (H X Z)) eqH
        (subst  H  Type (H X Z)) (≡⇒←-subst eqO)
           (subst  H  Type (H Y Z)) (sym $ ≡⇒←-subst eqO)
              (subst  H  Type (H Y Z)) (sym eqH) f)
              C.∙
            subst  H  Type (H X Y)) (sym $ ≡⇒←-subst eqO)
              (subst  H  Type (H X Y)) (sym eqH) g)))                  ≡⟨ elim
                                                                                eqO   {X Y Z F G}
                                                                                        (eqH : subst  Obj  Obj  Obj  SET ℓ₂) eqO F  G)
                                                                                        (comp :  X Y Z 
                                                                                                Type (F Y Z)  Type (F X Y)  Type (F X Z))
                                                                                        (f : Type (G Y Z)) (g : Type (G X Y)) 
                                                                                  subst  H  Type (H X Z)) eqH
                                                                                    (subst  H  Type (H X Z)) (≡⇒←-subst eqO)
                                                                                       (comp (≡⇒← eqO X) (≡⇒← eqO Y) (≡⇒← eqO Z)
                                                                                          (subst  H  Type (H Y Z)) (sym $ ≡⇒←-subst eqO)
                                                                                             (subst  H  Type (H Y Z)) (sym eqH) f))
                                                                                          (subst  H  Type (H X Y)) (sym $ ≡⇒←-subst eqO)
                                                                                             (subst  H  Type (H X Y)) (sym eqH) g))))
                                                                                    
                                                                                  subst (uncurry Q) (Σ-≡,≡→≡ eqO eqH)  {X Y Z}  comp X Y Z) f g)
                                                                                C {X Y Z F G} eqH comp f g 
          subst  H  Type (H X Z)) eqH
            (subst  H  Type (H X Z)) (≡⇒←-subst (refl C))
               (comp (≡⇒← (refl C) X) (≡⇒← (refl C) Y) (≡⇒← (refl C) Z)
                  (subst  H  Type (H Y Z)) (sym $ ≡⇒←-subst (refl C))
                     (subst  H  Type (H Y Z)) (sym eqH) f))
                  (subst  H  Type (H X Y)) (sym $ ≡⇒←-subst (refl C))
                     (subst  H  Type (H X Y)) (sym eqH) g))))                  ≡⟨ cong₂  f g 
                                                                                              subst  H  Type (H X Z)) eqH $
                                                                                                subst  H  Type (H X Z)) (≡⇒←-subst (refl C)) $
                                                                                                  comp (≡⇒← (refl C) X) (≡⇒← (refl C) Y)
                                                                                                       (≡⇒← (refl C) Z) f g)
                                                                                       expand-sym-≡⇒←-subst
                                                                                       expand-sym-≡⇒←-subst 
          subst  H  Type (H X Z)) eqH
            (subst  H  Type (H X Z)) (≡⇒←-subst (refl C))
               (comp (≡⇒← (refl C) X) (≡⇒← (refl C) Y) (≡⇒← (refl C) Z)
                  (subst  f  Type (F (f Y) (f Z))) (sym ≡⇒←-refl)
                     (subst  H  Type (H Y Z))
                        (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                        (subst  H  Type (H Y Z)) (sym eqH) f)))
                  (subst  f  Type (F (f X) (f Y))) (sym ≡⇒←-refl)
                     (subst  H  Type (H X Y))
                        (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                        (subst  H  Type (H X Y)) (sym eqH) g)))))              ≡⟨ expand-≡⇒←-subst 

          subst  H  Type (H X Z)) eqH
            (subst  H  Type (H X Z))
               (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
               (subst  f  Type (F (f X) (f Z))) ≡⇒←-refl
                  (comp (≡⇒← (refl C) X) (≡⇒← (refl C) Y)
                        (≡⇒← (refl C) Z)
                     (subst  f  Type (F (f Y) (f Z))) (sym ≡⇒←-refl)
                        (subst  H  Type (H Y Z))
                           (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                           (subst  H  Type (H Y Z)) (sym eqH) f)))
                     (subst  f  Type (F (f X) (f Y))) (sym ≡⇒←-refl)
                        (subst  H  Type (H X Y))
                           (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                           (subst  H  Type (H X Y)) (sym eqH) g))))))          ≡⟨ cong (subst  H  Type (H X Z)) eqH 
                                                                                           subst  H  Type (H X Z))
                                                                                             (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)) $
                                                                                       dependent-cong′
                                                                                          h eq 
                                                                                            comp (h X) (h Y) (h Z)
                                                                                              (subst  f  Type (F (f Y) (f Z))) (sym eq)
                                                                                                 (subst  H  Type (H Y Z))
                                                                                                    (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                                                                                                    (subst  H  Type (H Y Z)) (sym eqH) f)))
                                                                                              (subst  f  Type (F (f X) (f Y))) (sym eq)
                                                                                                 (subst  H  Type (H X Y))
                                                                                                    (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                                                                                                    (subst  H  Type (H X Y)) (sym eqH) g))))
                                                                                         _ 
          subst  H  Type (H X Z)) eqH
            (subst  H  Type (H X Z))
               (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
               (comp X Y Z
                  (subst  f  Type (F (f Y) (f Z))) (sym (refl P.id))
                     (subst  H  Type (H Y Z))
                        (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                        (subst  H  Type (H Y Z)) (sym eqH) f)))
                  (subst  f  Type (F (f X) (f Y))) (sym (refl P.id))
                     (subst  H  Type (H X Y))
                        (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                        (subst  H  Type (H X Y)) (sym eqH) g)))))              ≡⟨ cong₂  p q 
                                                                                       subst  H  Type (H X Z)) eqH
                                                                                         (subst  H  Type (H X Z))
                                                                                            (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                                                                                            (comp X Y Z
                                                                                               (subst  f  Type (F (f Y) (f Z))) p
                                                                                                  (subst  H  Type (H Y Z))
                                                                                                     (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                                                                                                     (subst  H  Type (H Y Z)) (sym eqH) f)))
                                                                                               (subst  f  Type (F (f X) (f Y))) q
                                                                                                  (subst  H  Type (H X Y))
                                                                                                     (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                                                                                                     (subst  H  Type (H X Y)) (sym eqH) g))))))
                                                                                       (sym-refl {x = P.id})
                                                                                       (sym-refl {x = P.id}) 
          subst  H  Type (H X Z)) eqH
            (subst  H  Type (H X Z))
               (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
               (comp X Y Z
                  (subst  f  Type (F (f Y) (f Z))) (refl P.id)
                     (subst  H  Type (H Y Z))
                        (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                        (subst  H  Type (H Y Z)) (sym eqH) f)))
                  (subst  f  Type (F (f X) (f Y))) (refl P.id)
                     (subst  H  Type (H X Y))
                        (subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                        (subst  H  Type (H X Y)) (sym eqH) g)))))              ≡⟨ cong₂  f g 
                                                                                              subst  H  Type (H X Z)) eqH
                                                                                                (subst  H  Type (H X Z))
                                                                                                   (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
                                                                                                   (comp X Y Z f g)))
                                                                                       (subst-refl _ _)
                                                                                       (subst-refl _ _) 
          subst  H  Type (H X Z)) eqH
            (subst  H  Type (H X Z))
               (sym $ subst-refl  Obj  Obj  Obj  SET ℓ₂) _)
               (comp X Y Z
                  (subst  H  Type (H Y Z))