{-# OPTIONS --postfix-projections --prop --rewriting #-}

module AcyclicTwoLevel-Pi where

open import Agda.Primitive
open import Lib
open import Fam as _
open import Id as _
open import Id-Tele as _
open import Id-Misc as _
open import Id-Acyclic as _
open import Pi as _
open import Pi-Tele as _
open import TwoLevel
open import Quotient
open import Cong
open import AcyclicTwoLevel
open import AcyclicTwoLevel-Id

module _ {i j} (C : TwoLevelFam {i} {j}) (IsAcyclic-C : IsAcyclic C) where
  private
    open IsAcyclic IsAcyclic-C
    open IsAcyclic-Cong C IsAcyclic-C
    module C              = TwoLevelFam C
    open Id-Tele-r C.Outer

    -- We use cheat here because the agda instance resolution is too slow...
    module CPi            = Pi-StrictBeta C.OuterPi
    module CId            = IdM C.Outer _
    module CC             = Fam (C.Outer ∗ C.Outer)
    module CCId           = IdM (C.Outer ∗ C.Outer) ⦃ CId-Elim-C = cheat ⦄ _
    module CCC            = Fam ((C.Outer ∗ C.Outer) ∗ C.Outer)
    module CCCId          = IdM ((C.Outer ∗ C.Outer) ∗ C.Outer) ⦃ CId-Elim-C = cheat ⦄ _
    module CCCC           = Fam (((C.Outer ∗ C.Outer) ∗ C.Outer) ∗ C.Outer)
    module CCCCId         = IdM (((C.Outer ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ⦃ CId-Elim-C = cheat ⦄ _

    module CCId-Elim-C    = Id-ElimM (C.Outer ∗ C.Outer) C.Outer ⦃ CId-Elim-C = cheat ⦄ ⦃ CId-Elim-D = cheat ⦄ ⦃ DId-Elim-D = cheat ⦄  _
    module CCCId-Elim-CC  = Id-ElimM ((C.Outer ∗ C.Outer) ∗ C.Outer) (C.Outer ∗ C.Outer) ⦃ CId-Elim-C = cheat ⦄ ⦃ CId-Elim-D = cheat ⦄ ⦃ DId-Elim-D = cheat ⦄  _
    module CCCCId-Elim-CC = Id-ElimM (((C.Outer ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) (C.Outer ∗ C.Outer) ⦃ CId-Elim-C = cheat ⦄ ⦃ CId-Elim-D = cheat ⦄ ⦃ DId-Elim-D = cheat ⦄ _

  private
    -- Copy of CPi with a definitional beta
    postulate cpi : Pi-StrictBeta C.Inner C.Outer
    module cpi = Pi-StrictBeta cpi
    {-# REWRITE cpi.app-βₛ #-}
    open Pi.Instances cpi.pi

  module _ ⦃ ICPi : Pi-Intro C.Inner C.Inner ⦄ where
    private
      module ICPi          = Pi-Intro ICPi
    C~-Pi-Intro : Cong-Pi-Intro C~ ⦃ CPi-Intro = ICPi ⦄
    C~-Pi-Intro .Cong-Pi-Intro.Π~ {A₁} {A₂} {B₁} {B₂} ∣ A~ ∣ B~
      = ∥-∥-ap (CCId-Elim-C.ap (λ (A , B) → ICPi.Π A (cpi.app B)) {x = A₁ , cpi.lam B₁} {y = A₂ , cpi.lam B₂})
               p₂
      where i⊤ = IsSet-⊤ {lzero} {lzero}
            p₂ = JM.funext' _ C.tm ⦃ ECPi = cpi.pi ⦄ ∣ A~ ∣
                 λ a₁ a₂ a~ → ∥-∥-ap (λ x → JM.baseChange↑ ⦃ IsSet-B = i⊤ ⦄ (λ _ → tt) (λ _ → C.ty) a~ (JM.Id-in ⦃ IsSet-A = i⊤ ⦄ (λ _ → C.ty) x)) (B~ ∣ a~ ∣)

    C~-Pi-Intro .Cong-Pi-Intro.lam~ {A₁} {A₂} {B₁} {B₂} {b₁} {b₂} ∣ A~ ∣ B~ b~
      = ∥-∥-ap (CCCId-Elim-CC.ap (λ ((A , B) , b) → ICPi.Π A (cpi.app B) , ICPi.lam {B = cpi.app B} (cpi.app b))
                {x = (A₁ , cpi.lam B₁) , cpi.lam b₁} {y = (A₂ , cpi.lam B₂) , cpi.lam b₂})
               p₃
      where i⊤ = IsSet-⊤ {lzero} {lzero}
            p₂ : ∥ CC.Tm (CCId.Id (A₁ , cpi.lam B₁) (A₂ , cpi.lam B₂)) ∥
            p₂ = JM.funext' _ C.tm ⦃ ECPi = cpi.pi ⦄ ∣ A~ ∣
                 λ a₁ a₂ a~ → ∥-∥-ap (λ x → JM.baseChange↑ ⦃ IsSet-B = i⊤ ⦄ (λ _ → tt) (λ _ → C.ty) a~ (JM.Id-in ⦃ IsSet-A = i⊤ ⦄ (λ _ → C.ty) x)) (B~ ∣ a~ ∣)

            p₃ : ∥ CCC.Tm (CCCId.Id ((A₁ , cpi.lam B₁) , cpi.lam b₁) ((A₂ , cpi.lam B₂) , cpi.lam b₂)) ∥
            p₃ = ∥-∥-bind p₂ λ p₂ →
                 let p₃₀ a₁ a₂ a~ = ∥-∥-ap (λ x → JM.baseChange↑ _ _ a~ x) (b~ ∣ JM.baseChange↓ (λ (A , B) → A) C.tm p₂ a~ ∣) in
                 JM.funext' C.ty C.tm ⦃ ECPi = cpi.pi ⦄ ∣ p₂ ∣ p₃₀

  module _ ⦃ ICPi : Pi-Intro C.Inner C.Inner ⦄ ⦃ ICId : Id-Intro C.Inner ⦄ ⦃ ICPi-App : Pi-App C.Inner C.Inner ⦃ CDPi-Intro = ICPi ⦄ ⦄ where
    open Id-Intro ICId
    open Pi-Intro ICPi
    open Pi-App ICPi-App

    C~-Pi-App : Cong-Pi-App C~ (C~-Id-Intro C IsAcyclic-C) ⦃ CPi-Intro = ICPi ⦄ C~-Pi-Intro ⦃ CPi-App = ICPi-App ⦄
    C~-Pi-App .Cong-Pi-App.app~ {A₁} {A₂} {B₁} {B₂} {f₁} {f₂} {a₁} {a₂} ∣ A~ ∣ B~ ∣ f~ ∣ ∣ a~ ∣
      = ∥-∥-ap (CCCCId-Elim-CC.ap {A = T₄}
                                  (λ (((A , B) , f) , a) → cpi.app B a , app {A = A} {B = cpi.app B} f a)
                                  {x = ((A₁ , cpi.lam B₁) , f₁) , a₁} {y = ((A₂ , cpi.lam B₂) , f₂) , a₂})
               p₄
      where i⊤ = IsSet-⊤ {lzero} {lzero}
            T₁ = C.ty
            T₂ = T₁ , λ A → cpi.Π A λ _ → C.ty
            p₂ : ∥ CC.Tm (CCId.Id {A = T₂} (A₁ , cpi.lam B₁) (A₂ , cpi.lam B₂)) ∥
            p₂ = JM.funext' _ C.tm ⦃ ECPi = cpi.pi ⦄ ∣ A~ ∣
                 λ a₁ a₂ a~ → ∥-∥-ap (λ x → JM.baseChange↑ ⦃ IsSet-B = i⊤ ⦄ (λ _ → tt) (λ _ → C.ty) a~ (JM.Id-in ⦃ IsSet-A = i⊤ ⦄ (λ _ → C.ty) x)) (B~ ∣ a~ ∣)

            T₃ = T₂ , λ (A , B) → C.tm (Π A (cpi.app B))
            p₃ : ∥ CCC.Tm (CCCId.Id {A = T₃} ((A₁ , cpi.lam B₁) , f₁) ((A₂ , cpi.lam B₂) , f₂)) ∥
            p₃ = ∥-∥-bind p₂ λ p₂ → ∣ JM.baseChange↑ {A = T₂} {B = C.ty} (λ (A , B) → Π A (cpi.app B)) C.tm p₂ f~ ∣

            T₄ = T₃ , λ ((A , B) , f) → C.tm A
            p₄ : ∥ CCCC.Tm (CCCCId.Id {A = T₄} (((A₁ , cpi.lam B₁) , f₁) , a₁) (((A₂ , cpi.lam B₂) , f₂) , a₂)) ∥
            p₄ = ∥-∥-bind p₃ λ p₃ → ∣ JM.baseChange↑ {A = T₃} {B = C.ty} (λ ((A , B) , f) → A) C.tm p₃ a~ ∣

    C~-Pi-App .Cong-Pi-App.app-β~ {A₁} {A₂} {B₁} {B₂} {b₁} {b₂} {a₁} {a₂} ∣ A~ ∣ B~ b~ ∣ a~ ∣
      = ∥-∥-ap (CCCCId-Elim-CC.ap {A = T₄} (λ (((A , B) , b) , a) → Id (app (lam {B = cpi.app B} (cpi.app b)) a) (cpi.app b a) , app-β {A = A} {B = cpi.app B} {f = cpi.app b} {a = a})
                                  {x = ((A₁ , cpi.lam B₁) , cpi.lam b₁) , a₁} {y = ((A₂ , cpi.lam B₂) , cpi.lam b₂) , a₂})
               p₄
      where i⊤ = IsSet-⊤ {lzero} {lzero}
            T₁ = C.ty
            T₂ = T₁ , λ A → cpi.Π A λ _ → C.ty
            p₂ : ∥ CC.Tm (CCId.Id {A = T₂} (A₁ , cpi.lam B₁) (A₂ , cpi.lam B₂)) ∥
            p₂ = JM.funext' _ C.tm ⦃ ECPi = cpi.pi ⦄ ∣ A~ ∣
                 λ a₁ a₂ a~ → ∥-∥-ap (λ x → JM.baseChange↑ ⦃ IsSet-B = i⊤ ⦄ (λ _ → tt) (λ _ → C.ty) a~ (JM.Id-in ⦃ IsSet-A = i⊤ ⦄ (λ _ → C.ty) x)) (B~ ∣ a~ ∣)

            T₃ = T₂ , λ (A , B) → cpi.Π A λ a → C.tm (cpi.app B a)
            p₃ : ∥ CCC.Tm (CCCId.Id {A = T₃} ((A₁ , cpi.lam B₁) , cpi.lam b₁) ((A₂ , cpi.lam B₂) , cpi.lam b₂)) ∥
            p₃ = ∥-∥-bind p₂ λ p₂ →
                 let p₃₀ a₁ a₂ a~ = ∥-∥-ap (λ x → JM.baseChange↑ _ _ a~ x) (b~ ∣ JM.baseChange↓ (λ (A , B) → A) C.tm p₂ a~ ∣) in
                 JM.funext' C.ty C.tm ⦃ ECPi = cpi.pi ⦄ ∣ p₂ ∣ p₃₀

            T₄ = T₃ , λ ((A , B) , b) → C.tm A
            p₄ : ∥ CCCC.Tm (CCCCId.Id {A = T₄} (((A₁ , cpi.lam B₁) , cpi.lam b₁) , a₁) (((A₂ , cpi.lam B₂) , cpi.lam b₂) , a₂)) ∥
            p₄ = ∥-∥-bind p₃ λ p₃ → ∣ JM.baseChange↑ {A = T₃} {B = C.ty} (λ ((A , B) , b) → A) C.tm p₃ a~ ∣