{-# 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 :
{ℓ ℓ' ℓ'' : 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)