2
H-level
source link: http://www.cse.chalmers.se/~nad/listings/equality/H-level.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
H-level
------------------------------------------------------------------------ -- H-levels ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} -- Partly based on Voevodsky's work on so-called univalent -- foundations. 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-levels -- H-levels ("homotopy levels"). 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 -- Note that H-level 2 is a synonym for Is-set. H-level-2≡Is-set : H-level 2 A ≡ Is-set A H-level-2≡Is-set = refl _ -- For-iterated-equality n P A means that P holds for (equalities -- over)^n A. 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) -- An alternative definition of h-levels. -- -- In some cases this definition, with only two cases, is easier to -- use. In other cases the definition above, which is less complicated -- for positive h-levels, is easier to use. H-level′ : ℕ → Type ℓ → Type ℓ H-level′ = flip For-iterated-equality Contractible -- Propositions are propositional types. Proposition : (ℓ : Level) → Type (lsuc ℓ) Proposition _ = ∃ Is-proposition -- Types that are sets. Set : (ℓ : Level) → Type (lsuc ℓ) Set _ = ∃ Is-set -- The underlying type. ⌞_⌟ : Set ℓ → Type ℓ ⌞ A ⌟ = proj₁ A ------------------------------------------------------------------------ -- General properties -- H-level′ is upwards closed in its first argument. mono₁′ : ∀ n → H-level′ n A → H-level′ (1 + n) A mono₁′ (suc n) h x y = mono₁′ n (h x y) mono₁′ {A = 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 and H-level′ are pointwise logically equivalent. 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 = x} {y = y} = from (suc n) (h x y) -- If A has h-level 1 + n, then the types of equality proofs between -- elements of type A have h-level n. +⇒≡ : {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 _ _ -- H-level is upwards closed in its first argument. 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 -- If A has h-level n, then the types of equality proofs between -- elements of type A also have h-level n. ⇒≡ : {x y : A} → ∀ n → H-level n A → H-level n (x ≡ y) ⇒≡ _ = +⇒≡ ∘ mono₁ _ -- If something is contractible given the assumption that it is -- inhabited, then it is propositional. [inhabited⇒contractible]⇒propositional : (A → Contractible A) → Is-proposition A [inhabited⇒contractible]⇒propositional h x = mono₁ 0 (h x) x -- If something has h-level (1 + n) given the assumption that it is -- inhabited, then it has h-level (1 + n). [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 -- An alternative characterisation of sets and higher h-levels. -- -- This is Theorem 7.2.7 from the HoTT book. 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) } -- If a propositional type is inhabited, then it is contractible. propositional⇒inhabited⇒contractible : Is-proposition A → A → Contractible A propositional⇒inhabited⇒contractible p x = (x , p x) -- H-level′ n respects (split) surjections. 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 -- H-level n respects (split) surjections. 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′
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK