```------------------------------------------------------------------------
-- 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 : Set a

------------------------------------------------------------------------
-- H-levels

-- H-levels ("homotopy levels").

H-level : ℕ → Set ℓ → Set ℓ
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 _

-- An alternative definition.
--
-- 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′ : ℕ → Set ℓ → Set ℓ
H-level′ zero    A = Contractible A
H-level′ (suc n) A = (x y : A) → H-level′ n (x ≡ y)

-- Propositions are propositional types.

Proposition : (ℓ : Level) → Set (lsuc ℓ)
Proposition _ = ∃ Is-proposition

-- Types that are sets.

SET : (ℓ : Level) → Set (lsuc ℓ)
SET _ = ∃ Is-set

-- The underlying type.

Type : SET ℓ → 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′
```