{-# OPTIONS --no-pattern-matching #-}
module theorem-3-1 where
open import agda.prelude
open import agda.postulates
open import agda.fibration
open import agda.exp-path
record IntUniv (C : ℘ Set → Set₁) : Set₃
where
open Fib₀ ℘ ℘` ℘`comp C
field
U : Set₂
El : Fib₀ U
code : {Γ : Set}(Φ : Fib₀ Γ) → Γ → U
Elcode : {Γ : Set}(Φ : Fib₀ Γ) → El [ code Φ ] ≡ Φ
fiberwise-fibrant-is-fibrant :
(P : ℘ Set)
(π : (i : 𝕀) → isFib ⊤ (λ _ → P i))
→
isFib 𝕀 P
fiberwise-fibrant-is-fibrant P π = subst (isFib 𝕀) u (snd Φ)
where
Φ : Fib₀ 𝕀
Φ = (El [ (λ i → code ((λ _ → P i) , π i) tt) ])
u : fst Φ ≡ P
u = funext (λ i → cong (λ x → fst x tt) (Elcode ((λ _ → P i) , π i)))
NoIntUniv :
(C : ℘ Set → Set₁)
(coe : (P : ℘ Set) → C P → P O → P I)
(O≡ : (i : 𝕀) → C (λ _ → O ≡ i))
→
IntUniv C → ⊥
NoIntUniv C coe O≡ iu = O≠I (coe P c refl)
where
P : ℘ Set
P i = O ≡ i
c : C P
c = IntUniv.fiberwise-fibrant-is-fibrant iu P (λ i _ → O≡ i) id
module NoIntCCHMUniv where
open import agda.cchm
coe :
{l : Level}
(P : ℘ (Set l))
(c : CCHM P)
→
P O → P I
coe P c x =
fst (c ⊥ cof⊥ (λ _ ()) (x , λ ()))
O≡ :
(i : 𝕀)
→
CCHM (λ _ → O ≡ i)
O≡ i _ _ _ a₀+ = (fst a₀+ , λ _ → uip)
NoIntCCHMUniv : IntUniv CCHM → ⊥
NoIntCCHMUniv iu = NoIntUniv CCHM coe O≡ iu
module NoIntCCTTUniv where
open import agda.cctt
coe :
{l : Level}
(P : ℘ (Set l))
(c : CCTT P)
→
P O → P I
coe P c x = fst (c ⊥ cof⊥ (λ _ ()) O x (λ ())) I
O≡ :
(i : 𝕀)
→
CCTT (λ _ → O ≡ i)
O≡ r φ cofφ t r' b text =
J (λ r₁ b₁ →
(t₁ : (i : 𝕀) → φ → O ≡ r₁) →
Σ ((x : 𝕀) → O ≡ r₁)
(λ f → Σ (f r' ≡ b₁) (λ _ → (j : 𝕀) (u : φ) → t₁ j u ≡ f j)))
(λ t → ((λ _ → refl)) , refl , (λ _ _ → uip)) b t
NoIntCCTTUniv : IntUniv CCTT → ⊥
NoIntCCTTUniv iu = NoIntUniv CCTT coe O≡ iu