{-# OPTIONS --no-pattern-matching --rewriting #-}
open import agda.prelude
open import agda-flat.prelude
open import agda.fibration
module agda-flat.tiny
(℘ :{♭}
{l : Level}
(Γ : Set l)
→
Set l)
(℘` :{♭}
{l m : Level}
{Γ : Set l}
{Δ : Set m}
(γ : Δ → Γ)
→
℘ Δ → ℘ Γ)
(℘`comp :{♭}
{l m n : Level}
{Γ : Set l}
{Δ : Set m}
{Θ : Set n}
(γ : Δ → Γ)
(σ : Θ → Δ)
(p : ℘ Θ)
→
℘` γ (℘` σ p) ≡ ℘` (γ ∘ σ) p)
where
postulate
√ :
{l :{♭} Level}
(A :{♭} Set l)
→
Set l
R :
{l l' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
(f :{♭} ℘ A → B)
→
A → √ B
L :
{l l' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
(g :{♭} A → √ B)
→
℘ A → B
LR :
{l l' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
{f :{♭} ℘ A → B}
→
L (R f) ≡ f
RL :
{l l' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
{g :{♭} A → √ B}
→
R (L g) ≡ g
R℘ :
{l l' l'' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
{C :{♭} Set l''}
(g :{♭} A → B)
(f :{♭} ℘ B → C)
→
R (f ∘ ℘` g) ≡ R f ∘ g
{-# REWRITE LR RL #-}
L℘ :
{l l' l'' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
{C :{♭} Set l''}
(f :{♭} B → √ C)
(g :{♭} A → B)
→
L f ∘ ℘` g ≡ L (f ∘ g)
L℘ f g = cong♭ L (R℘ g (L f))
√` :
{l l' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
(f :{♭} A → B)
→
√ A → √ B
√` f = R (f ∘ L id)
√R :
{l l' l'' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
{C :{♭} Set l''}
(g :{♭} B → C)
(f :{♭} ℘ A → B)
→
√` g ∘ R f ≡ R (g ∘ f)
√R g f =
proof
R (g ∘ L id) ∘ R f
≡[ symm (R℘ (R f) (g ∘ L id)) ]
R (g ∘ L id ∘ ℘`(R f))
≡[ cong♭ (λ h → R (g ∘ h)) (L℘ id (R f)) ]
R (g ∘ f)
qed
L√ :
{l l' l'' :{♭} Level}
{A :{♭} Set l}
{B :{♭} Set l'}
{C :{♭} Set l''}
(g :{♭} B → C)
(f :{♭} A → √ B)
→
g ∘ L f ≡ L (√` g ∘ f)
L√ g f = cong♭ L (symm (√R g (L f)))