{-# OPTIONS --postfix-projections --prop #-}
module Pi-Tele 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
open import Pi as _

----------------------------------------------------------------
--- Derivation of Pi type structures on the join of families ---
----------------------------------------------------------------

module Pi-Tele-l {ie je} (E : Fam {ie} {je}) ⦃ EId : Id-Intro E ⦄ ⦃ EId-Elim-E : Id-Elim E E ⦄ {ic jc id jd} {C : Fam {ic} {jc}} {D : Fam {id} {jd}}
                 ⦃ CEPi : Pi C E ⦄ ⦃ DEPi : Pi D E ⦄ where
  private
    module E    = Fam E
    module EId  = IdM E _
    module CEPi = Pi CEPi
    module DEPi = Pi DEPi

  private
    instance
     Pi-Intro-∗-l : Pi-Intro (C ∗ D) E
     Pi-Intro-∗-l .Pi-Intro.Π (A , B) C = CEPi.Π A λ a → DEPi.Π (B a) λ b → C (a , b)
     Pi-Intro-∗-l .Pi-Intro.lam c = CEPi.lam λ a → DEPi.lam λ b → c (a , b)

     Pi-App-∗-l : Pi-App (C ∗ D) E
     Pi-App-∗-l .Pi-App.app f (a , b) = DEPi.app (CEPi.app f a) b
     Pi-App-∗-l .Pi-App.app-β {f = f} {a = (a , b)} = EId.trans (DEPi.happly CEPi.app-β b) DEPi.app-β

     Pi-Funext-Weak-∗-l : Pi-Funext-Weak (C ∗ D) E
     Pi-Funext-Weak-∗-l .Pi-Funext-Weak.funext {f = f} {g = g} x = CEPi.funext (CEPi.lam (λ a → DEPi.funext (DEPi.lam (λ b → DEPi.app (CEPi.app x a) b))))

     Pi-Funext-Weak-∗-l .Pi-Funext-Weak.happly-funext {A} {B} {f} {g} h = p where
       p₀ : ∀ a b → E.Tm (EId.Id (EId.ap (λ fg → DEPi.app (CEPi.app fg a) b)
                                         (CEPi.funext (CEPi.lam (λ a → DEPi.funext (DEPi.lam (λ b → DEPi.app (CEPi.app h a) b))))))
                                 (DEPi.app (CEPi.app h a) b))
       p₀ a b = EId.trans (EId.ap-∘ (λ k → CEPi.app k a) (λ k → DEPi.app k b))
                (EId.trans (EId.ap (EId.ap (λ k → DEPi.app k b)) (EId.trans (EId.sym CEPi.app-β) (EId.trans (CEPi.happly (CEPi.happly-funext _) _) CEPi.app-β)))
                (EId.trans (EId.sym DEPi.app-β) (EId.trans (DEPi.happly (DEPi.happly-funext _) _) DEPi.app-β)))

       p : E.Tm (EId.Id (CEPi.lam λ a → DEPi.lam λ b → EId.ap (λ fg → DEPi.app (CEPi.app fg a) b)
                                                              (CEPi.funext (CEPi.lam (λ a → DEPi.funext (DEPi.lam (λ b → DEPi.app (CEPi.app h a) b))))))
                        h)
       p = CEPi.funext (CEPi.lam λ a → EId.trans CEPi.app-β (DEPi.funext (DEPi.lam λ b → EId.trans DEPi.app-β (p₀ a b))))

     Pi-∗-l : Pi (C ∗ D) E
     Pi-∗-l .Pi.Pi-intro  = Pi-Intro-∗-l
     Pi-∗-l .Pi.Pi-app    = Pi-App-∗-l
     Pi-∗-l .Pi.Pi-funext = Pi-Funext-HO⇒Pi-Funext (Pi-Funext-Contr⇒Pi-Funext-HO (Pi-Funext-Weak⇒Pi-Funext-Contr Pi-Funext-Weak-∗-l))

module _ {ic jc id jd ie je} (C : Fam {ic} {jc}) (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄
         ⦃ CDPi : Pi C D ⦄ (E : Fam {ie} {je}) ⦃ EId : Id-Intro E ⦄ ⦃ DId-Elim-E : Id-Elim D E ⦄ ⦃ EId-Elim-E : Id-Elim E E ⦄ ⦃ EId-Elim-D : Id-Elim E D ⦄
         ⦃ CEPi : Pi C E ⦄ where
  private
    open Id-Tele-r D
    open Id-Tele-r E
    module C          = Fam C
    module D          = Fam D
    module E          = Fam E
    module DE         = Fam (D ∗ E)
    module EE         = Fam (E ∗ E)
    module CDPi       = Pi CDPi
    module CEPi       = Pi CEPi
    module DId        = IdM D _
    module DId-Elim-E = Id-ElimM D E _
    module EId        = IdM E _
    module DEId       = IdM (D ∗ E) _
    module EEId       = IdM (E ∗ E) _

    module CDPi-Funext-Contr = Pi-Funext-Contr (Pi-Funext-Weak⇒Pi-Funext-Contr (Pi-Funext⇒Pi-Funext-Weak CDPi.Pi-funext))
    module CEPi-Funext-Contr = Pi-Funext-Contr (Pi-Funext-Weak⇒Pi-Funext-Contr (Pi-Funext⇒Pi-Funext-Weak CEPi.Pi-funext))

  instance
    abstract
      Pi-Intro-∗-r : Pi-Intro C (D ∗ E)
      Pi-Intro-∗-r .Pi-Intro.Π A B = CDPi.Π A (λ a → B a .fst) , λ f → CEPi.Π A λ a → B a .snd (CDPi.app f a)
      Pi-Intro-∗-r .Pi-Intro.lam {B = B} b = CDPi.lam (λ a → b a .fst) , CEPi.lam λ a → DId-Elim-E.transp (λ c → B a .snd c) (b a .snd) (DId.sym CDPi.app-β)

      Pi-App-∗-r : Pi-App C (D ∗ E)
      Pi-App-∗-r .Pi-App.app (fd , fe) a = CDPi.app fd a , CEPi.app fe a
      Pi-App-∗-r .Pi-App.app-β {B = B} {a = a} = CDPi.app-β
                                               , EId.trans (EId.ap (λ k → DId-Elim-E.transp (B a .snd) k CDPi.app-β) CEPi.app-β) (EId.trans DId-Elim-E.transp-trans
                                                           (EId.trans (DId-Elim-E.ap (DId-Elim-E.transp _ _) (DId.trans-sym-l _)) DId-Elim-E.transp-β))

      private
        module Elim1 = Id-Elim-ParamM (D ∗ D) (E ∗ E) (D ∗ E) _
        module Elim2 = Id-ElimM (E ∗ E) (D ∗ E) _

      Pi-Funext-HO-∗-r : Pi-Funext-HO C (D ∗ E)
      Pi-Funext-HO-∗-r .Pi-Funext-HO.elim-Id {A = A} {B = B} {f = fd , fe} P d (gd , ge) (hd , he) = k where
        isContr-T' : EEId.isContr (CEPi.Π A (λ a → B a .snd (CDPi.app fd a)) , λ ge → CEPi.Π A (λ a → EId.Id _ (CEPi.app ge a)))
        isContr-T' = EEId.isContr-retract
                     (λ (ge , he) → ge , CEPi.lam (λ a → EId.trans (EId.trans (DId-Elim-E.ap (DId-Elim-E.transp (B a .snd) _) CDPi.app-β) DId-Elim-E.transp-β) (CEPi.app he a)))
                     (λ (ge , he) → ge , CEPi.lam (λ a → EId.trans (EId.sym (EId.trans (DId-Elim-E.ap (DId-Elim-E.transp (B a .snd) _) CDPi.app-β) DId-Elim-E.transp-β)) (CEPi.app he a)))
                     (λ (ge , he) → EId.idp , EId.trans EId.transp-β (CEPi.funext (CEPi.lam λ a → EId.trans CEPi.app-β (EId.trans (EId.ap (EId.trans _) CEPi.app-β) (EId.trans EId.trans-assoc
                       (EId.trans (EId.ap (λ k → EId.trans k (CEPi.app he a)) (EId.trans-sym-r _)) EId.trans-β-l))))))
                     (CEPi-Funext-Contr.isContr-T {f = fe})

        k₀ : ∀ ge he → DE.Tm (P (fd , ge) ((CDPi.lam λ _ → DId.idp) , he))
        k₀ ge he = Elim2.isContr-transp isContr-T'
                                        (λ (ge , he) → P (fd , ge) ((CDPi.lam λ _ → DId.idp) , he))
                                        (ge , he)
                                        d

        k : DE.Tm (P (gd , ge) (hd , he))
        k = Elim1.isContr-transp CDPi-Funext-Contr.isContr-T
                                 (λ (gd , hd) → (CEPi.Π A λ a → B a .snd (CDPi.app gd a)) , λ ge → CEPi.Π A λ a → DEId.Id (CDPi.app fd a , CEPi.app fe a) (CDPi.app gd a , CEPi.app ge a) .snd (CDPi.app hd a))
                                 (λ (gd , hd) (ge , he) → P (gd , ge) (hd , he))
                                 {x = (fd , CDPi.lam λ _ → DId.idp)} (gd , hd) (λ (ge , he) → k₀ ge he) (ge , he)
      Pi-Funext-HO-∗-r .Pi-Funext-HO.elim-Id-β P d = DEId.trans (Elim1.isContr-transp-β _ _ _ _ _) (Elim2.isContr-transp-β _ _ _)

      Pi-∗-r : Pi C (D ∗ E)
      Pi-∗-r .Pi.Pi-intro = Pi-Intro-∗-r
      Pi-∗-r .Pi.Pi-app = Pi-App-∗-r
      Pi-∗-r .Pi.Pi-funext = Pi-Funext-HO⇒Pi-Funext Pi-Funext-HO-∗-r