{-# OPTIONS --rewriting #-}

module DisjointUnion  where

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

----------------------------------------------------------------------
-- Disjoint union types
----------------------------------------------------------------------
Sum :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  (B : Γ → Set ℓ'')
  → -------------------
  Γ → Set (ℓ' ⊔ ℓ'')
Sum A B x = A x ⊎ B x

SumAct :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Γ → Set ℓ'')
  {{_ : isFib B}}
  (x y : Γ)
  (p : x ~ y)
   → -------------------
   Sum A B x → Sum A B y
SumAct _ _ _ _ p (inl a) = inl (p ∗ a)
SumAct _ _ _ _ p (inr b) = inr (p ∗ b)

SumActId :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Γ → Set ℓ'')
  {{_ : isFib B}}
  (x  : Γ)
  (c : Sum A B x)
  → ----------------------------
  c ~ SumAct A B x x (~refl x) c
SumActId _ {{α}} _ _ (inl a) = ~cong inl (~substrefl α a)
SumActId _ _ {{β}} _ (inr b) = ~cong inr (~substrefl β b)


isFibSum :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Γ → Set ℓ'')
  {{_ : isFib B}}
  → ----------------
  isFib (Sum A B)
isFibSum A B = (SumAct A B , SumActId A B)