```{-# OPTIONS --rewriting #-}

module Sigma  where

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

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

SigAct :
{ℓ ℓ' ℓ'' : Level}
{Γ : Set ℓ}
(A : Γ → Set ℓ')
{{_ : isFib A}}
(B : Σ Γ A → Set ℓ'')
{{_ : isFib B}}
(x y : Γ)
(p : x ~ y)
→ ---------------------------
Sig A B x → Sig A B y
SigAct _ _ _ _ p (a , b) = (p ∗ a , ~lift p a ∗ b)

~Σext :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
{x y : Γ}
(p : x ~ y)
{A : Γ → Set ℓ'}
{{_ : isFib A}}
(a : A x)
{b : A y}
(q : p ∗ a ~ b)
→ ---------------
(x , a) ~ (y , b)
~Σext {y = y} p a q = (~cong (y ,_) q) ∙ (~lift p a)

SigActId :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
(A : Γ → Set ℓ')
{{_ : isFib A}}
(B : Σ Γ A → Set ℓ')
{{_ : isFib B}}
(x  : Γ)
(c : Sig A B x)
→ ----------------------------
c ~ SigAct A B x x (~refl x) c
SigActId A {{α}} B {{β}} x (a , b) =
path:
(a , b)
~[ ~Σext (~substrefl α a) b (~refl ((~substrefl α a) ∗ b)) ]
(~refl x ∗ a , (~cong (x ,_) (~substrefl α a)) ∗ b)
~[ ~cong (λ q → (~refl x ∗ a , q ∗ b)) (~symm (~liftrefl x a)) ]
(~refl x ∗ a , (~lift (~refl x) a) ∗ b)
endp
where
instance
β' : isFib (λ (a : A x) → B (x , a))
fst β' _ _ q = ~subst β (~cong (x ,_) q)
snd β' _     = ~substrefl β

isFibSig :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
(A : Γ → Set ℓ')
{{_ : isFib A}}
(B : Σ Γ A → Set ℓ')
{{_ : isFib B}}
→ ------------------
isFib (Sig A B)
isFibSig A B = (SigAct A B , SigActId A B)
```