{-# OPTIONS --rewriting #-}
open import agda.prelude
open import agda-flat.prelude
open import agda.postulates
open import agda.fibration
module theorem-5-2-relative
(U₀ :{♭} (l : Level) → Set (ℓ₂ ⊔ lsuc l))
(El₀ :{♭} {l : Level} → U₀ l → Set l)
(℘ :{♭}
{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)
(C :{♭} {l : Level} (P : ℘ (U₀ l)) → U₀ (ℓ₁ ⊔ l))
where
open import agda-flat.tiny ℘ ℘` ℘`comp
isFib₀ :
{l l' : Level}
(Γ : Set l')
(A : Γ → U₀ l)
→
Set (ℓ₁ ⊔ l ⊔ l')
isFib₀ Γ A = (p : ℘ Γ) → El₀ (C (℘` A p))
Fib₀ :
{l' : Level}
(l : Level)
(Γ : Set l')
→
Set (ℓ₂ ⊔ l' ⊔ lsuc l)
Fib₀ l Γ = Σ A ∶ (Γ → U₀ l), isFib₀ Γ A
infixl 5 _[_]
_[_] :
{l l' l'' : Level}
{Γ : Set l'}
{Γ' : Set l''}
(Φ : Fib₀ l Γ)
(γ : Γ' → Γ)
→
Fib₀ l Γ'
(A , α) [ γ ] = (A ∘ γ , α[γ]) where
α[γ] : isFib₀ _ (A ∘ γ)
α[γ] p' = subst (El₀ ∘ C) (℘`comp A γ p') (α (℘` γ p'))
Elt : (l :{♭} Level) → Set (ℓ₂ ⊔ lsuc l)
Elt l = Σ A ∶ (U₀ l) , El₀ A
pr₁ : {l :{♭} Level} → Elt l → U₀ l
pr₁ = fst
U : (l :{♭} Level) → Set (ℓ₂ ⊔ lsuc l)
U l = Σ X ∶ (U₀ l × √(Elt (ℓ₁ ⊔ l))) , √` pr₁ (snd X) ≡ R C (fst X)
π₁ : {l :{♭} Level} → U l → U₀ l
π₁ x = fst (fst x)
π₂ : {l :{♭} Level} → U l → √(Elt (ℓ₁ ⊔ l))
π₂ x = snd (fst x)
pr₁Lπ₂ :
{l :{♭} Level}
→
pr₁ ∘ L (π₂ {l}) ≡ C ∘ ℘` (π₁)
pr₁Lπ₂ =
proof
pr₁ ∘ L π₂
≡[ L√ pr₁ π₂ ]
L (√` pr₁ ∘ π₂)
≡[ cong♭ L (funext snd) ]
L (R (C) ∘ (π₁))
≡[ cong♭ L (symm (R℘ (π₁) (C))) ]
(C) ∘ ℘` (π₁)
qed
υ : {l :{♭} Level} → isFib₀ (U l) π₁
υ p = subst El₀ (cong (apply p) pr₁Lπ₂) (snd (L π₂ p))
Lπ₂ :
{l :{♭} Level}(p : ℘(U l))
→
L π₂ p ≡ (C (℘` π₁ p) , υ p)
Lπ₂ p = Σext ((cong (apply p) pr₁Lπ₂)) refl
El : {l :{♭} Level} → Fib₀ l (U l)
El = (π₁ , υ)
code :
{l1 l :{♭} Level}
{Γ :{♭} Set l1}
(Φ :{♭} Fib₀ l Γ)
→
Γ → U l
code {l1}{l} {Γ} Aα x = ((A x , f x) , cong (apply x) u)
where
A = fst Aα
α = snd Aα
f : Γ → √(Elt (ℓ₁ ⊔ l))
f = R ⟨ C ∘ ℘` A , α ⟩
u : √` pr₁ ∘ f ≡ R C ∘ A
u =
proof
√` pr₁ ∘ f
≡[ cong♭ R (symm (L√ pr₁ f)) ]
R (pr₁ ∘ ⟨ C ∘ ℘` A , α ⟩)
≡[ R℘ A C ]
R C ∘ A
qed
module _
{l1 :{♭} Level}
{l :{♭} Level}
{Γ :{♭} Set l1}
(Φ :{♭} Fib₀ l Γ)
where
υ∘℘`codeΦ : isFib₀ Γ (fst Φ)
υ∘℘`codeΦ p =
subst (El₀ ∘ C) (℘`comp π₁ (code Φ) p) (υ (℘` (code Φ) p))
υ∘℘code : υ∘℘`codeΦ ≡ snd Φ
υ∘℘code = funext (λ p → congsnd (v p) refl)
where
congsnd :
{l l' : Level}
{A : Set l}
{B : A → Set l'}
{z z' : Σ A B}
(p : z ≡ z')
(q : fst z ≡ fst z')
→
subst B q (snd z) ≡ snd z'
congsnd {B = B} {z} {z'} p q =
proof
subst B q (snd z)
≡[ cong (λ h → subst B h (snd z)) (uip {p = q} {cong fst p}) ]
subst B (cong fst p) (snd z)
≡[ symm (cong (λ h → h (snd z)) (subst-cong-assoc B fst p)) ]
subst (λ z₁ → B (fst z₁)) p (snd z)
≡[ congd snd p ]
snd z'
qed
A : Γ → U₀ l
A = fst Φ
α : isFib₀ Γ A
α = snd Φ
v :
(p : ℘ Γ)
→
(C (℘` A p) , υ∘℘`codeΦ p) ≡ (C (℘` A p) , α p)
v p =
proof
(C (℘` A p) , υ∘℘`codeΦ p)
≡[ symm (Σext (cong C (℘`comp π₁ (code Φ) p))
(symm (cong (λ f → f (υ (℘` (code Φ) p)))
(subst-cong-assoc El₀ C (℘`comp π₁ (code Φ) p))))) ]
(C (℘` π₁ (℘` (code Φ) p)) , υ (℘` (code Φ) p))
≡[ symm (Lπ₂ (℘`(code Φ) p)) ]
L π₂ (℘`(code Φ) p)
≡[ cong (apply p) (L℘ π₂ (code Φ)) ]
(C (℘` A p) , α p)
qed
Elcode : El [ code Φ ] ≡ Φ
Elcode = Σext refl υ∘℘code
code[] :
{l1 l2 l :{♭} Level}
{Γ :{♭} Set l1}
{Δ :{♭} Set l2}
(Φ :{♭} Fib₀ l Γ)
(γ :{♭} Δ → Γ)
(x : Δ)
→
code (Φ [ γ ]) x ≡ code Φ (γ x)
code[] {l = l} {Γ} Aα γ x = Σext (×ext refl (e x)) uip
where
A = fst Aα
α = snd Aα
RC℘` :
{l' :{♭} Level}
{Γ :{♭} Set l'}
(_ :{♭} Fib₀ l Γ)
→
Γ → √ (Elt (lsuc lzero ⊔ l))
RC℘` Bβ = R ⟨ C ∘ ℘`(fst Bβ) , snd Bβ ⟩
e :
(x : _ )
→
RC℘` (Aα [ γ ]) x ≡ RC℘` Aα (γ x)
e x = step₁ · step₂ where
step₁ : RC℘` (Aα [ γ ]) x ≡ R ⟨ C ∘ (℘` A) ∘ (℘` γ) , α ∘ ℘` γ ⟩ x
step₁ = cong♭ (λ X → R X x) (funext (λ p → symm (helper p)))
where
helper :
(p : ℘ _)
→
(C (℘` A (℘` γ p)) , α (℘` γ p)) ≡
(C (℘` (A ∘ γ) p) , snd (Aα [ γ ]) p)
helper p =
cong (λ x → (C (fst x) , snd x))
(Σext (℘`comp A γ p) refl)
step₂ : R ⟨ C ∘ (℘` A) ∘ (℘` γ) , α ∘ ℘` γ ⟩ x ≡ RC℘` Aα (γ x)
step₂ = cong♭ (apply x) (R℘ γ ⟨ C ∘ ℘` A , α ⟩)
codeEl≡id : {l :{♭} Level}(X : U l) → code El X ≡ X
codeEl≡id {l} X = Σext (cong (λ f → (π₁ X , f X)) u) uip
where
u : R ⟨ C ∘ ℘` π₁ , υ ⟩ ≡ π₂ {l}
u = cong♭ R (symm (funext Lπ₂))
codeEl :
{l1 l :{♭} Level}
{Γ :{♭} Set l1}
(γ :{♭} Γ → U l)
→
code (El [ γ ]) ≡ γ
codeEl γ = funext (λ x →
proof
code (El [ γ ]) x
≡[ code[] El γ x ]
code El (γ x)
≡[ codeEl≡id (γ x) ]
γ x
qed)
module UnivOverall (l :{♭} Level) where
U' :{♭} Set (ℓ₂ ⊔ lsuc l)
U' = U l
El' :{♭} Fib₀ l U'
El' = El
code' : {l1 :{♭} Level} {Γ :{♭} Set l1} (Φ :{♭} Fib₀ l Γ) → Γ → U'
code' = code
Elcode' : {l1 :{♭} Level} {Γ :{♭} Set l1} (Φ :{♭} Fib₀ l Γ) → El' [ code' Φ ] ≡ Φ
Elcode' = Elcode
codeEl' : {l1 :{♭} Level} {Γ :{♭} Set l1} (γ :{♭} Γ → U') → code' (El' [ γ ]) ≡ γ
codeEl' = codeEl