{-# OPTIONS --postfix-projections --without-K #-}

open import Agda.Primitive
open import HoTT

record Equiv {i j} (A : Set i) (B : Set j) : Set (lsuc (i ⊔ j)) where
  field
    equiv-rel : A → B → Set (i ⊔ j)
    equiv-fun→ : ∀ a → is-contr (Σ B λ b → equiv-rel a b)
    equiv-fun← : ∀ b → is-contr (Σ A λ a → equiv-rel a b)
open Equiv

record IsRefl {i} {A : Set i} (Aₑ : Equiv A A) : Set (lsuc i) where
  field
    refl-rel   : ∀ a → Aₑ .equiv-rel a a → Set i
    refl-contr : ∀ a → is-contr (Σ _ (refl-rel a))
open IsRefl

--------------------------------------------------------------------------------

Equiv-Id : ∀ {i} (A : Set i) → Equiv A A
Equiv-Id A .equiv-rel x y = Id x y
Equiv-Id A .equiv-fun→ a = is-contr-path-from
Equiv-Id A .equiv-fun← b = is-contr-path-to

IsRefl-Id : ∀ {i} (A : Set i) → IsRefl (Equiv-Id A)
IsRefl-Id A .refl-rel a p = Id p refl
IsRefl-Id A .refl-contr a = is-contr-path-to

--------------------------------------------------------------------------------

DepEquiv : ∀ {i j} {Γ₁ Γ₂ : Set i} (Γₑ : Equiv Γ₁ Γ₂) (A₁ : Γ₁ → Set j) (A₂ : Γ₂ → Set j) → Set (i ⊔ lsuc j)
DepEquiv Γₑ A₁ A₂ = ∀ {γ₁} {γ₂} (γₑ : Γₑ .equiv-rel γ₁ γ₂) → Equiv (A₁ γ₁) (A₂ γ₂)

DepIsRefl : ∀ {i j} {Γ Γₑ} (Γᵣ : IsRefl {i} {Γ} Γₑ) {A : Γ → Set j} (Aₑ : DepEquiv Γₑ A A) → Set (i ⊔ lsuc j)
DepIsRefl Γᵣ Aₑ = ∀ {γ} {γₑ} (γᵣ : Γᵣ .refl-rel γ γₑ) → IsRefl (Aₑ γₑ)

Equiv→is-equiv : ∀ {i j} {A : Set i} {B : Set j} (E : Equiv A B)
                   (f : A → B) (f-graph : ∀ a → E .equiv-rel a (f a))
                 → is-equiv f
Equiv→is-equiv E f f-graph b
  = is-contr-retract
    (λ { (a , e) → a , ap fst (is-contr-all-paths (E .equiv-fun→ a) (f a , f-graph a) (b , e)) })
    (λ { (a , refl) → a , f-graph _ })
    (λ { (a , refl) → pair-Id refl (ap (ap _) (is-contr-all-paths-β _)) })
    (E .equiv-fun← b)

Equiv-graph : ∀ {i} {A : Set i} {B : Set i} 
                (f : A → B) (f-equiv : is-equiv f)
              → Equiv A B
Equiv-graph f f-equiv .equiv-rel a b = Id (f a) b
Equiv-graph f f-equiv .equiv-fun→ a = is-contr-path-from
Equiv-graph f f-equiv .equiv-fun← b = f-equiv _

Equiv-between-contr : ∀ {i} {A : Set i} {B : Set i} → is-contr A → is-contr B → Equiv A B
Equiv-between-contr cA cB .equiv-rel _ _ = ⊤
Equiv-between-contr cA cB .equiv-fun→ _ = is-contr-Σ cB λ _ → is-contr-⊤
Equiv-between-contr cA cB .equiv-fun← _ = is-contr-Σ cA λ _ → is-contr-⊤

module _ {i} {A : Set i} {B : Set i} (pA : is-prop A) (pB : is-prop B) (f : A → B) (g : B → A) where
  Equiv-between-prop : Equiv A B
  Equiv-between-prop .equiv-rel _ _ = ⊤
  Equiv-between-prop .equiv-fun→ a = is-contr-Σ (pB (f a)) λ _ → is-contr-⊤
  Equiv-between-prop .equiv-fun← b = is-contr-Σ (pA (g b)) λ _ → is-contr-⊤

--------------------------------------------------------------------------------

module _ {i} {j}
  {A₁ A₂ : Set i} (Aₑ : Equiv A₁ A₂)
  {B₁ B₂} (Bₑ : DepEquiv {i} {j} Aₑ B₁ B₂)
  where

  Σ-Equiv : Equiv {i ⊔ j} (Σ A₁ B₁) (Σ A₂ B₂)
  Σ-Equiv .equiv-rel (a₁ , b₁) (a₂ , b₂) = Σ (Aₑ .equiv-rel a₁ a₂) (λ aₑ → Bₑ aₑ .equiv-rel b₁ b₂)
  Σ-Equiv .equiv-fun→ _ = is-contr-ΣΣ (Aₑ .equiv-fun→ _) λ _ _ → Bₑ _ .equiv-fun→ _
  Σ-Equiv .equiv-fun← _ = is-contr-ΣΣ (Aₑ .equiv-fun← _) λ _ _ → Bₑ _ .equiv-fun← _

  module _ {p₁ p₂} (pₑ : Σ-Equiv .equiv-rel p₁ p₂) where
    fst-Equiv : Aₑ .equiv-rel (fst p₁) (fst p₂)
    fst-Equiv = fst pₑ

    snd-Equiv : Bₑ fst-Equiv .equiv-rel (snd p₁) (snd p₂)
    snd-Equiv = snd pₑ

  module _
    {a₁ a₂} (aₑ : Aₑ .equiv-rel a₁ a₂)
    {b₁ b₂} (bₑ : Bₑ aₑ .equiv-rel b₁ b₂)
    where

    pair-Equiv : Σ-Equiv .equiv-rel (a₁ , b₁) (a₂ , b₂)
    pair-Equiv = aₑ , bₑ

--------------------------------------------------------------------------------

module _ {i} {j}
  {A : Set i} {Aₑ : Equiv A A} (Aᵣ : IsRefl Aₑ)
  {B} {Bₑ : DepEquiv {i} {j} Aₑ B B} (Bᵣ : ∀ {a aₑ} (aᵣ : Aᵣ .refl-rel a aₑ) → IsRefl (Bₑ aₑ))
  where

  Σ-IsRefl : IsRefl (Σ-Equiv Aₑ Bₑ)
  Σ-IsRefl .refl-rel (a , b) (aₑ , bₑ) = Σ (Aᵣ .refl-rel a aₑ) λ aᵣ → Bᵣ aᵣ .refl-rel b bₑ
  Σ-IsRefl .refl-contr (a , b)
    = is-contr-ΣΣ (Aᵣ .refl-contr a) (λ _ _ → Bᵣ _ .refl-contr _)

  module _ {p pₑ} (pᵣ : Σ-IsRefl .refl-rel p pₑ) where
    fst-IsRefl : Aᵣ .refl-rel (fst p) (fst-Equiv Aₑ Bₑ pₑ)
    fst-IsRefl = fst pᵣ

    snd-IsRefl : Bᵣ fst-IsRefl .refl-rel (snd p) (snd-Equiv Aₑ Bₑ pₑ)
    snd-IsRefl = snd pᵣ

  module _
    {a aₑ} (aᵣ : Aᵣ .refl-rel a aₑ)
    {b bₑ} (bᵣ : Bᵣ aᵣ .refl-rel b bₑ)
    where

    pair-IsRefl : Σ-IsRefl .refl-rel (a , b) (pair-Equiv Aₑ Bₑ aₑ bₑ)
    pair-IsRefl = aᵣ , bᵣ

--------------------------------------------------------------------------------

module _ {i j k} {A : Set i} {B : A → Set j} {C : A → Set k} (g : ∀ a → B a → C a) where
  total : Σ A B → Σ A C
  total (a , b) = a , g a b
 
module _ {i j} {A : Set i} {B : A → Set j} {C : A → Set j} (g : ∀ a → B a → C a) where
 
  equiv-total : (∀ a → is-equiv (g a)) → is-equiv (total g)
  equiv-total g-equiv
    = Equiv→is-equiv
      (Σ-Equiv (Equiv-Id _) λ { refl → Equiv-graph (g _) (g-equiv _) })
      (total g)
      (λ { (a , b) → refl , refl })

equiv-total-contr : ∀ {i} {A : Set i} {B : A → Set i} {C : A → Set i} → (∀ a → is-contr (B a)) → (∀ a → is-contr (C a))
               → (g : ∀ a → B a → C a)
               → is-equiv {A = Σ A B} {B = Σ A C} λ p → _ , g _ (p .snd)
equiv-total-contr cB cC g
  = Equiv→is-equiv
    (Σ-Equiv (Equiv-Id _) λ { refl → Equiv-between-contr (cB _) (cC _) })
    (λ { (a , b) → (a , g a b) })
    (λ { (a , b) → refl , tt })

--------------------------------------------------------------------------------

module _ {i} {j}
  {A₁ A₂ : Set i} (Aₑ : Equiv A₁ A₂)
  {B₁ B₂} (Bₑ : DepEquiv {i} {j} Aₑ B₁ B₂)
  where

  Π-Equiv : Equiv (∀ a₁ → B₁ a₁) (∀ a₂ → B₂ a₂)
  Π-Equiv .equiv-rel
    = λ f₁ f₂ → ∀ {a₁} {a₂} (aₑ : Aₑ .equiv-rel a₁ a₂) → Bₑ aₑ .equiv-rel (f₁ a₁) (f₂ a₂) 
  Π-Equiv .equiv-fun→ f₁
    = is-contr-retract
        {A = Σ (∀ a₂ → B₂ a₂) λ f₂ → (a : Σ _ λ a₂ → Σ _ λ a₁ → Aₑ .equiv-rel a₁ a₂) → Bₑ (a .snd .snd) .equiv-rel (f₁ _) (f₂ _)}
        (λ { (f₂ , fₑ) → f₂ , λ aₑ → fₑ (_ , (_ , aₑ)) })
        (λ { (f₂ , fₑ) → f₂ , λ a → fₑ (a .snd .snd) })
        (λ _ → refl)
        (is-contr-ΣΠ
          {B = B₂}
          (λ { (a₂ , (_ , _)) → a₂ })
          (fst-equiv (Aₑ .equiv-fun←))
          {D = λ a b₂ → Bₑ (a .snd .snd) .equiv-rel _ b₂}
          (λ a → Bₑ (a .snd .snd) .equiv-fun→ _))
  Π-Equiv .equiv-fun← f₂
    = is-contr-retract
        {A = Σ (∀ a₁ → B₁ a₁) λ f₁ → (a : Σ _ λ a₁ → Σ _ λ a₂ → Aₑ .equiv-rel a₁ a₂) → Bₑ (a .snd .snd) .equiv-rel (f₁ _) (f₂ _)}
        (λ { (f₁ , fₑ) → f₁ , λ aₑ → fₑ (_ , (_ , aₑ)) })
        (λ { (f₁ , fₑ) → f₁ , λ a → fₑ (a .snd .snd) })
        (λ _ → refl)
        (is-contr-ΣΠ
          {B = B₁}
          (λ { (a₁ , (_ , _)) → a₁ })
          (fst-equiv (Aₑ .equiv-fun→))
          {D = λ a b₁ → Bₑ (a .snd .snd) .equiv-rel b₁ _}
          (λ a → Bₑ (a .snd .snd) .equiv-fun← _))

--------------------------------------------------------------------------------

module _ {i} {j}
  {A : Set i} (Aₑ : Equiv A A) (Aᵣ : IsRefl Aₑ)
  {B} (Bₑ : DepEquiv {i} {j} Aₑ B B) (Bᵣ : ∀ {a aₑ} (aᵣ : Aᵣ .refl-rel a aₑ) → IsRefl (Bₑ aₑ))
  where

  Π-IsRefl : IsRefl (Π-Equiv Aₑ Bₑ)
  Π-IsRefl .refl-rel f fₑ = ∀ {a aₑ} (aᵣ : Aᵣ .refl-rel a aₑ) → Bᵣ aᵣ .refl-rel (f a) (fₑ aₑ)
  Π-IsRefl .refl-contr f
    = is-contr-retract
        {A = Σ ((a : Σ _ λ a₁ → Σ _ λ a₂ → Aₑ .equiv-rel a₁ a₂) → Bₑ (a .snd .snd) .equiv-rel (f (a .fst)) (f (a .snd .fst))) λ fₑ →
             (a : Σ _ λ a → Σ _ λ aₑ → Aᵣ .refl-rel a aₑ) → Bᵣ (a .snd .snd) .refl-rel (f _) (fₑ _)}
        (λ { (fₑ , fᵣ) → (λ aₑ → fₑ (_ , _ , aₑ)) , λ aᵣ → fᵣ (_ , _ , aᵣ) })
        (λ { (fₑ , fᵣ) → (λ a → fₑ (a .snd .snd)) , (λ a → fᵣ (a .snd .snd)) })
        (λ _ → refl)
        (is-contr-ΣΠ
         {A = Σ A (λ a₁ → Σ A (Aₑ .equiv-rel a₁))}
         {B = λ z → Bₑ (z .snd .snd) .equiv-rel (f (z .fst)) (f (z .snd .fst))}
         {C = Σ A (λ a → Σ (Aₑ .equiv-rel a a) (Aᵣ .refl-rel a))}
         (λ { (a , aₑ , aᵣ) → a , a , aₑ })
         (equiv-total-contr (λ _ → Aᵣ .refl-contr _) (λ _ → Aₑ .equiv-fun→ _) _)
         {D = λ a x → Bᵣ (a .snd .snd) .refl-rel _ x}
         (λ _ → Bᵣ _ .refl-contr _))

--------------------------------------------------------------------------------

module _ {i}
  {A₁ A₂ : Set i} (Aₑ : Equiv A₁ A₂)
  {B₁ B₂} (Bₑ : DepEquiv Aₑ B₁ B₂)
  where

  shape : W A₁ B₁ → W A₂ B₂ → Set i
  shape (sup a₁ f₁) (sup a₂ f₂) = Aₑ .equiv-rel a₁ a₂
  
  pos : ∀ x₁ x₂ → shape x₁ x₂ → Set i
  pos (sup a₁ f₁) (sup a₂ f₂) aₑ = Σ _ λ b₁ → Σ _ λ b₂ → Bₑ aₑ .equiv-rel b₁ b₂ 

  color : ∀ x₁ x₂ → (aₑ : shape x₁ x₂) → pos x₁ x₂ aₑ → W A₁ B₁ × W A₂ B₂
  color (sup a₁ f₁) (sup a₂ f₂) aₑ (b₁ , (b₂ , bₑ)) = f₁ b₁ , f₂ b₂

  W-Equiv-rel : W A₁ B₁ → W A₂ B₂ → Set i
  W-Equiv-rel x₁ x₂
    = IW (W A₁ B₁ × W A₂ B₂)
         (λ { (x₁ , x₂) → shape x₁ x₂ })
         (λ { {x₁ , x₂} aₑ → pos x₁ x₂ aₑ })
         (λ { {x₁ , x₂} {aₑ} b → color x₁ x₂ aₑ b })
         (x₁ , x₂)

  abstract
    W-Equiv-fun→ : ∀ x → is-contr (Σ _ λ y → W-Equiv-rel x y)
    W-Equiv-fun→ (sup a₁ f₁)
      = let g = λ b → W-Equiv-fun→ (f₁ b) in
        is-contr-retract
          {A = Σ (Σ A₂ λ a₂ → B₂ a₂ → W A₂ B₂) λ { (a₂ , f₂) → Σ (Aₑ .equiv-rel a₁ a₂) λ aₑ → (b : Σ _ λ b₁ → Σ _ λ b₂ → Bₑ aₑ .equiv-rel b₁ b₂) → W-Equiv-rel (f₁ (b .fst)) (f₂ (b .snd .fst)) } }
          (λ { ((a₂ , f₂) , (aₑ , fₑ)) → sup a₂ f₂ , IW-sup _ _ _ _ _ aₑ fₑ })
          (λ { (sup a₂ f₂ , (sup (_ , aₑ) g , (refl , h))) → ((a₂ , f₂) , (aₑ , λ b → g b , h b)) })
          (λ { (sup a₂ f₂ , (sup (_ , aₑ) g , (refl , h))) → refl })
          (is-contr-ΣΣ
            (Aₑ .equiv-fun→ _)
            (λ a₂ aₑ → is-contr-ΣΠ
                       {A = B₂ _}
                       {B = λ b₂ → W A₂ B₂}
                       {C = Σ _ λ b₁ → Σ _ λ b₂ → Bₑ aₑ .equiv-rel b₁ b₂}
                       (λ { (_ , (b₂ , _)) → b₂ })
                       (λ b → is-contr-retract
                              {A = Σ (Σ (B₂ a₂) (λ b₂ → Id b₂ b)) λ { (b₂ , _) → Σ (B₁ a₁) λ b₁ → Bₑ aₑ .equiv-rel b₁ b₂ }}
                              (λ { ((b₂ , p) , (b₁ , bₑ)) → (b₁ , (b₂ , bₑ)) , p })
                              (λ { ((b₁ , (b₂ , bₑ)) , p) → (b₂ , p) , (b₁ , bₑ) })
                              (λ _ → refl)
                              (is-contr-Σ is-contr-path-to λ _ → Bₑ aₑ .equiv-fun← _))
                       {D = λ b x → W-Equiv-rel (f₁ (b .fst)) x}
                       (λ { (b₁ , (_ , _)) → g b₁ })))

    W-Equiv-fun← : ∀ y → is-contr (Σ _ λ x → W-Equiv-rel x y)
    W-Equiv-fun← (sup a₂ f₂)
      = let g = λ b → W-Equiv-fun← (f₂ b) in
        is-contr-retract
          {A = Σ (Σ A₁ λ a₁ → B₁ a₁ → W A₁ B₁) λ { (a₁ , f₁) → Σ (Aₑ .equiv-rel a₁ a₂) λ aₑ → (b : Σ _ λ b₁ → Σ _ λ b₂ → Bₑ aₑ .equiv-rel b₁ b₂) → W-Equiv-rel (f₁ (b .fst)) (f₂ (b .snd .fst)) } }
          (λ { ((a₁ , f₁) , (aₑ , fₑ)) → sup a₁ f₁ , IW-sup _ _ _ _ _ aₑ fₑ })
          (λ { (sup a₁ f₁ , (sup (_ , aₑ) g , (refl , h))) → ((a₁ , f₁) , (aₑ , λ b → g b , h b)) })
          (λ { (sup a₁ f₁ , (sup (_ , aₑ) g , (refl , h))) → refl })
          (is-contr-ΣΣ
            (Aₑ .equiv-fun← _)
            (λ a₁ aₑ → is-contr-ΣΠ
                       {A = B₁ _}
                       {B = λ b₁ → W A₁ B₁}
                       {C = Σ _ λ b₁ → Σ _ λ b₂ → Bₑ aₑ .equiv-rel b₁ b₂}
                       (λ { (b₁ , (_ , _)) → b₁ })
                       (λ b → is-contr-retract
                              {A = Σ (Σ (B₁ a₁) (λ b₁ → Id b₁ b)) λ { (b₁ , _) → Σ (B₂ a₂) λ b₂ → Bₑ aₑ .equiv-rel b₁ b₂ }}
                              (λ { ((b₁ , p) , (b₂ , bₑ)) → ((b₁ , (b₂ , bₑ)) , p) })
                              (λ { ((b₁ , (b₂ , bₑ)) , p) → ((b₁ , p) , (b₂ , bₑ)) })
                              (λ _ → refl)
                              (is-contr-Σ is-contr-path-to λ _ → Bₑ aₑ .equiv-fun→ _))
                       {D = λ b x → W-Equiv-rel x (f₂ (b .snd .fst))}
                       (λ { (_ , (b₂ , _)) → g b₂ })))

  W-Equiv : Equiv (W A₁ B₁) (W A₂ B₂)
  W-Equiv .equiv-rel x₁ x₂ = W-Equiv-rel x₁ x₂
  W-Equiv .equiv-fun→ = W-Equiv-fun→
  W-Equiv .equiv-fun← = W-Equiv-fun←

  module _
    {a₁ a₂} (aₑ : Aₑ .equiv-rel a₁ a₂)
    {f₁ f₂} (fₑ : ∀ {b₁ b₂} (bₑ : Bₑ aₑ .equiv-rel b₁ b₂) → W-Equiv .equiv-rel (f₁ b₁) (f₂ b₂))
    where

    sup-Equiv : W-Equiv .equiv-rel (sup a₁ f₁) (sup a₂ f₂)
    sup-Equiv = IW-sup _ _ _ _ _ aₑ λ b → fₑ (b .snd .snd)
    
  module _ {k}
    {P₁ : W A₁ B₁ → Set k} {P₂ : W A₂ B₂ → Set k} (Pₑ : ∀ {x₁ x₂} (xₑ : W-Equiv .equiv-rel x₁ x₂) → Equiv (P₁ x₁) (P₂ x₂))
    {sup'₁ sup'₂}
      (sup'ₑ : ∀ {a₁ a₂} (aₑ : Aₑ .equiv-rel a₁ a₂)
                 {f₁ f₂} (fₑ : ∀ {b₁ b₂} (bₑ : Bₑ aₑ .equiv-rel b₁ b₂) → W-Equiv .equiv-rel (f₁ b₁) (f₂ b₂))
                 {p₁ p₂} (pₑ : ∀ {b₁ b₂} (bₑ : Bₑ aₑ .equiv-rel b₁ b₂) → Pₑ (fₑ bₑ) .equiv-rel (p₁ b₁) (p₂ b₂))
               → Pₑ (sup-Equiv aₑ fₑ) .equiv-rel (sup'₁ a₁ f₁ p₁) (sup'₂ a₂ f₂ p₂))
    where

    W-elim-Equiv : ∀ {x₁ x₂} (xₑ : W-Equiv .equiv-rel x₁ x₂)
                 → Pₑ xₑ .equiv-rel (W-elim P₁ sup'₁ x₁) (W-elim P₂ sup'₂ x₂)
    W-elim-Equiv {sup a₁ f₁} {sup a₂ f₂} (sup aₑ fₑ , refl , h)
      = sup'ₑ (aₑ .snd) _ (λ bₑ → W-elim-Equiv ((fₑ (_ , _ , bₑ)) , h (_ , _ , bₑ)))

--------------------------------------------------------------------------------

module _
  {A} (Aₑ : Equiv A A) (Aᵣ : IsRefl Aₑ)
  {B} (Bₑ : DepEquiv Aₑ B B) (Bᵣ : ∀ {a aₑ} (aᵣ : Aᵣ .refl-rel a aₑ) → IsRefl (Bₑ aₑ))
  where

  shape' : (x : W A B) (xₑ : W-Equiv-rel Aₑ Bₑ x x) → Set
  shape' (sup a f) (sup (_ , aₑ) fₑ , (refl , _)) = Aᵣ .refl-rel a aₑ
  
  pos' : (x : W A B) (xₑ : W-Equiv-rel Aₑ Bₑ x x) → shape' x xₑ → Set
  pos' (sup a f) (sup (_ , aₑ) fₑ , (refl , _)) aᵣ = Σ _ λ b → Σ _ λ bₑ → Bᵣ aᵣ .refl-rel b bₑ 

  color' : (x : W A B) (xₑ : W-Equiv-rel Aₑ Bₑ x x) → (aᵣ : shape' x xₑ) → pos' x xₑ aᵣ → Σ _ λ x → W-Equiv-rel Aₑ Bₑ x x
  color' (sup a f) (sup (_ , aₑ) fₑ , (refl , gₑ)) aᵣ (b , bₑ , bᵣ) = (f b) , (fₑ (b , b , bₑ) , gₑ (b , b , bₑ))

  W-IsRefl-rel : (x : W A B) (xₑ : W-Equiv-rel Aₑ Bₑ x x) → Set
  W-IsRefl-rel x xₑ =
    IW (Σ _ λ x → W-Equiv-rel Aₑ Bₑ x x)
       (λ { (x , xₑ) → shape' x xₑ })
       (λ { {x , xₑ} → pos' x xₑ })
       (λ { {x , xₑ} {_} → color' x xₑ _ })
       (x , xₑ)

  abstract
    W-IsRefl-contr : (x : W A B) → is-contr (Σ _ λ xₑ → W-IsRefl-rel x xₑ)
    W-IsRefl-contr (sup a f)
      = let grec = λ b → W-IsRefl-contr (f b) in
        is-contr-retract
          {A = Σ (Σ (Aₑ .equiv-rel a a) λ aₑ → (b : Σ _ λ b₁ → Σ _ λ b₂ → Bₑ aₑ .equiv-rel b₁ b₂) → W-Equiv-rel Aₑ Bₑ (f (b .fst)) (f (b .snd .fst))) λ (aₑ , fₑ) →
               Σ (Aᵣ .refl-rel a aₑ) λ aᵣ → (b : Σ _ λ b → Σ _ λ bₑ → Bᵣ aᵣ .refl-rel b bₑ) → W-IsRefl-rel (f (b .fst)) (fₑ (b .fst , b .fst , b .snd .fst))}
          (λ { ((aₑ , fₑ) , (aᵣ , fᵣ)) → IW-sup _ _ _ _ _ aₑ fₑ , IW-sup _ _ _ _ _ aᵣ fᵣ })
          (λ { ((sup (_ , aₑ) fₑ , (refl , hₑ)) , (sup (_ , aᵣ) fᵣ , (refl , hᵣ))) → (aₑ , λ b → fₑ b , hₑ b) , (aᵣ , λ b → fᵣ b , hᵣ b) })
          (λ { ((sup (_ , aₑ) fₑ , (refl , hₑ)) , (sup (_ , aᵣ) fᵣ , (refl , hᵣ))) → refl })
          (is-contr-ΣΣ
            (Aᵣ .refl-contr _)
            (λ aₑ aᵣ → is-contr-ΣΠ
                       {A = Σ (B a) (λ b₁ → Σ (B a) (Bₑ aₑ .equiv-rel b₁))}
                       {B = λ z → W-Equiv-rel Aₑ Bₑ (f (z .fst)) (f (z .snd .fst))}
                       {C = Σ (B a) (λ b → Σ (Bₑ aₑ .equiv-rel b b) (Bᵣ aᵣ .refl-rel b))}
                       (λ { (b , bₑ , bᵣ) → _ , _ , bₑ })
                       (equiv-total-contr (λ _ → Bᵣ aᵣ .refl-contr _) (λ _ → Bₑ aₑ .equiv-fun→ _) _)
                       {D = λ b x → W-IsRefl-rel _ x}
                       (λ { (b , bₑ , bᵣ) → grec _ })))


  W-IsRefl : IsRefl (W-Equiv Aₑ Bₑ)
  W-IsRefl .refl-rel = W-IsRefl-rel
  W-IsRefl .refl-contr = W-IsRefl-contr

--------------------------------------------------------------------------------

module _ {i}
  {A₁ A₂ : Set i} (Aₑ : Equiv A₁ A₂)
  {x₁ x₂} (xₑ : Aₑ .equiv-rel x₁ x₂)
  {y₁ y₂} (yₑ : Aₑ .equiv-rel y₁ y₂)
  where

  Id-Equiv-rel : Id x₁ y₁ → Id x₂ y₂ → Set i 
  Id-Equiv-rel refl refl = Id xₑ yₑ

module _ {i}
  {A₁ A₂ : Set i} (Aₑ : Equiv A₁ A₂)
  {x₁ x₂} (xₑ : Aₑ .equiv-rel x₁ x₂)
  where

  abstract
    Id-Equiv-fun↓ : ∀ {y₁} p₁ {y₂} p₂ → is-contr (Σ _ λ yₑ → Id-Equiv-rel Aₑ xₑ {y₁} {y₂} yₑ p₁ p₂)
    Id-Equiv-fun↓ refl refl = is-contr-path-from

module _ {i}
  {A₁ A₂ : Set i} (Aₑ : Equiv A₁ A₂)
  {x₁ x₂} (xₑ : Aₑ .equiv-rel x₁ x₂)
  {y₁ y₂} (yₑ : Aₑ .equiv-rel y₁ y₂)
  where
       
  Id-Equiv : Equiv (Id x₁ y₁) (Id x₂ y₂)
  Id-Equiv .equiv-rel  = Id-Equiv-rel Aₑ xₑ yₑ
  Id-Equiv .equiv-fun→ refl
    = is-contr-π₂
      (Aₑ .equiv-fun→ x₁)
      (is-contr-ΣΣ
       {D = λ y₂ q yₑ → Id-Equiv-rel Aₑ xₑ yₑ refl q}
       is-contr-path-from
       (λ { _ refl → is-contr-path-from }))
      _
  Id-Equiv .equiv-fun← refl
    = is-contr-π₂
      (Aₑ .equiv-fun← x₂)
      (is-contr-ΣΣ
       {D = λ y₁ p yₑ → Id-Equiv-rel Aₑ xₑ yₑ p refl}
       is-contr-path-from
       (λ { _ refl → is-contr-path-from }))
      _

module _ {i}
  {A₁ A₂ : Set i} (Aₑ : Equiv A₁ A₂)
  {x₁ x₂} (xₑ : Aₑ .equiv-rel x₁ x₂)
  where

  refl-Equiv : Id-Equiv-rel Aₑ xₑ xₑ refl refl
  refl-Equiv = refl

module _ {i j}
  {A₁ A₂ : Set i} (Aₑ : Equiv A₁ A₂)
  {x₁ x₂} (xₑ : Aₑ .equiv-rel x₁ x₂)
  {P₁ P₂} (Pₑ : DepEquiv {i} {j} (Σ-Equiv Aₑ (λ yₑ → Id-Equiv Aₑ xₑ yₑ)) P₁ P₂)
  {d₁ d₂} (dₑ : Pₑ (xₑ , refl-Equiv Aₑ xₑ) .equiv-rel d₁ d₂)
  where

  J-Equiv : ∀ {y₁ y₂} (yₑ : Aₑ .equiv-rel y₁ y₂)
              {p₁ p₂} (pₑ : Id-Equiv Aₑ xₑ yₑ .equiv-rel p₁ p₂)
            → Pₑ (yₑ , pₑ) .equiv-rel (J (λ y p → P₁ (y , p)) p₁ d₁) (J (λ y p → P₂ (y , p)) p₂ d₂)
  J-Equiv _ {refl} {refl} refl = dₑ

--------------------------------------------------------------------------------

module _ {i}
  {A : Set i} {Aₑ : Equiv A A} (Aᵣ : IsRefl Aₑ)
  {x} {xₑ : Aₑ .equiv-rel x x} (xᵣ : Aᵣ .refl-rel x xₑ)
  {y} {yₑ : Aₑ .equiv-rel y y} (yᵣ : Aᵣ .refl-rel y yₑ)
  where

  Id-IsRefl-rel : ∀ p → Id-Equiv-rel Aₑ xₑ yₑ p p → Set i
  Id-IsRefl-rel refl refl = Id xᵣ yᵣ

module _ {i}
  {A : Set i} {Aₑ : Equiv A A} (Aᵣ : IsRefl Aₑ)
  {x} {xₑ : Aₑ .equiv-rel x x} (xᵣ : Aᵣ .refl-rel x xₑ)
  where

  Id-IsRefl-fun↓ : ∀ {y} p (yₑ : Aₑ .equiv-rel y y) pₑ
                 → is-contr (Σ _ λ yᵣ → Id-IsRefl-rel Aᵣ xᵣ {y} {yₑ} yᵣ p pₑ)
  Id-IsRefl-fun↓ refl yₑ refl = is-contr-path-from
  
module _ {i}
  {A : Set i} {Aₑ : Equiv A A} (Aᵣ : IsRefl Aₑ)
  {x} {xₑ : Aₑ .equiv-rel x x} (xᵣ : Aᵣ .refl-rel x xₑ)
  {y} {yₑ : Aₑ .equiv-rel y y} (yᵣ : Aᵣ .refl-rel y yₑ)
  where

  Id-IsRefl : IsRefl (Id-Equiv Aₑ xₑ yₑ)
  Id-IsRefl .refl-rel   = Id-IsRefl-rel Aᵣ xᵣ yᵣ
  Id-IsRefl .refl-contr refl
    = is-contr-π₂
      (Aᵣ .refl-contr x)
      (is-contr-ΣΣ
       {D = λ yₑ q yᵣ → Id-IsRefl-rel Aᵣ xᵣ yᵣ refl q}
       is-contr-path-from
       (λ { _ refl → is-contr-path-from }))
      _

module _ {i}
  {A : Set i} {Aₑ : Equiv A A} (Aᵣ : IsRefl Aₑ)
  {x} {xₑ : Aₑ .equiv-rel x x} (xᵣ : Aᵣ .refl-rel x xₑ)
  where

  refl-IsRefl : Id-IsRefl-rel Aᵣ xᵣ xᵣ refl (refl-Equiv Aₑ xₑ)
  refl-IsRefl = refl

module _ {i j}
  {A : Set i} {Aₑ : Equiv A A} (Aᵣ : IsRefl Aₑ)
  {x} {xₑ : Aₑ .equiv-rel x x} (xᵣ : Aᵣ .refl-rel x xₑ)
  {P} {Pₑ : DepEquiv {i} {j} (Σ-Equiv Aₑ λ yₑ → Id-Equiv Aₑ xₑ yₑ) P P}
    (Pᵣ : DepIsRefl {Γₑ = Σ-Equiv Aₑ λ yₑ → Id-Equiv Aₑ xₑ yₑ} (Σ-IsRefl Aᵣ λ yᵣ → Id-IsRefl Aᵣ xᵣ yᵣ) Pₑ)
  {d} {dₑ : Pₑ (xₑ , refl-Equiv Aₑ xₑ) .equiv-rel d d} (dᵣ : Pᵣ (xᵣ , (refl-IsRefl Aᵣ xᵣ)) .refl-rel d dₑ)
  where

  J-IsRefl : ∀ {y} {yₑ : Aₑ .equiv-rel y y} (yᵣ : Aᵣ .refl-rel y yₑ)
               {p} {pₑ : Id-Equiv-rel Aₑ xₑ yₑ p p} (pᵣ : Id-IsRefl-rel Aᵣ xᵣ yᵣ p pₑ)
             → Pᵣ (yᵣ , pᵣ) .refl-rel _ (J-Equiv Aₑ xₑ Pₑ dₑ yₑ pₑ)
  J-IsRefl _ {refl} {refl} refl = dᵣ

--------------------------------------------------------------------------------

equiv-to-id : ∀ {i} {A B : Set i} → equiv A B → Id A B
equiv-to-id {i} {A} {B} f
  = transp-contr (ua A) (λ { (B , _) → Id A B })
    (_ , id-equiv)
    (_ , f)
    refl
    
module _ {i} {A B : Set i} where
  equiv→Equiv : equiv A B → Equiv A B
  equiv→Equiv (f , f-equiv) = Equiv-graph f f-equiv

  Equiv→equiv : Equiv A B → equiv A B
  Equiv→equiv R .fst a = R .equiv-fun→ a .is-contr-center .fst
  Equiv→equiv R .snd = Equiv→is-equiv R _ λ a → R .equiv-fun→ a .is-contr-center .snd

module _ {i} {A B : Set i} where
  Id-between-Equiv : {R₁ R₂ : Equiv A B}
                   → (∀ x y → equiv (R₁ .equiv-rel x y) (R₂ .equiv-rel x y))
                   → Id R₁ R₂
  Id-between-Equiv {R₁} {R₂} p = ap (λ { (x , y , z) → record { equiv-rel = x ; equiv-fun→ = y ; equiv-fun← = z } }) inner
    where
      inner : Id {A = Σ (A → B → Set i) λ R → (∀ a → is-contr (Σ B λ b → R a b)) × (∀ b → is-contr (Σ A λ a → R a b))}
                 (R₁ .equiv-rel , R₁ .equiv-fun→ , R₁ .equiv-fun←)
                 (R₂ .equiv-rel , R₂ .equiv-fun→ , R₂ .equiv-fun←)
      inner
        = pair-Id
          (lam-Id λ x → lam-Id λ y → equiv-to-id (p x y))
          (is-prop-all-paths (is-prop-Σ (is-prop-Π λ a → is-prop-is-contr) (λ _ → is-prop-Π λ a → is-prop-is-contr))
            _ _)

  equiv→Equiv← : ∀ (R : Equiv A B) → Id (equiv→Equiv (Equiv→equiv R)) R
  equiv→Equiv← R = Id-between-Equiv (λ x y → _ , iso→equiv (to _ _) (fr _ _) (to-fr _ _) (fr-to _ _))
    where
      to : ∀ x y → equiv→Equiv (Equiv→equiv R) .equiv-rel x y → R .equiv-rel x y
      to x y refl = R .equiv-fun→ x .is-contr-center .snd
      
      fr : ∀ x y → R .equiv-rel x y → equiv→Equiv (Equiv→equiv R) .equiv-rel x y
      fr x y p = transp-contr (R .equiv-fun→ x) (λ { (z , q) → Id _ z }) (R .equiv-fun→ x .is-contr-center) (y , p)
                 refl 

      fr-to : ∀ x y p → Id (fr x y (to x y p)) p
      fr-to _ _ refl = transp-contr-β

      to-fr : ∀ x y p → Id (to x y (fr x y p)) p
      to-fr x y p = transp-contr (R .equiv-fun→ x) (λ { (z , q) → Id (to x z (fr x z q)) q }) (R .equiv-fun→ x .is-contr-center) (y , p)
                    (ap (to _ _) transp-contr-β)

  Equiv→equiv← : ∀ (E : equiv A B) → Id (Equiv→equiv (equiv→Equiv E)) E
  Equiv→equiv← _ = pair-Id refl (is-prop-all-paths (is-prop-Π (λ _ → is-prop-is-contr)) _ _)

  equiv↔Equiv : equiv (equiv A B) (Equiv A B)
  equiv↔Equiv = _ , iso→equiv equiv→Equiv Equiv→equiv equiv→Equiv← Equiv→equiv←
  
  Equiv↔equiv : equiv (Equiv A B) (equiv A B) 
  Equiv↔equiv = _ , iso→equiv Equiv→equiv equiv→Equiv Equiv→equiv← equiv→Equiv←

  Equiv-op : Equiv A B → Equiv B A
  Equiv-op R .equiv-rel x y = R .equiv-rel y x
  Equiv-op R .equiv-fun→ = R .equiv-fun←
  Equiv-op R .equiv-fun← = R .equiv-fun→

module _ {i} {A B : Set i} where
  equiv-Equiv-op : equiv (Equiv A B) (Equiv B A)
  equiv-Equiv-op = _ , iso→equiv Equiv-op Equiv-op (λ _ → refl) (λ _ → refl)

abstract
  ua' : ∀ {i} {A : Set i} → is-contr (Σ (Set i) (λ B → Σ (B → A) is-equiv))
  ua' {i} {A}
    = is-contr-equiv _
      (Equiv→equiv
        (Σ-Equiv (Equiv-Id _) (λ { {B} refl → equiv→Equiv (comp-equiv equiv↔Equiv (comp-equiv equiv-Equiv-op Equiv↔equiv)) }))
        .snd)
      (ua A)

Univ-Equiv : ∀ {i} → Equiv (Set i) (Set i)
Univ-Equiv .equiv-rel = Equiv
Univ-Equiv {i} .equiv-fun→ A
  = is-contr-equiv _
    (equiv-total _ (λ B → comp-equiv (_ , is-equiv-lower) equiv↔Equiv .snd))
    (is-contr-retract
      (total (λ _ → lift {_} {lsuc i}))
      (total (λ _ → lower))
      (λ _ → refl)
      (ua _))
Univ-Equiv {i} .equiv-fun← B
  = is-contr-equiv _
    (equiv-total _ (λ B → comp-equiv (_ , is-equiv-lower) equiv↔Equiv .snd))
    (is-contr-retract
     (total λ _ → lift {_} {lsuc i})
     (total λ _ → lower)
     (λ _ → refl)
     ua')

module _ {i} {A : Set i} (E : Equiv A A) where
  private
    Id-between-IsRefl : {R₁ R₂ : IsRefl E}
                      → (∀ x y → equiv (R₁ .refl-rel x y) (R₂ .refl-rel x y))
                      → Id R₁ R₂
    Id-between-IsRefl {R₁} {R₂} p = ap (λ { (x , y) → record { refl-rel = x ; refl-contr = y } }) inner
      where
        inner : Id {A = Σ (∀ a → E .equiv-rel a a → Set i) λ R → ∀ a → is-contr (Σ _ (R a))}
                   (R₁ .refl-rel , R₁ .refl-contr)
                   (R₂ .refl-rel , R₂ .refl-contr)
        inner = pair-Id (lam-Id λ _ → lam-Id λ _ → equiv-to-id (p _ _))
                        (is-prop-all-paths
                          (is-prop-Π λ _ → is-prop-is-contr)
                          _ _)

    IsRefl→refl : IsRefl E → (a : A) → Lift (lsuc i) (E .equiv-rel a a)
    IsRefl→refl R a .lower = R .refl-contr a .is-contr-center .fst

    refl→IsRefl : ((a : A) → Lift (lsuc i) (E .equiv-rel a a)) → IsRefl E
    refl→IsRefl f .refl-rel   a aₑ = Id (f a .lower) aₑ
    refl→IsRefl f .refl-contr _ = is-contr-path-from

    IsRefl→refl← : ∀ R → Id (IsRefl→refl (refl→IsRefl R)) R
    IsRefl→refl← R = refl

    refl→IsRefl← : ∀ R → Id (refl→IsRefl (IsRefl→refl R)) R
    refl→IsRefl← R = Id-between-IsRefl (λ x y → _ , iso→equiv (fr x y) (to x y) (fr-to x y) (to-fr x y))
      where
        fr : ∀ x y → Id (R .refl-contr x .is-contr-center .fst) y → R .refl-rel x y
        fr x _ refl = R .refl-contr x .is-contr-center .snd

        to : ∀ x y → R .refl-rel x y → Id (R .refl-contr x .is-contr-center .fst) y
        to x y p = transp-contr (R .refl-contr x) (λ { (y , p) → Id (R .refl-contr x .is-contr-center .fst) y })
                   (R .refl-contr x .is-contr-center) (y , p) refl

        fr-to : ∀ x y p → Id (fr x y (to x y p)) p
        fr-to x y p = transp-contr (R .refl-contr x) (λ { (y , p) → Id (fr x y (to x y p)) p })
                      (R .refl-contr x .is-contr-center) (y , p) (ap (fr _ _) transp-contr-β)

        to-fr : ∀ x y p → Id (to x y (fr x y p)) p
        to-fr _ _ refl = transp-contr-β

  IsRefl↔refl : equiv (IsRefl E) (∀ a → Lift (lsuc i) (E .equiv-rel a a))
  IsRefl↔refl = _ , iso→equiv IsRefl→refl refl→IsRefl IsRefl→refl← refl→IsRefl←

  refl↔IsRefl : equiv (∀ a → Lift (lsuc i) (E .equiv-rel a a)) (IsRefl E)
  refl↔IsRefl = _ , iso→equiv refl→IsRefl IsRefl→refl refl→IsRefl← IsRefl→refl← 

module _ {i} {A : Set i} (E : Equiv A A) (cE : ∀ a b → E .equiv-rel a b) (x : A) where
  is-contr-from-Equiv : is-contr A
  is-contr-from-Equiv .is-contr-center = x
  is-contr-from-Equiv .is-contr-path y
    = transp-contr (E .equiv-fun→ x) (λ { (y , _) → Id x y })
      (x , cE _ _)
      (y , cE _ _)
      refl

Univ-IsRefl : ∀ {i} → IsRefl (Univ-Equiv {i})
Univ-IsRefl {i} .refl-rel _ E = IsRefl E
Univ-IsRefl {i} .refl-contr A
  = is-contr-equiv _
    (equiv-total _ (λ E → refl↔IsRefl _ .snd))
    (is-contr-retract
      (λ { ((x , y , z) , w) → (record { equiv-rel = x ; equiv-fun→ = y ; equiv-fun← = z }) , (λ a → lift (w a)) })
      (λ { (E , r) → (E .equiv-rel , E .equiv-fun→ , E .equiv-fun←) , (λ a → r a .lower) })
      (λ a → refl)
      is-contr-T)
  where
    T = Σ (Σ (A → A → Set i) λ R → (∀ a → is-contr (Σ A λ b → R a b)) × (∀ b → is-contr (Σ A λ a → R a b))) λ E →
          ((a : A) → E .fst a a)

    Equiv→T : Σ (Equiv A A) (λ E → ∀ a → E .equiv-rel a a) → T
    Equiv→T (x , y) = (x .equiv-rel , x .equiv-fun→ , x .equiv-fun←) , y

    TE : Equiv T T
    TE = Σ-Equiv
         (Σ-Equiv (Π-Equiv (Equiv-Id A) λ _ → Π-Equiv (Equiv-Id A) λ _ → Univ-Equiv) λ R →
           Equiv-between-prop
             (is-prop-Σ
               (is-prop-Π λ _ → is-prop-is-contr) λ _ →
               (is-prop-Π λ _ → is-prop-is-contr))
             (is-prop-Σ
               (is-prop-Π λ _ → is-prop-is-contr) λ _ →
               (is-prop-Π λ _ → is-prop-is-contr))
               (λ x → (λ a → is-contr-equiv _ (Equiv→equiv (Σ-Equiv (Equiv-Id A) (λ { refl → R refl refl })) .snd) (x .fst a))
                    , (λ b → is-contr-equiv _ (Equiv→equiv (Σ-Equiv (Equiv-Id A) (λ { refl → R refl refl })) .snd) (x .snd b)))
               (λ x → (λ a → is-contr-equiv _ (Equiv→equiv (Σ-Equiv (Equiv-Id A) (λ { refl → Equiv-op (R refl refl) })) .snd) (x .fst a))
                    , (λ b → is-contr-equiv _ (Equiv→equiv (Σ-Equiv (Equiv-Id A) (λ { refl → Equiv-op (R refl refl) })) .snd) (x .snd b))))
         λ R → Π-Equiv (Equiv-Id A) λ a → R .fst a a
  

    fr : ∀ (a b : T) x y → a .fst .fst x y → b .fst .fst x y
    fr a b x y p
      = transp-contr (a .fst .snd .fst x) (λ { (y , _) → b .fst .fst x y })
        (x , a .snd x)
        (y , p)
        (b .snd x)

    all : ∀ (a b : T) x y → Equiv (a .fst .fst x y) (b .fst .fst x y)
    all a b x y = equiv→Equiv (_ , iso→equiv (fr a b _ _) (to _ _) (fr-to _ _) (to-fr _ _))
      where
        to : ∀ x y → b .fst .fst x y → a .fst .fst x y
        to x y p
          = transp-contr (b .fst .snd .fst x) (λ { (y , _) → a .fst .fst x y })
            (x , b .snd x)
            (y , p)
            (a .snd x)
  
        fr-to : ∀ x y p → Id (fr a b x y (to x y p)) p
        fr-to x y p
          = transp-contr (b .fst .snd .fst x) (λ { (y , p) → Id (fr a b x y (to x y p)) p })
            (x , b .snd x)
            (y , p)
            (ap (fr a b x x) transp-contr-β ∙ transp-contr-β)

        to-fr : ∀ x y p → Id (to x y (fr a b x y p)) p
        to-fr x y p
          = transp-contr (a .fst .snd .fst x) (λ { (y , p) → Id (to x y (fr a b x y p)) p })
            (x , a .snd x)
            (y , p)
            (ap (to x x) transp-contr-β ∙ transp-contr-β)

    is-contr-T : is-contr T
    is-contr-T
      = is-contr-from-Equiv
        TE
        (λ a b → ((λ { refl refl → all a b _ _ }) , tt) , λ { refl → transp-contr-β })
        (Equiv→T (Equiv-Id _ , λ _ → refl))