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

module AcyclicTwoLevel-Id 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

module _ {i j} (C : TwoLevelFam {i} {j}) (IsAcyclic-C : IsAcyclic C) where
  open IsAcyclic IsAcyclic-C
  private
    module C            = TwoLevelFam C
    open Id-Tele-r C.Outer
    open IsAcyclic-Cong C IsAcyclic-C
    module CPi          = Pi-StrictBeta C.OuterPi
    module IC           = Fam C.Inner

    -- We use cheat here because the agda instance resolution is too slow...
    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 CCCCC    = Fam ((((C.Outer ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ∗ C.Outer)
    module CCCCCId  = IdM ((((C.Outer ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ⦃ CId-Elim-C = cheat ⦄ _
    module CCCCCC   = Fam (((((C.Outer ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ∗ C.Outer)
    module CCCCCCId = IdM (((((C.Outer ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ∗ C.Outer) ⦃ CId-Elim-C = cheat ⦄ _

    module CCCId-Elim-C = Id-ElimM ((C.Outer ∗ C.Outer) ∗ C.Outer) C.Outer ⦃ CId-Elim-C = cheat ⦄ ⦃ CId-Elim-D = cheat ⦄ ⦃ DId-Elim-D = cheat ⦄ _
    module CCCCCCId-Elim-CC = Id-ElimM (((((C.Outer ∗ C.Outer) ∗ 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-βₛ #-}

  module _ ⦃ ICId : Id-Intro C.Inner ⦄ where
    private
      module ICId = Id-Intro ICId

    C~-Id-Intro : Cong-Id-Intro C~
    C~-Id-Intro .Cong-Id-Intro.Id~ {A₁} {A₂} {x₁} {x₂} {y₁} {y₂} ∣ A~ ∣ ∣ x~ ∣ ∣ y~ ∣
      = ∣ CCCId-Elim-C.ap {A = T₃} (λ ((A , x) , y) → ICId.Id {A} x y) p₃ ∣
      where T₂ : CC.Ty
            T₂ = C.ty , C.tm
            p₂ : CC.Tm (CCId.Id {A = T₂} (A₁ , x₁) (A₂ , x₂))
            p₂ = x~

            T₃ : CCC.Ty
            T₃ = (C.ty , C.tm) , λ (A , _) → C.tm A
            p₃ : CCC.Tm (CCCId.Id {A = T₃} ((A₁ , x₁) , y₁) ((A₂ , x₂) , y₂))
            p₃ = JM.baseChange↑ (λ (A , x) → A) _ p₂ y~
    C~-Id-Intro .Cong-Id-Intro.idp~ ∣ A~ ∣ ∣ x~ ∣
      = ∣ CCId.ap {A = C.ty , C.tm} (λ (A , x) → _ , ICId.idp {A} {x}) x~ ∣



  -- ----- I gave up on the definition of the congruence over the elimination
  -- -----  structure, because of Agda performance issues with instance arguments.

  -- the : ∀ {i} (A : Set i) → A → A
  -- the A a = a

  -- module IsAcyclic-Id-Elim ⦃ ICId : Id-Intro C.Inner ⦄ ⦃ ICId-Elim-IC : Id-Elim C.Inner C.Inner ⦄ where
  --   private
  --     module ICId = Id-Intro ICId
  --     module ICId-Elim-IC = Id-Elim ICId-Elim-IC

  --   C~-Id-Elim : Cong-Id-Elim C~ IsAcyclic-Id-Intro.C~-Id-Intro
  --   C~-Id-Elim .Cong-Id-Elim.J~ {A₁} {A₂} {x₁} {x₂} {P₁} {P₂} {d₁} {d₂} {y₁} {y₂} {p₁} {p₂} ∣ A~ ∣ ∣ x~ ∣ P~ ∣ d~ ∣ ∣ y~ ∣ ∣ p~ ∣
  --     = ∥-∥-ap (CCCCCCId-Elim-CC.ap (λ (((((A , x) , P) , d) , y) , p) → (cpi.app (cpi.app P y) p , ICId-Elim-IC.J {A} {x} (λ (z , q) → cpi.app (cpi.app P z) q) d (y , p)))
  --                                   {x = ((((A₁ , x₁), cpi.lam λ z → cpi.lam λ q → P₁ (z , q)) , d₁) , y₁) , p₁}
  --                                   {y = ((((A₂ , x₂), cpi.lam λ z → cpi.lam λ q → P₂ (z , q)) , d₂) , y₂) , p₂})
  --              r₆
  --     where T₂ : CC.Ty
  --           T₂ = C.ty , C.tm
  --           r₂ : CC.Tm (CCId.Id {A = T₂} (A₁ , x₁) (A₂ , x₂))
  --           r₂ = x~

  --           i⊤ = IsSet-⊤ {lzero} {lzero}

  --           T₃ : CCC.Ty
  --           T₃ = T₂ , λ (A , x) → cpi.Π A λ z → cpi.Π (ICId.Id x z) λ q → C.ty
  --           r₃ : ∥ CCC.Tm (CCCId.Id {A = T₃} ((A₁ , x₁) , cpi.lam λ z → cpi.lam λ q → P₁ (z , q)) ((A₂ , x₂) , cpi.lam λ z → cpi.lam λ q → P₂ (z , q))) ∥
  --           r₃ = JM-funext' ⦃ IEPi = cpi.pi ⦄ λ z₁ z₂ z~ →
  --                ∥-∥-ap (λ x → {!!})
  --                (JM-funext' ⦃ IEPi = cpi.pi ⦄ {A = {!!}} {B = {!ICId.Id !}} λ q₁ q₂ q~ →
  --                ∥-∥-ap (λ x → {!!})
  --                (P~ ∣ z~ ∣ ∣ q~ ∣))

  --           T₄ : CCCC.Ty
  --           T₄ = T₃ , λ ((A , x) , P) → C.tm (cpi.app (cpi.app P x) ICId.idp)
  --           r₄ : ∥ CCCC.Tm (CCCCId.Id {A = T₄} (((A₁ , x₁) , cpi.lam λ z → cpi.lam λ q → P₁ (z , q)) , d₁) ((((A₂ , x₂) , cpi.lam λ z → cpi.lam λ q → P₂ (z , q))) , d₂)) ∥
  --           r₄ = {!!}

  --           T₅ : CCCCC.Ty
  --           T₅ = T₄ , λ (((A , x) , P) , d) → C.tm A

  --           T₆ : CCCCCC.Ty
  --           T₆ = T₅ , λ ((((A , x) , P) , d) , y) → C.tm (ICId.Id x y)

  --           r₆ = {!!}


  --   C~-Id-Elim .Cong-Id-Elim.J-β~ {A₁} {A₂} {x₁} {x₂} {P₁} {P₂} {d₁} {d₂} A~ x~ P~ d~ = cheatP