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

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

----------------------------------
--- Acyclic higher congruences ---
----------------------------------

record IsAcyclic {i j} (C : TwoLevelFam {i} {j}) : Set (i ⊔ j) where
  private
    module C   = TwoLevelFam C
    module CId = IdM C.Outer ⦃ _ ⦄ ⦃ CId-Elim-C = C.OuterId-Elim ⦄ _

  field
    instance
      IsSet-ty : CId.IsSet C.ty
      IsSet-tm : ∀ {A} → CId.IsSet (C.tm A)

--------------------------------------------------------------------------------
--- Construction of an ordinary congruence from an acyclic higher congruence ---
--------------------------------------------------------------------------------
module IsAcyclic-Cong {i j} (C : TwoLevelFam {i} {j}) (IsAcyclic-C : IsAcyclic C) where
  private
    open IsAcyclic IsAcyclic-C
    module C           = TwoLevelFam C
    open Id-Tele-r C.Outer
    module OC          = Fam C.Outer
    module IC          = Fam C.Inner
    module CId         = IdM C.Outer _
    module CC          = Fam (C.Outer ∗ C.Outer)
    module CCId        = IdM (C.Outer ∗ C.Outer) _
    module CCId-Elim-C = Id-ElimM (C.Outer ∗ C.Outer) C.Outer _
    module CId-Elim-CC = Id-ElimM C.Outer (C.Outer ∗ C.Outer) _

    module CTele-Self  = Id-Tele-Self C.Outer

  C~pre : PreCong-Fam C.Inner
  C~pre .PreCong-Fam.Ty~ x y          = ∥ C.Tmᵒ (CId.Id x y) ∥
  C~pre .PreCong-Fam.Ty~R {A}         = ∣ CId.idp ∣
  C~pre .PreCong-Fam.Ty~S ∣ p ∣       = ∣ CId.sym p ∣
  C~pre .PreCong-Fam.Ty~T ∣ p ∣ ∣ q ∣ = ∣ CId.trans p q ∣

  C~pre .PreCong-Fam.Tm~ {A = A} {B = B} _ a b = ∥ CC.Tm (JM.Id C.tm a b) ∥
  C~pre .PreCong-Fam.Tm~R {A} {a}     = ∣ CCId.idp ∣
  C~pre .PreCong-Fam.Tm~S ∣ p ∣       = ∣ CCId.sym p ∣
  C~pre .PreCong-Fam.Tm~T ∣ p ∣ ∣ q ∣ = ∣ CCId.trans p q ∣

  C~pre .PreCong-Fam.Tm~fib ∣ p ∣ a   = ∣ CId.transp C.tm a p , ∣ p , CId.idp ∣ ∣

  tm⋆ : ∀ n → LIxTele n C.Inner .Fam.Ty → LIxTele n C.Outer .Fam.Ty
  tm⋆-eq : ∀ n A → LIxTele n C.Outer .Fam.Tm (tm⋆ n A) ≡ LIxTele n C.Inner .Fam.Tm A
  tm⋆ zero x = _
  tm⋆ (suc n) (A₁ , A₂) rewrite L.! (tm⋆-eq n A₁) = tm⋆ n A₁ , λ a → C.tm (A₂ a)
  tm⋆-eq zero A = refl
  tm⋆-eq (suc n) (A₁ , A₂) rewrite L.! (tm⋆-eq n A₁) = refl
  {-# REWRITE tm⋆-eq #-}
  postulate tm⋆-eq-refl : ∀ n A → tm⋆-eq n A ≡ refl
  {-# REWRITE tm⋆-eq-refl #-}

  IsSet-tm⋆ : ∀ {n A} → Id-Intro.IsSet (CTele-Self.Id-Intro-LIxTele n) (tm⋆ n A)
  IsSet-tm⋆ {zero} {A} = IsSet-⊤
  IsSet-tm⋆ {suc n} {A₁ , A₂}
    = IsSet-Σ ⦃ CId = CTele-Self.Id-Intro-LIxTele n ⦄ ⦃ CId-Elim-C = CTele-Self.Id-Elim-LIxTele n n ⦄ {D = C.Outer} ⦃ CId-Elim-D = CTele-Self.Id-Elim-LIxTele-Base n ⦄
              ⦃ DId-Elim-C = CTele-Self.Id-Elim-LIxTele-RBase n ⦄
              ⦃ IsSet-A = IsSet-tm⋆ {n} {A₁} ⦄

  Ty⋆~R : ∀ n A → PreCong-Fam.Ty⋆~ C~pre {n} A A
  Tm⋆~-out : ∀ n A x y → PreCong-Fam.Tm⋆~ C~pre {n} (Ty⋆~R n A) x y → ∥ LIxTele n C.Outer .Fam.Tm (CTele-Self.Id-Intro-LIxTele n .Id-Intro.Id {tm⋆ n A} x y) ∥
  Ty⋆~R zero    _         = tt
  Ty⋆~R (suc n) (A₁ , A₂) = Ty⋆~R n A₁ , λ γ δ x →
    let module E = Id-Elim ⦃ CTele-Self.Id-Intro-LIxTele n ⦄ (CTele-Self.Id-Elim-LIxTele n ) in
    ∥-∥-bind (Tm⋆~-out n A₁ _ _ x) λ p → ∣ E.ap (λ x → _ , A₂ x) p .snd ∣
  Tm⋆~-out zero A x y x₁ = ∣ tt ∣
  Tm⋆~-out (suc n) (A₁ , A₂) (x₁ , x₂) (y₁ , y₂) (p₁ , p₂)
    = ∥-∥-bind p₂ λ p₂ →
      ∥-∥-bind (Tm⋆~-out n A₁ x₁ y₁ p₁) λ kk →
      ∣ (let l = JM.baseChange↑ {C = C.Outer} {D = LIxTele n C.Outer} ⦃ DId = CTele-Self.Id-Intro-LIxTele n ⦄
                                ⦃ DId-Elim-D = CTele-Self.Id-Elim-LIxTele n n ⦄  ⦃ DId-Elim-C = CTele-Self.Id-Elim-LIxTele-Base n ⦄
                                ⦃ CId-Elim-D = CTele-Self.Id-Elim-LIxTele-RBase n ⦄ {E = C.Outer} ⦃ DId-Elim-E = CTele-Self.Id-Elim-LIxTele-Base n ⦄
                                ⦃ IsSet-A = IsSet-tm⋆ {n} {A₁} ⦄ A₂ C.tm kk p₂ in l) ∣

  C~-ap : ∀ n → PreCong-Ap C~pre n (λ {A} → Ty⋆~R n A)
  C~-ap n .PreCong-Ap.ap-Ty B p   =
    let module E = Id-Elim ⦃ CTele-Self.Id-Intro-LIxTele n ⦄ (CTele-Self.Id-Elim-LIxTele n ) in
    ∥-∥-bind (Tm⋆~-out n _ _ _ p) λ p →
    ∣ E.ap (λ x → _ , B x) p .snd ∣
  C~-ap n .PreCong-Ap.ap-Tm B b p =
    let module E₁ = Id-Elim ⦃ CTele-Self.Id-Intro-LIxTele n ⦄ (CTele-Self.Id-Elim-LIxTele n ) in
    let module E₂ = Id-Elim ⦃ CTele-Self.Id-Intro-LIxTele n ⦄ (CTele-Self.Id-Elim-LIxTele n ) in
    ∥-∥-bind (Tm⋆~-out n _ _ _ p) λ p →
    ∣ (let e = E₂.ap {B = (_ , λ _ → C.ty) , λ (_ , A) → C.tm A} (λ x → (_ , B x), b x) p
       in JM.baseChange↑ {C = C.Outer} {D = C.Outer} {E = Fam-⊤ ∗ C.Outer} ⦃ IsSet-B = IsSet-Σ ⦃ IsSet-A = IsSet-⊤ ⦄ ⦄
                          (λ A → _ , A) (λ (_ , A) → C.tm A) (E₁.ap (λ x → _ , B x) p .snd) e) ∣
  C~-ap n .PreCong-Ap.ap-next = C~-ap (suc n)

  C~ : Cong-Fam C.Inner
  C~ .Cong-Fam.C~ = C~pre
  C~ .Cong-Fam.C~-ap = C~-ap _