{-# 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)