{-# OPTIONS --postfix-projections --prop #-}
module 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 _

---------------------------------
--- Pi introduction structure ---
---------------------------------
record Pi-Intro {ic jc id jd} (C : Fam {ic} {jc}) (D : Fam {id} {jd}) : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  private
    module C = Fam C
    module D = Fam D

  field Π : ∀ (A : C.Ty) (B : C.Tm A → D.Ty) → D.Ty
        lam : ∀ {A B} → ((a : C.Tm A) → D.Tm (B a)) → D.Tm (Π A B)

--------------------------------
--- Pi application structure ---
--------------------------------
record Pi-App {ic jc id jd} (C : Fam {ic} {jc})
               (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄
               ⦃ CDPi-Intro : Pi-Intro C D ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  private
    open Pi-Intro CDPi-Intro
    module C   = Fam C
    module D   = Fam D
    module DId = Id-Intro DId

  field app : ∀ {A B} (f : D.Tm (Π A B)) (a : C.Tm A) → D.Tm (B a)
        app-β : ∀ {A B} {f : (a : C.Tm A) → D.Tm (B a)} {a : C.Tm A} → D.Tm (DId.Id (app {B = B} (lam f) a) (f a))

------------------------------------------------------
--- Pi introduction structure with a strict β rule ---
------------------------------------------------------
record Pi-App-Strict {ic jc id jd} (C : Fam {ic} {jc}) (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ ⦃ CDPi-Intro : Pi-Intro C D ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  open Pi-Intro CDPi-Intro
  private
    module C   = Fam C
    module D   = Fam D
    module DId = IdM D _

  field app : ∀ {A B} (f : D.Tm (Π A B)) (a : C.Tm A) → D.Tm (B a)
        app-βₛ : ∀ {A B} {f : (a : C.Tm A) → D.Tm (B a)} {a : C.Tm A} → app {B = B} (lam f) a ≡ f a

  app-β : ∀ {A B} {f : (a : C.Tm A) → D.Tm (B a)} {a : C.Tm A} → D.Tm (DId.Id (app {B = B} (lam f) a) (f a))
  app-β {A} {B} {f} {a} = L.transp (λ z → D.Tm (DId.Id (app (lam f) a) z)) (app-βₛ {A} {B} {f} {a}) DId.idp

  instance
    Pi-App-Strict⇒Pi-App : Pi-App C D
    Pi-App-Strict⇒Pi-App .Pi-App.app   = app
    Pi-App-Strict⇒Pi-App .Pi-App.app-β = app-β

----------------------------------------------------------------------------------------
--- Several (mutually derivable) definitions of Pi extensionality structures:        ---
---   - Weak Pi extensionality structures                                            ---
---   - Pi extensionality structures                                                 ---
---   - Contractibility of the type (g : Π A B) × (Π A λ a → Id (app f a) (app g a)) ---
---   - Higher-order Pi extensionality structures                                    ---
----------------------------------------------------------------------------------------

record Pi-Funext-Weak {ic jc id jd} (C : Fam {ic} {jc})
                      (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ DId-ELim-D : Id-Elim D D ⦄
                      ⦃ CDPi-Intro : Pi-Intro C D ⦄ ⦃ CDPi-App : Pi-App C D ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  private
    open Pi-Intro CDPi-Intro
    open Pi-App CDPi-App
    module C   = Fam C
    module D   = Fam D
    module DId = IdM D _

  field funext : ∀ {A B} {f g : D.Tm (Π A B)} → D.Tm (Π A λ a → DId.Id (app f a) (app g a)) → D.Tm (DId.Id f g)

  happly : ∀ {A B} {f g : D.Tm (Π A B)} → D.Tm (DId.Id f g) → (a : C.Tm A) → D.Tm (DId.Id (app f a) (app g a))
  happly p a = DId.ap (λ fg → app fg a) p

  field happly-funext : ∀ {A B f} {g : D.Tm (Π A B)} h → D.Tm (DId.Id (lam (happly (funext {f = f} {g = g} h))) h)

record Pi-Funext {ic jc id jd} (C : Fam {ic} {jc})
               (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ DId-ELim-D : Id-Elim D D ⦄
               ⦃ CDPi-Intro : Pi-Intro C D ⦄ ⦃ CDPi-App : Pi-App C D ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  private
    open Pi-Intro CDPi-Intro
    open Pi-App CDPi-App
    module C   = Fam C
    module D   = Fam D
    module DId = IdM D _

  field funext : ∀ {A B} {f g : D.Tm (Π A B)} → D.Tm (Π A λ a → DId.Id (app f a) (app g a)) → D.Tm (DId.Id f g)
        funext-β : ∀ {A B} {f} → D.Tm (DId.Id (funext {A} {B} {f = f} (lam (λ a → DId.idp))) DId.idp)

  happly : ∀ {A B} {f g : D.Tm (Π A B)} → D.Tm (DId.Id f g) → (a : C.Tm A) → D.Tm (DId.Id (app f a) (app g a))
  happly p a = DId.ap (λ fg → app fg a) p

  happly-β : ∀ {A B} {f : D.Tm (Π A B)} {a : C.Tm A} → D.Tm (DId.Id (happly {f = f} DId.idp a) DId.idp)
  happly-β {A} {B} {f} {a} = DId.J-β

  eta : ∀ {A B} (f : D.Tm (Π A B)) → D.Tm (DId.Id (lam (app f)) f)
  eta f = funext (lam (λ a → app-β))

  xi : ∀ {A B} {f g : (a : C.Tm A) → D.Tm (B a)} (h : (a : C.Tm A) → D.Tm (DId.Id (f a) (g a))) → D.Tm (DId.Id (lam {B = B} f) (lam g))
  xi h = funext (lam (λ a → DId.trans app-β (DId.trans (h a) (DId.sym app-β))))

  xi-β : ∀ {A B  f} → D.Tm (DId.Id (xi {A} {B} {f} (λ a → DId.idp)) DId.idp)
  xi-β {A} {B} {f} = DId.trans (DId.ap funext (xi (λ a → DId.trans (DId.ap (DId.trans app-β) DId.trans-β-l) (DId.trans-sym-r _)))) funext-β

  field
    happly-funext : ∀ {A B f} {g : D.Tm (Π A B)} h → D.Tm (DId.Id (lam (happly (funext {f = f} {g = g} h))) h)
    happly-funext-β : ∀ {A B f} → D.Tm (DId.Id (happly-funext {A = A} {B = B} {f = f} {g = f} (lam (λ _ → DId.idp)))
                                               (xi (λ a → DId.trans (DId.ap (λ k → happly k a) funext-β) happly-β)))

record Pi-Funext-Contr {ic jc id jd} (C : Fam {ic} {jc}) (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ ⦃ CDPi-Intro : Pi-Intro C D ⦄ ⦃ CDPi-App : Pi-App C D ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  private
    open Pi-Intro CDPi-Intro
    open Pi-App CDPi-App
    open Id-Tele-r D
    module C    = Fam C
    module D    = Fam D
    module DId  = IdM D _
    module DD   = Fam (D ∗ D)
    module DDId = IdM (D ∗ D) ⦃ CId-Elim-C = Id-Elim-∗-l {C = D ∗ D} {D = D} {E = D} ⦄ _

  field isContr-T : ∀ {A B f} → DDId.isContr (Π A B , λ g → Π A (λ a → DId.Id (app f a) (app g a)))


record Pi-Funext-HO {ic jc id jd} (C : Fam {ic} {jc}) (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ ⦃ CDPi-Intro : Pi-Intro C D ⦄ ⦃ CDPi-App : Pi-App C D ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  private
    open Pi-Intro CDPi-Intro
    open Pi-App CDPi-App
    module C   = Fam C
    module D   = Fam D
    module DId = IdM D _

  field elim-Id : ∀ {A B} {f : D.Tm (Π A B)} (P : ∀ (g : D.Tm (Π A B)) (h : D.Tm (Π A λ a → DId.Id (app f a) (app g a))) → D.Ty)
                    (d : D.Tm (P f (lam λ _ → DId.idp)))
                    → ∀ g h → D.Tm (P g h)
        elim-Id-β : ∀ {A B} {f : D.Tm (Π A B)} (P : ∀ (g : D.Tm (Π A B)) (h : D.Tm (Π A λ a → DId.Id (app f a) (app g a))) → D.Ty)
                    (d : D.Tm (P f (lam λ _ → DId.idp)))
                    → D.Tm (DId.Id (elim-Id P d f (lam λ _ → DId.idp)) d)

module _ {ic jc id jd} {C : Fam {ic} {jc}} {D : Fam {id} {jd}} ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ ⦃ CDPi-Intro : Pi-Intro C D ⦄ ⦃ CDPi-App : Pi-App C D ⦄ where
  private
    open Pi-Intro CDPi-Intro
    open Pi-App CDPi-App
    open Id-Tele-r D
    module C           = Fam C
    module D           = Fam D
    module DId         = IdM D _
    module DDId        = IdM (D ∗ D) _
    module DDId-Elim-D = Id-ElimM (D ∗ D) D _

  module _ (CDPi-Funext : Pi-Funext C D) where
    open Pi-Funext CDPi-Funext
    Pi-Funext⇒Pi-Funext-Weak : Pi-Funext-Weak C D
    Pi-Funext⇒Pi-Funext-Weak .Pi-Funext-Weak.funext = funext
    Pi-Funext⇒Pi-Funext-Weak .Pi-Funext-Weak.happly-funext = happly-funext

  module _ (CDPi-Funext-Weak : Pi-Funext-Weak C D) where
    open Pi-Funext-Weak CDPi-Funext-Weak
    Pi-Funext-Weak⇒Pi-Funext-Contr : Pi-Funext-Contr C D
    Pi-Funext-Weak⇒Pi-Funext-Contr .Pi-Funext-Contr.isContr-T {A} {B} {f}
      = DDId.isContr-retract (λ (g , h) → g , lam λ a → happly h a)
                             (λ (g , h) → g , funext h)
                             (λ (g , h) → DId.idp , DId.trans DId.transp-β (happly-funext _))
                             (isContr-PathFrom f)

  module _ (CDPi-Funext-Contr : Pi-Funext-Contr C D) where
    open Pi-Funext-Contr CDPi-Funext-Contr
    Pi-Funext-Contr⇒Pi-Funext-HO : Pi-Funext-HO C D
    Pi-Funext-Contr⇒Pi-Funext-HO .Pi-Funext-HO.elim-Id P d g h
      = DDId-Elim-D.isContr-transp isContr-T (λ (g , h) → P g h) (g , h) d
    Pi-Funext-Contr⇒Pi-Funext-HO .Pi-Funext-HO.elim-Id-β P d
      = DDId-Elim-D.isContr-transp-β _ _ _

  module _ (CDPi-Funext-HO : Pi-Funext-HO C D) where
    open Pi-Funext-HO CDPi-Funext-HO

    private
      happly : ∀ {A B} {f g : D.Tm (Π A B)} → D.Tm (DId.Id f g) → (a : C.Tm A) → D.Tm (DId.Id (app f a) (app g a))
      happly p a = DId.ap (λ fg → app fg a) p

      happly-β : ∀ {A B} {f : D.Tm (Π A B)} {a : C.Tm A} → D.Tm (DId.Id (happly {f = f} DId.idp a) DId.idp)
      happly-β {A} {B} {f} {a} = DId.J-β

      funext : ∀ {A B} {f g : D.Tm (Π A B)} → D.Tm (Π A λ a → DId.Id (app f a) (app g a)) → D.Tm (DId.Id f g)
      funext {f = f} {g = g} h = elim-Id (λ g h → DId.Id f g) DId.idp g h

      funext-β : ∀ {A B} {f} → D.Tm (DId.Id (funext {A} {B} {f = f} {g = f} (lam (λ a → DId.idp))) DId.idp)
      funext-β = elim-Id-β _ _

      xi : ∀ {A B} {f g : (a : C.Tm A) → D.Tm (B a)} (h : (a : C.Tm A) → D.Tm (DId.Id (f a) (g a))) → D.Tm (DId.Id (lam {B = B} f) (lam g))
      xi h = funext (lam (λ a → DId.trans app-β (DId.trans (h a) (DId.sym app-β))))

    Pi-Funext-HO⇒Pi-Funext : Pi-Funext C D
    Pi-Funext-HO⇒Pi-Funext .Pi-Funext.funext {A} {B} {f} {g} h = funext {f = f} {g = g} h
    Pi-Funext-HO⇒Pi-Funext .Pi-Funext.funext-β {A} {B} {f} = funext-β
    Pi-Funext-HO⇒Pi-Funext .Pi-Funext.happly-funext {A} {B} {f} {g} h
      = elim-Id (λ g h → DId.Id (lam (happly (funext {f = f} {g = g} h))) h) (xi (λ a → DId.trans (DId.ap (λ k → happly k a) funext-β) happly-β)) g h
    Pi-Funext-HO⇒Pi-Funext .Pi-Funext.happly-funext-β {A} {B} {f} = elim-Id-β _ _

------------------------------
--- Full Pi type structure ---
------------------------------
record Pi {ic jc id jd} (C : Fam {ic} {jc}) (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  private
    module DId = IdM D _
  field
    instance
      Pi-intro : Pi-Intro C D
      Pi-app : Pi-App C D ⦃ CDPi-Intro = Pi-intro ⦄
      Pi-funext : Pi-Funext C D ⦃ CDPi-Intro = Pi-intro ⦄ ⦃ CDPi-App = Pi-app ⦄
  open Pi-Intro Pi-intro public
  open Pi-App Pi-app public
  open Pi-Funext Pi-funext public
  open Pi-Funext-Contr (Pi-Funext-Weak⇒Pi-Funext-Contr (Pi-Funext⇒Pi-Funext-Weak Pi-funext)) public

  module Instances where
    instance
      IsSet-Π : ∀ {A B} → ⦃ IsSet-B : ∀ {a} → DId.IsSet (B a) ⦄ → DId.IsSet (Π A B)
      IsSet-Π = cheat

---------------------------------------------------
--- Full Pi type structure with a strict β rule ---
---------------------------------------------------
record Pi-StrictBeta {ic jc id jd} (C : Fam {ic} {jc}) (D : Fam {id} {jd}) ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ : Set (ic ⊔ jc ⊔ id ⊔ jd) where
  field
    instance
      Pi-intro : Pi-Intro C D
      Pi-app-strict : Pi-App-Strict C D ⦃ CDPi-Intro = Pi-intro ⦄
      Pi-funext : Pi-Funext C D ⦃ CDPi-Intro = Pi-intro ⦄ ⦃ CDPi-App = Pi-App-Strict.Pi-App-Strict⇒Pi-App ⦃ CDPi-Intro = Pi-intro ⦄ Pi-app-strict ⦄
  pi : Pi C D
  pi .Pi.Pi-intro = Pi-intro
  pi .Pi.Pi-app = _
  pi .Pi.Pi-funext = Pi-funext

  open Pi-Intro Pi-intro public
  open Pi-App-Strict Pi-app-strict public
  open Pi-Funext Pi-funext public
  open Pi-Funext-Contr (Pi-Funext-Weak⇒Pi-Funext-Contr (Pi-Funext⇒Pi-Funext-Weak Pi-funext)) public