{-# OPTIONS --rewriting #-}

module Pi  where

open import Equality
open import EquationalReasoning
open import Fibration
open import FunExt
open import Interval
open import Level
open import Path
open import Product

----------------------------------------------------------------------
-- Pi types
----------------------------------------------------------------------
Pi :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  (B : Σ Γ A → Set ℓ'')
  → ---------------------------
  Γ → Set (ℓ' ⊔ ℓ'')
Pi A B x = (a : A x) → B(x , a)

PiAct :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Σ Γ A → Set ℓ')
  {{_ : isFib B}}
  (x y : Γ)
  (p : x ~ y)
  → ------------------
  Pi A B x → Pi A B y
PiAct _ _ _ _ p f a = ~symm (~lift (~symm p) a) ∗ (f (~symm p ∗ a))

PiActId :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Σ Γ A → Set ℓ')
  {{_ : isFib B}}
  (x  : Γ)
  (f : (a : A x) → B(x , a))
  → ---------------------------
  f ~ PiAct A B x x (~refl x) f
PiActId A {{α}} B {{β}} x f =
  ~funext (λ a →
  path:
    f a
  ~[ ~substrefl β (f a) ]
    ~refl (x , a) ∗ f a
  ~[ ~cong (_∗ f a) (≡to~ (atInj refl)) ]
    ~symm (~cong (x ,_) (~refl a)) ∗ f a
  ~[ ~cong (λ{(b , q) → ~symm (~cong (x ,_) q) ∗ f b})
     (~contr (~substrefl α a)) ]
    ~symm (~cong (x ,_) (~substrefl α a)) ∗ f (~refl x ∗ a)
  ~[ ~cong (λ q → (~symm q) ∗ f (~refl x ∗ a)) (~symm (~liftrefl x a)) ] 
    ~symm (~lift (~refl x) a) ∗ f (~refl x ∗ a)
  ~[ ≡to~ (cong (λ q → ~symm (~lift q a) ∗ f (q ∗ a)) ~symmrefl) ]
    ~symm (~lift (~symm (~refl x)) a) ∗ f ((~symm (~refl x)) ∗ a)
  endp)

isFibPi :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Σ Γ A → Set ℓ')
  {{_ : isFib B}}
  → ------------------
  isFib (Pi A B)
isFibPi A B = (PiAct A B , PiActId A B)