module Id.Tele where

open import Agda.Primitive
open import Lib
open import Fam as _

open import Id.Intro
open import Id.Elim
open import Id.Id

---------------------------------------------------------------------------------
--- Derivation of identity type elimination structure on the join of families ---
---------------------------------------------------------------------------------

module _ {C : Fam} ⦃ CId : Id-Intro C ⦄
         {D : Fam} ⦃ DId : Id-Intro D ⦄ ⦃ CId-Elim-D : Id-Elim C D ⦄ where
  private
    module C          = Fam C
    module CId        = Id-Intro CId
    module CId-Elim-D = Id-Elim CId-Elim-D
    module D          = Fam D
    module DId        = Id-Intro DId

  instance
    Id-Intro-∗ : Id-Intro (C ∗ D)
    Id-Intro-∗ .Id-Intro.Id (xc , xd) (yc , yd) = CId.Id xc yc , λ p → DId.Id (CId-Elim-D.transp _ xd p) yd
    Id-Intro-∗ .Id-Intro.idp = CId.idp , CId-Elim-D.transp-β

module Id-Tele-r (E : Fam) ⦃ EId : Id-Intro E ⦄ ⦃ EId-Elim-E : Id-Elim E E ⦄  where
  private
    module EId = IdM E _
  instance
    Id-Elim-⊤-r : Id-Elim Fam-⊤ E
    Id-Elim-⊤-r .Id-Elim.J P d yp = d
    Id-Elim-⊤-r .Id-Elim.J-β = EId.idp

  module _ {C : Fam} ⦃ CId : Id-Intro C ⦄
           {D : Fam} ⦃ DId : Id-Intro D ⦄ ⦃ CId-Elim-D : Id-Elim C D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄
           ⦃ CId-Elim-E : Id-Elim C E ⦄ ⦃ DId-Elim-E : Id-Elim D E ⦄ where
    private
      module C          = Fam C
      module CId        = Id-Intro CId
      module CId-Elim-D = Id-Elim CId-Elim-D
      module D          = Fam D
      module DId        = IdM D _
      module E          = Fam E
      module CId-Elim-E = Id-Elim CId-Elim-E
      module DId-Elim-E = Id-ElimM D E _
      module CDId       = Id-Intro (Id-Intro-∗ {C = C} {D = D})

    instance
      abstract
        Id-Elim-∗-r : Id-Elim (C ∗ D) E
        Id-Elim-∗-r = record { J = λ P d yp → d₅ _ _ _ _ P d yp
                             ; J-β = λ { {P = P} {d} → jβ _ _ _ _ P d } }
          where module _ (Ac : C.Ty) (Ad : C.Tm Ac → D.Ty) (xc : C.Tm Ac) (xd : D.Tm (Ad xc))
                         (P : CDId.IdFrom {A = Ac , Ad} (xc , xd) → E.Ty)
                         (d : E.Tm (P CDId.IdFrom-center)) where
                  tβ = CId-Elim-D.transp-β {d = _}
                  abstract
                    d₁ : E.Tm (P ((xc , _) , (CId.idp , DId.trans tβ DId.idp)))
                    d₁ = DId-Elim-E.transp (λ z → P ((xc , _) , _ , z)) d (DId.sym DId.trans-β-r)
                    d₂ : ∀ z q → E.Tm (P ((xc , z) , (CId.idp , DId.trans tβ (DId.trans (DId.sym tβ) q))))
                    d₂ z q = DId-Elim-E.J (λ (w , r) → P ((xc , w) , (CId.idp , DId.trans tβ r)))
                                          d₁
                                          (_ , DId.trans (DId.sym tβ) q)
                    d₂tβ : E.Tm (P ((xc , xd) , (CId.idp , DId.trans tβ (DId.trans (DId.sym tβ) tβ))))
                    d₂tβ = d₂ _ tβ
                    d₂β : E.Tm (EId.Id (d₂ _ tβ) (DId-Elim-E.transp (λ z → (P ((xc , _) , (_ , z)))) d₁ (DId.ap (DId.trans tβ) (DId.sym DId.trans-sym-l))))
                    d₂β = DId-Elim-E.J (λ (z , q) → EId.Id (DId-Elim-E.J (λ (w , r) → P ((xc , w) , (CId.idp , DId.trans tβ r))) d₁ (_ , z))
                                                           (DId-Elim-E.transp (λ z → (P ((xc , _) , (_ , z)))) d₁ (DId.ap (DId.trans tβ) q)))
                          (EId.trans DId-Elim-E.J-β (EId.sym (EId.trans (DId-Elim-E.ap (DId-Elim-E.transp (λ z → P ((xc , _) , _ , z)) _) DId.ap-β) DId-Elim-E.transp-β)))
                          (_ , DId.sym DId.trans-sym-l)
                    d₃ : ∀ z q → E.Tm (P ((xc , z) , (CId.idp , q)))
                    d₃ z q = DId-Elim-E.transp (λ z → P ((xc , _) , _ , z)) (d₂ z q)
                             (DId.trans DId.trans-assoc (DId.trans (DId.ap (λ a → DId.trans a q) DId.trans-sym-r) DId.trans-β-l))

                    d₄ : ∀ (yp : CId.IdFrom xc) → E.Tm (P (_ , (yp .snd , DId.idp)))
                    d₄ (_ , pc) = CId-Elim-E.J (λ (z , q) → P (_ , (q , DId.idp))) (d₃ _ _) (_ , pc)
                    d₅ : ∀ (yp : CDId.IdFrom (xc , xd)) → E.Tm (P (_ , (yp .snd .fst , yp .snd .snd)))
                    d₅ yp@(_ , (pc , pd)) = DId-Elim-E.J (λ (z , q) → P (_ , (pc , q))) (d₄ _) (_ , pd)

                    eq₁ : E.Tm (EId.Id (d₂ _ tβ)
                                        (DId-Elim-E.transp (λ z → P ((xc , _) , (_ , z))) d
                                          (DId.sym (DId.trans DId.trans-assoc (DId.trans (DId.ap (λ a → DId.trans a tβ) DId.trans-sym-r) DId.trans-β-l)))))
                    eq₁ = EId.trans d₂β (EId.trans DId-Elim-E.transp-trans (DId-Elim-E.ap (DId-Elim-E.transp _ d) (DId.trans-pentagon _)))
                    eq₂ : E.Tm (EId.Id (d₃ _ tβ) d)
                    eq₂ = EId.trans (EId.ap (λ k → DId-Elim-E.transp (λ z → P ((xc , _) , _ , z)) k (DId.trans DId.trans-assoc (DId.trans (DId.ap (λ a → DId.trans a tβ) DId.trans-sym-r) DId.trans-β-l))) eq₁)
                                     (EId.trans DId-Elim-E.transp-trans (EId.trans (DId-Elim-E.ap (λ k → DId-Elim-E.transp (λ z → P ((xc , _) , _ , z)) d k) DId.trans-sym-l)
                                     DId-Elim-E.transp-β))
                    eq₃ : E.Tm (EId.Id (DId-Elim-E.J (λ (z , q) → P ((_ , z) , (_ , q))) (d₃ _ _) (_ , tβ)) d)
                    eq₃ = EId.trans (DId-Elim-E.J (λ (z , q) → EId.Id (DId-Elim-E.J (λ (z , q) → P ((_ , z) , (_ , q))) (d₃ _ _) (z , q)) (d₃ z q))
                                                   DId-Elim-E.J-β (_ , tβ))
                                     eq₂
                    eq₄ : E.Tm (EId.Id (d₄ CId.IdFrom-center) (d₃ _ _))
                    eq₄ = CId-Elim-E.J-β
                    eq₅ : E.Tm (EId.Id (d₅ (_ , (CId.idp , CId-Elim-D.transp-β))) (DId-Elim-E.J (λ (z , q) → P ((_ , z) , (_ , q))) (d₃ _ _) (_ , CId-Elim-D.transp-β)))
                    eq₅ = DId-Elim-E.J (λ (z , q) → EId.Id (d₅ (_ , (CId.idp , q))) (DId-Elim-E.J (λ (z , q) → P ((_ , z) , (_ , q))) (d₃ _ _) (_ , q)))
                          (EId.trans DId-Elim-E.J-β(EId.trans eq₄ (EId.sym DId-Elim-E.J-β)))
                          (_ , CId-Elim-D.transp-β)
                    jβ : E.Tm (EId.Id (d₅ (_ , (CId.idp , CId-Elim-D.transp-β))) d)
                    jβ = EId.trans eq₅ eq₃

module _ {C : Fam} ⦃ CId : Id-Intro C ⦄ where
  instance
    Id-Elim-⊤-l : Id-Elim C Fam-⊤
    Id-Elim-⊤-l = _

module _ {C : Fam} ⦃ CId : Id-Intro C ⦄
         {D : Fam} ⦃ DId : Id-Intro D ⦄ ⦃ CId-Elim-D : Id-Elim C D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄
         {E : Fam} ⦃ EId : Id-Intro E ⦄ ⦃ CId-Elim-E : Id-Elim C E ⦄ ⦃ DId-Elim-E : Id-Elim D E ⦄ ⦃ EId-Elim-E : Id-Elim E E ⦄ where
  private
    module C          = Fam C
    module CId        = Id-Intro CId
    module CId-Elim-D = Id-Elim CId-Elim-D
    module D          = Fam D
    module DId        = IdM D _
    module E          = Fam E
    module CId-Elim-E = Id-Elim CId-Elim-E
    module DId-Elim-E = Id-ElimM D E _
    module EId        = IdM E _
    module CDId       = Id-Intro (Id-Intro-∗ {C = C} {D = D})

  instance
    abstract
      Id-Elim-∗-l : Id-Elim C (D ∗ E)
      Id-Elim-∗-l = record { J = λ P (d , e) yp → d₅ _ _ (fst ∘ P) (snd ∘ P) d e yp , e₅ _ _ (fst ∘ P) (snd ∘ P) d e yp
                           ; J-β = λ { {P = P} {d , e} → CId-Elim-D.J-β , eq₃ _ _ (fst ∘ P) (snd ∘ P) d e } }
        where module _ (A : C.Ty) (x : C.Tm A)
                       (Pd : CId.IdFrom x → D.Ty) (Pe : (yp : CId.IdFrom x) → D.Tm (Pd yp) → E.Ty)
                       (d : D.Tm (Pd CId.IdFrom-center)) (e : E.Tm (Pe CId.IdFrom-center d)) where
                d₅ : ∀ (yp : CId.IdFrom x) → D.Tm (Pd yp)
                d₅ (y , p) = CId-Elim-D.J Pd d (y , p)
                e₄ : ∀ z q → E.Tm (Pe _ z)
                e₄ z q = DId-Elim-E.transp (λ z → Pe CId.IdFrom-center z) e {y = z} q
                e₅ : ∀ (yp : CId.IdFrom x) → E.Tm (Pe yp (d₅ yp))
                e₅ (y , p) = CId-Elim-E.J (λ yp → Pe yp (d₅ yp)) (e₄ _ (DId.sym CId-Elim-D.J-β)) (y , p)

                eq₀ : E.Tm (EId.Id (DId-Elim-E.transp (Pe CId.IdFrom-center) (e₄ _ DId.idp) (DId.sym DId.idp)) e)
                eq₀ = DId-Elim-E.transp (λ z → EId.Id (DId-Elim-E.transp (Pe CId.IdFrom-center) (e₄ _ DId.idp) z) e)
                        (EId.trans DId-Elim-E.transp-β DId-Elim-E.transp-β) (DId.sym DId.sym-β)
                eq₁ : E.Tm (EId.Id (DId-Elim-E.transp (Pe CId.IdFrom-center) (e₄ (d₅ CId.IdFrom-center) (DId.sym CId-Elim-D.J-β)) (DId.sym (DId.sym CId-Elim-D.J-β))) e)
                eq₁ = DId-Elim-E.J (λ (_ , q) → EId.Id (DId-Elim-E.transp (Pe CId.IdFrom-center) (e₄ _ q) (DId.sym q)) e)
                        eq₀ (_ , _)
                eq₂ : E.Tm (EId.Id (DId-Elim-E.transp (Pe CId.IdFrom-center) (e₄ (d₅ CId.IdFrom-center) (DId.sym CId-Elim-D.J-β)) CId-Elim-D.J-β) e)
                eq₂ = DId-Elim-E.transp (λ z → EId.Id (DId-Elim-E.transp (Pe CId.IdFrom-center) (e₄ (d₅ CId.IdFrom-center) (DId.sym CId-Elim-D.J-β)) z) e)
                        eq₁ (DId.sym-sym _)
                eq₃ : E.Tm (EId.Id (DId-Elim-E.transp (Pe CId.IdFrom-center) (e₅ CId.IdFrom-center) CId-Elim-D.J-β) e)
                eq₃ = EId.transp (λ z → EId.Id (DId-Elim-E.transp (Pe CId.IdFrom-center) z CId-Elim-D.J-β) e)
                        eq₂ (EId.sym CId-Elim-E.J-β)

-----------------------------------------------------------------------------------
--- Derivation of identity type elimination structure on families of telescopes ---
-----------------------------------------------------------------------------------

module Id-Tele-Self (C : Fam) ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄ where
  private
    module C   = Fam C
    module CId = IdM C _

  Id-Intro-LIxTele : (n : ℕ) → Id-Intro (LIxTele n C)
  Id-Elim-LIxTele-Base : (n : ℕ) → Id-Elim (LIxTele n C) ⦃ CId = Id-Intro-LIxTele n ⦄ C

  Id-Intro-LIxTele zero    = _
  Id-Intro-LIxTele (suc n) = Id-Intro-∗ ⦃ CId = Id-Intro-LIxTele n ⦄ ⦃ CId-Elim-D = Id-Elim-LIxTele-Base n ⦄

  Id-Elim-LIxTele-Base zero    = record { J = λ P d yp → d ; J-β = CId.idp }
  Id-Elim-LIxTele-Base (suc n) = Id-Tele-r.Id-Elim-∗-r _ ⦃ CId = Id-Intro-LIxTele n ⦄ ⦃ CId-Elim-D = Id-Elim-LIxTele-Base n ⦄ ⦃ CId-Elim-E = Id-Elim-LIxTele-Base n ⦄

  Id-Elim-LIxTele : (n : ℕ) → (m : ℕ) → Id-Elim (LIxTele n C) ⦃ CId = Id-Intro-LIxTele n ⦄ (LIxTele m C) ⦃ DId = Id-Intro-LIxTele m ⦄
  Id-Elim-LIxTele n zero    = _
  Id-Elim-LIxTele n (suc m) = Id-Elim-∗-l ⦃ CId = Id-Intro-LIxTele n ⦄ ⦃ DId = Id-Intro-LIxTele m ⦄ ⦃ CId-Elim-D = Id-Elim-LIxTele n m ⦄
                                          ⦃ DId-Elim-D = Id-Elim-LIxTele m m ⦄ ⦃ CId-Elim-E = Id-Elim-LIxTele-Base n ⦄ ⦃ DId-Elim-E = Id-Elim-LIxTele-Base m ⦄
  Id-Elim-LIxTele-RBase : (n : ℕ) → Id-Elim C (LIxTele n C) ⦃ DId = Id-Intro-LIxTele n ⦄
  Id-Elim-LIxTele-RBase zero = _
  Id-Elim-LIxTele-RBase (suc n) = Id-Elim-∗-l ⦃ CId = CId ⦄ ⦃ DId = Id-Intro-LIxTele n ⦄ ⦃ CId-Elim-D = Id-Elim-LIxTele-RBase n ⦄ ⦃ DId-Elim-D = Id-Elim-LIxTele n n ⦄ ⦃ DId-Elim-E = Id-Elim-LIxTele-Base n ⦄

  Id-Intro-LIxTele₁ : (n : ℕ) → Id-Intro (LIxTele₁ n C)
  Id-Elim-LIxTele₁-Base : (n : ℕ) → Id-Elim (LIxTele₁ n C) ⦃ CId = Id-Intro-LIxTele₁ n ⦄ C

  Id-Intro-LIxTele₁ zero    = record { Id = λ {A} x y → CId.Id {A} x y ; idp = λ {A} {x} → CId.idp }
  Id-Intro-LIxTele₁ (suc n) = Id-Intro-∗ ⦃ CId = Id-Intro-LIxTele₁ n ⦄ ⦃ CId-Elim-D = Id-Elim-LIxTele₁-Base n ⦄

  Id-Elim-LIxTele₁-Base zero    = record { J = CId.J ; J-β = CId.J-β }
  Id-Elim-LIxTele₁-Base (suc n) = Id-Tele-r.Id-Elim-∗-r _ ⦃ CId = Id-Intro-LIxTele₁ n ⦄ ⦃ CId-Elim-D = Id-Elim-LIxTele₁-Base n ⦄ ⦃ CId-Elim-E = Id-Elim-LIxTele₁-Base n ⦄

  Id-Elim-LIxTele₁ : (n : ℕ) → (m : ℕ) → Id-Elim (LIxTele₁ n C) ⦃ CId = Id-Intro-LIxTele₁ n ⦄ (LIxTele₁ m C) ⦃ DId = Id-Intro-LIxTele₁ m ⦄
  Id-Elim-LIxTele₁ n zero    = let module E = Id-Elim ⦃ Id-Intro-LIxTele₁ n ⦄ (Id-Elim-LIxTele₁-Base n) in
                               record { J = λ P d yp → E.J (λ yp → P yp) d yp ; J-β = λ {A} {x} {P} {d} → E.J-β }
  Id-Elim-LIxTele₁ n (suc m) = Id-Elim-∗-l ⦃ CId = Id-Intro-LIxTele₁ n ⦄ ⦃ DId = Id-Intro-LIxTele₁ m ⦄ ⦃ CId-Elim-D = Id-Elim-LIxTele₁ n m ⦄
                                           ⦃ DId-Elim-D = Id-Elim-LIxTele₁ m m ⦄ ⦃ CId-Elim-E = Id-Elim-LIxTele₁-Base n ⦄ ⦃ DId-Elim-E = Id-Elim-LIxTele₁-Base m ⦄

module Id-Tele (C : Fam) ⦃ CId : Id-Intro C ⦄ {{CId-Elim-C : Id-Elim C C}}
               (D : Fam) ⦃ DId : Id-Intro D ⦄ {{CId-Elim-D : Id-Elim C D}} {{DId-Elim-D : Id-Elim D D}} where
  private
    module C        = Fam C
    module CId      = Id-Intro CId
    module DId      = Id-Intro DId
    module CId-Tele = Id-Tele-Self C
    module DId-Tele = Id-Tele-Self D

  Id-Elim-LIxTele-Base : (n : ℕ) → Id-Elim (LIxTele n C) ⦃ CId = CId-Tele.Id-Intro-LIxTele n ⦄ D ⦃ DId = DId ⦄
  Id-Elim-LIxTele-Base zero    = record { J = λ P d yp → d ; J-β = DId.idp }
  Id-Elim-LIxTele-Base (suc n) = Id-Tele-r.Id-Elim-∗-r _ ⦃ CId = CId-Tele.Id-Intro-LIxTele n ⦄ ⦃ CId-Elim-D = CId-Tele.Id-Elim-LIxTele-Base n ⦄ ⦃ CId-Elim-E = Id-Elim-LIxTele-Base n ⦄

  Id-Elim-LIxTele : (n : ℕ) → (m : ℕ) → Id-Elim (LIxTele n C) ⦃ CId = CId-Tele.Id-Intro-LIxTele n ⦄ (LIxTele m D) ⦃ DId = DId-Tele.Id-Intro-LIxTele m ⦄
  Id-Elim-LIxTele n zero    = _
  Id-Elim-LIxTele n (suc m) = Id-Elim-∗-l ⦃ CId = CId-Tele.Id-Intro-LIxTele n ⦄ ⦃ DId = DId-Tele.Id-Intro-LIxTele m ⦄ ⦃ CId-Elim-D = Id-Elim-LIxTele n m ⦄
                                          ⦃ DId-Elim-D = DId-Tele.Id-Elim-LIxTele m m ⦄ ⦃ CId-Elim-E = Id-Elim-LIxTele-Base n ⦄ ⦃ DId-Elim-E = DId-Tele.Id-Elim-LIxTele-Base m ⦄