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