{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
module H-level
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open Derived-definitions-and-properties eq
open import Logical-equivalence hiding (id; _∘_)
open import Nat eq
open import Prelude
open import Surjection eq hiding (id; _∘_)
private
variable
a ℓ : Level
m n : ℕ
A B : Type a
H-level : ℕ → Type ℓ → Type ℓ
H-level zero A = Contractible A
H-level (suc zero) A = Is-proposition A
H-level (suc (suc n)) A = {x y : A} → H-level (suc n) (x ≡ y)
private
H-level-2≡Is-set : H-level 2 A ≡ Is-set A
H-level-2≡Is-set = refl _
For-iterated-equality : ℕ → (Type ℓ → Type ℓ) → (Type ℓ → Type ℓ)
For-iterated-equality zero P A = P A
For-iterated-equality (suc n) P A =
(x y : A) → For-iterated-equality n P (x ≡ y)
H-level′ : ℕ → Type ℓ → Type ℓ
H-level′ = flip For-iterated-equality Contractible
Proposition : (ℓ : Level) → Type (lsuc ℓ)
Proposition _ = ∃ Is-proposition
Set : (ℓ : Level) → Type (lsuc ℓ)
Set _ = ∃ Is-set
⌞_⌟ : Set ℓ → Type ℓ
⌞ A ⌟ = proj₁ A
mono₁′ : ∀ n → H-level′ n A → H-level′ (1 + n) A
mono₁′ (suc n) h x y = mono₁′ n (h x y)
mono₁′ {A} zero h x y = trivial x y , irr
where
trivial : (x y : A) → x ≡ y
trivial x y =
x ≡⟨ sym $ proj₂ h x ⟩
proj₁ h ≡⟨ proj₂ h y ⟩∎
y ∎
irr : (x≡y : x ≡ y) → trivial x y ≡ x≡y
irr = elim (λ {x y} x≡y → trivial x y ≡ x≡y)
(λ x → trans-symˡ (proj₂ h x))
H-level⇔H-level′ : H-level n A ⇔ H-level′ n A
H-level⇔H-level′ = record { to = to _; from = from _ }
where
to : ∀ n → H-level n A → H-level′ n A
to zero h = h
to (suc zero) h = λ x → mono₁′ 0 (x , h x) x
to (suc (suc n)) h = λ x y → to (suc n) h
from : ∀ n → H-level′ n A → H-level n A
from zero h = h
from (suc zero) h x y = proj₁ (h x y)
from (suc (suc n)) h {x} {y} = from (suc n) (h x y)
+⇒≡ : {x y : A} → H-level (suc n) A → H-level n (x ≡ y)
+⇒≡ h = _⇔_.from H-level⇔H-level′ $ _⇔_.to H-level⇔H-level′ h _ _
mono₁ : ∀ n → H-level n A → H-level (1 + n) A
mono₁ n =
_⇔_.from H-level⇔H-level′ ∘
mono₁′ n ∘
_⇔_.to H-level⇔H-level′
abstract
mono : m ≤ n → H-level m A → H-level n A
mono (≤-refl′ eq) = subst (λ n → H-level n _) eq
mono (≤-step′ m≤n eq) =
subst (λ n → H-level n _) eq ∘
mono₁ _ ∘
mono m≤n
⇒≡ : {x y : A} → ∀ n → H-level n A → H-level n (x ≡ y)
⇒≡ _ = +⇒≡ ∘ mono₁ _
[inhabited⇒contractible]⇒propositional :
(A → Contractible A) → Is-proposition A
[inhabited⇒contractible]⇒propositional h x = mono₁ 0 (h x) x
[inhabited⇒+]⇒+ : ∀ n → (A → H-level (1 + n) A) → H-level (1 + n) A
[inhabited⇒+]⇒+ n h =
_⇔_.from H-level⇔H-level′ λ x → _⇔_.to H-level⇔H-level′ (h x) x
2+⇔∀1+≡ :
∀ n → H-level (2 + n) A ⇔ ((x : A) → H-level (1 + n) (x ≡ x))
2+⇔∀1+≡ n = record
{ to = λ h _ → h
; from = λ h → [inhabited⇒+]⇒+ _
(elim (λ {x y} _ → H-level (1 + n) (x ≡ y)) h)
}
propositional⇒inhabited⇒contractible :
{@0 A : Type a} →
Is-proposition A → A → Contractible A
propositional⇒inhabited⇒contractible p x = (x , p x)
respects-surjection′ :
A ↠ B → ∀ n → H-level′ n A → H-level′ n B
respects-surjection′ A↠B zero (x , irr) = (to x , irr′)
where
open _↠_ A↠B
irr′ : ∀ y → to x ≡ y
irr′ = λ y →
to x ≡⟨ cong to (irr (from y)) ⟩
to (from y) ≡⟨ right-inverse-of y ⟩∎
y ∎
respects-surjection′ A↠B (suc n) h = λ x y →
respects-surjection′ (↠-≡ A↠B) n (h (from x) (from y))
where open _↠_ A↠B
respects-surjection :
A ↠ B → ∀ n → H-level n A → H-level n B
respects-surjection A↠B n =
_⇔_.from H-level⇔H-level′ ∘
respects-surjection′ A↠B n ∘
_⇔_.to H-level⇔H-level′