{-# OPTIONS --no-projection-like #-}
open import 1Lab.Path.Groupoid
open import 1Lab.Type.Sigma
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.HLevel.Closure where


Closure of h-levels🔗

private variable
ℓ ℓ' : Level
A B C : Type ℓ
F G : A → Type ℓ


When showing that a given type is a homotopy -type, it’s often possible to reason syntactically about the type formers which were used in the construction of This is fundamentally because the are closed under a variety of type-forming operations, and that fact boils down to the fact that, in a homotopy type theory, the structure of identity types tends to be “self-similar” — for example, paths between pairs are pairs of paths.

Split surjections and retractions🔗

The fundamental result that we will piggy-back to derive the closure of under various operations is that contractible types are closed under split surjections. Unfolding this, it says that if we have a map and a section assigning fibres of over each then is contractible whenever is.

The proof is a short calculation:

split-surjection→is-contr
: (f : A → B) (s : (b : B) → fibre f b)
→ is-contr A → is-contr B
split-surjection→is-contr f s c .centre  = f (c .centre)
split-surjection→is-contr f s c .paths x =
f (c .centre) ≡⟨ ap f (c .paths _) ⟩≡
f (s x .fst)  ≡⟨ s x .snd ⟩≡
x             ∎


Usually, the data of a split surjection is unpacked to talk about retractions instead. That is, instead of talking about a section of fibres, we unpack the components to mention the inverse map and the proof that

retract→is-contr
: (f : A → B) (g : B → A)
→ is-left-inverse f g → is-contr A → is-contr B
retract→is-contr f g h isC .centre = f (isC .centre)
retract→is-contr f g h isC .paths x =
f (isC .centre) ≡⟨ ap f (isC .paths _) ⟩≡
f (g x)         ≡⟨ h _ ⟩≡
x               ∎


Recalling that our hierarchy of has two base cases, if we are to show that all h-levels are closed under retractions, we should also repeat the argument above for propositions. This turns out to be no biggie, so that there is no impediment to starting the inductive proof.

retract→is-prop
: (f : A → B) (g : B → A) → is-left-inverse f g
→ is-prop A → is-prop B
retract→is-prop f g h propA x y =
x       ≡⟨ sym (h _) ⟩≡
f (g x) ≡⟨ ap f (propA _ _) ⟩≡
f (g y) ≡⟨ h _ ⟩≡
y       ∎

retract→is-hlevel
: (n : Nat) (f : A → B) (g : B → A)
→ is-left-inverse f g → is-hlevel A n → is-hlevel B n
retract→is-hlevel 0 = retract→is-contr
retract→is-hlevel 1 = retract→is-prop


In the inductive case, we show that a retraction induces retractions between path spaces: the map is a split surjection. The construction simply whiskers the proof with paths that cancel

retract→is-hlevel (suc (suc n)) f g h hlevel x y =
retract→is-hlevel (suc n) sect (ap g) inv (hlevel (g x) (g y)) where
sect : g x ≡ g y → x ≡ y
sect path =
x       ≡⟨ sym (h _) ⟩≡
f (g x) ≡⟨ ap f path ⟩≡
f (g y) ≡⟨ h _ ⟩≡
y       ∎


The proof that this function does invert ap g on the left is boring, but it consists mostly of symbol pushing. The only non-trivial step, and the key to the proof, is the theorem that homotopies behave like natural transformations: We can flip ap f (ap g path) and h y to get a pair of paths that annihilates on the left, and path on the right.

    inv : is-left-inverse sect (ap g)
inv path =
sym (h x) ∙ ap f (ap g path) ∙ h y ∙ refl ≡⟨ ap (λ e → sym (h _) ∙ _ ∙ e) (∙-idr (h _)) ⟩≡
sym (h x) ∙ ap f (ap g path) ∙ h y        ≡⟨ ap₂ _∙_ refl (sym (homotopy-natural h _)) ⟩≡
sym (h x) ∙ h x ∙ path                    ≡⟨ ∙-assoc _ _ _ ⟩≡
(sym (h x) ∙ h x) ∙ path                  ≡⟨ ap₂ _∙_ (∙-invl (h x)) refl ⟩≡
refl ∙ path                               ≡⟨ ∙-idl path ⟩≡
path                                      ∎


Isomorphisms and equivalences🔗

Even though we know that univalence implies that are closed under equivalences, this does not apply to types in different universe levels. However, the construction above does, since every equivalence, having a two-sided inverse, is a split surjection.

iso→is-hlevel : (n : Nat) (f : A → B) → is-iso f → is-hlevel A n → is-hlevel B n
iso→is-hlevel n f im = retract→is-hlevel n f g h
where open is-iso im renaming (inv to g ; rinv to h)

Iso→is-hlevel : (n : Nat) → Iso B A → is-hlevel A n → is-hlevel B n
Iso→is-hlevel n (f , im) = retract→is-hlevel n g f h
where open is-iso im renaming (inv to g ; linv to h)

equiv→is-hlevel : (n : Nat) (f : A → B) → is-equiv f → is-hlevel A n → is-hlevel B n
equiv→is-hlevel n f eqv = iso→is-hlevel n f (is-equiv→is-iso eqv)

Equiv→is-hlevel : (n : Nat) → (B ≃ A) → is-hlevel A n → is-hlevel B n
Equiv→is-hlevel n f = equiv→is-hlevel n _ (Equiv.inverse f .snd)


Functions into n-types🔗

We can now prove that the are closed under all type formers whose identity types are “self-similar”. While we have to handle the base cases ourselves, closure under retracts can take care of the inductive cases. Function extensionality implies that an identity between functions is a function into identities:

Π-is-hlevel : ∀ {a b} {A : Type a} {B : A → Type b}
→ (n : Nat) (Bhl : (x : A) → is-hlevel (B x) n)
→ is-hlevel ((x : A) → B x) n
Π-is-hlevel 0 bhl = record
{ paths = λ x i a → bhl _ .paths (x a) i
}
Π-is-hlevel 1 bhl f g i a = bhl a (f a) (g a) i
Π-is-hlevel (suc (suc n)) bhl f g = retract→is-hlevel (suc n)
funext happly (λ x → refl)
(Π-is-hlevel (suc n) λ x → bhl x (f x) (g x))

Π-is-hlevel'
: ∀ {a b} {A : Type a} {B : A → Type b}
→ (n : Nat) (Bhl : (x : A) → is-hlevel (B x) n)
→ is-hlevel ({x : A} → B x) n
Π-is-hlevel' n bhl = retract→is-hlevel n
(λ f {x} → f x) (λ f x → f) (λ _ → refl)
(Π-is-hlevel n bhl)

Π-is-hlevel²
: ∀ {a b c} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
→ (n : Nat) (Bhl : (x : A) (y : B x) → is-hlevel (C x y) n)
→ is-hlevel (∀ x y → C x y) n
Π-is-hlevel² n w = Π-is-hlevel n λ _ → Π-is-hlevel n (w _)

Π-is-hlevel²'
: ∀ {a b c} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
→ (n : Nat) (Bhl : (x : A) (y : B x) → is-hlevel (C x y) n)
→ is-hlevel (∀ {x y} → C x y) n
Π-is-hlevel²' n w = Π-is-hlevel' n λ _ → Π-is-hlevel' n (w _)

Π-is-hlevel³
: ∀ {a b c d} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
{D : ∀ a b → C a b → Type d}
→ (n : Nat) (Bhl : (x : A) (y : B x) (z : C x y) → is-hlevel (D x y z) n)
→ is-hlevel (∀ x y z → D x y z) n
Π-is-hlevel³ n w = Π-is-hlevel n λ _ → Π-is-hlevel² n (w _)

Π-is-hlevel³'
: ∀ {a b c d} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
{D : ∀ a b → C a b → Type d}
→ (n : Nat) (Bhl : (x : A) (y : B x) (z : C x y) → is-hlevel (D x y z) n)
→ is-hlevel (∀ {x y z} → D x y z) n
Π-is-hlevel³' n w = Π-is-hlevel' n λ _ → Π-is-hlevel²' n (w _)


By taking the codomain to be a constant family, we obtain that the are an exponential ideal: is an if is.

fun-is-hlevel : ∀ n → is-hlevel B n → is-hlevel (A → B) n
fun-is-hlevel n hl = Π-is-hlevel n λ _ → hl


Sums of n-types🔗

A similar argument, using the fact that paths between pairs are pairs of paths, shows that dependent sums are also closed under h-levels.

Σ-is-hlevel
: {B : A → Type ℓ'} (n : Nat)
→ is-hlevel A n → (∀ x → is-hlevel (B x) n)
→ is-hlevel (Σ A B) n
Σ-is-hlevel 0 acontr bcontr = record
{ centre = acontr .centre , bcontr _ .centre
; paths  = λ x → Σ-pathp
(acontr .paths _)
(is-prop→pathp (λ _ → is-contr→is-prop (bcontr _)) _ _)
}

Σ-is-hlevel 1 aprop bprop (a , b) (a' , b') i =
aprop a a' i , is-prop→pathp (λ i → bprop (aprop a a' i)) b b' i

Σ-is-hlevel {B = B} (suc (suc n)) h1 h2 (x , p) (y , q) =
iso→is-hlevel (suc n) _ (Σ-path-iso .snd) \$
Σ-is-hlevel (suc n) (h1 x y) λ x → h2 y (subst B x p) q


Analogous to the case of dependent products and functions, a non-dependent sum is a product.

×-is-hlevel : ∀ n → is-hlevel A n → is-hlevel B n → is-hlevel (A × B) n
×-is-hlevel n ahl bhl = Σ-is-hlevel n ahl (λ _ → bhl)


Similarly, Lift does not induce a change of h-levels, i.e. if is an in a universe then it’s also an in any successor universe:

opaque
Lift-is-hlevel : ∀ n → is-hlevel A n → is-hlevel (Lift ℓ' A) n
Lift-is-hlevel n a-hl = retract→is-hlevel n lift Lift.lower (λ _ → refl) a-hl

  Lift-is-hlevel' : ∀ n → is-hlevel (Lift ℓ' A) n → is-hlevel A n
Lift-is-hlevel' n lift-hl = retract→is-hlevel n Lift.lower lift (λ _ → refl) lift-hl


Finally, we’ll show that the fibres of a function between are themselves

fibre-is-hlevel
: ∀ n → is-hlevel A n → is-hlevel B n
→ (f : A → B) → ∀ b → is-hlevel (fibre f b) n
fibre-is-hlevel n Ah Bh f b = Σ-is-hlevel n Ah λ _ → Path-is-hlevel n Bh


Automation🔗

For the common case of proving that a composite type built out of pieces with a known h-level has that same h-level, we can apply the helpers above very uniformly. So uniformly, in fact, that Agda’s instance resolution mechanism can do it for us. However, since is-hlevel is a recursive definition which unfolds depending on the level, we must introduce a record wrapper around this type which prevents recursion. Otherwise we could not expect Agda to find instances in scope.

record H-Level {ℓ} (T : Type ℓ) (n : Nat) : Type ℓ where
constructor hlevel-instance
field
has-hlevel : is-hlevel T n


The canonical entry point for the search is hlevel, which turns an instance argument of H-Level to an actual usable witness. Note that the parameter is explicit: We can not expect Agda to recover from the expected type of the application.

hlevel : ∀ {ℓ} {T : Type ℓ} n ⦃ x : H-Level T n ⦄ → is-hlevel T n
hlevel n ⦃ x ⦄ = H-Level.has-hlevel x

private variable
S T : Type ℓ

module _ where
open H-Level
H-Level-is-prop : ∀ {n} → is-prop (H-Level T n)
H-Level-is-prop {n = n} x y i .has-hlevel =
is-hlevel-is-prop n (x .has-hlevel) (y .has-hlevel) i


Because of the way we set up our search, the “leaves” in the instance search must support offsetting the index by any positive number: Rather than defining an instance saying that e.g.  has h-level 2, we define an instance saying it has h-level for any choice of This is done using the basic-instance helper:

basic-instance : ∀ {ℓ} {T : Type ℓ} n → is-hlevel T n → ∀ {k} → H-Level T (n + k)
basic-instance {T = T} n hl {k} =
subst (H-Level T) (+-comm n k) (hlevel-instance (is-hlevel-+ n k hl))
where
+-comm : ∀ n k → k + n ≡ n + k
+-comm zero k = go k where
go : ∀ k → k + 0 ≡ k
go zero = refl
go (suc x) = ap suc (go x)
+-comm (suc n) k = go n k ∙ ap suc (+-comm n k) where
go : ∀ n k → k + suc n ≡ suc (k + n)
go n zero = refl
go n (suc k) = ap suc (go n k)

prop-instance : ∀ {ℓ} {T : Type ℓ} → is-prop T → ∀ {k} → H-Level T (suc k)
prop-instance {T = T} hl = hlevel-instance (is-prop→is-hlevel-suc hl)


We then have a family of instances for solving compound types, e.g. function types, path types, lifts, etc.

instance opaque
H-Level-pi
: ∀ {n} {S : T → Type ℓ}
→ ⦃ ∀ {x} → H-Level (S x) n ⦄
→ H-Level (∀ x → S x) n
H-Level-pi {n = n} .H-Level.has-hlevel = Π-is-hlevel n λ _ → hlevel n

H-Level-⊤ : ∀ {n} → H-Level ⊤ n
H-Level-⊤ {n = zero} = hlevel-instance (contr tt (λ x i → tt))
H-Level-⊤ {n = suc n} = prop-instance λ x y i → tt

H-Level-⊥ : ∀ {n} → H-Level ⊥ (suc n)
H-Level-⊥ {n = n} = prop-instance λ x y → absurd x

H-Level-pi'
: ∀ {n} {S : T → Type ℓ}
→ ⦃ ∀ {x} → H-Level (S x) n ⦄
→ H-Level (∀ {x} → S x) n
H-Level-pi' {n = n} .H-Level.has-hlevel = Π-is-hlevel' n λ _ → hlevel n

H-Level-sigma
: ∀ {n} {S : T → Type ℓ}
→ ⦃ H-Level T n ⦄ → ⦃ ∀ {x} → H-Level (S x) n ⦄
→ H-Level (Σ T S) n
H-Level-sigma {n = n} .H-Level.has-hlevel =
Σ-is-hlevel n (hlevel n) λ _ → hlevel n

H-Level-PathP
: ∀ {n} {S : I → Type ℓ} ⦃ s : H-Level (S i1) (suc n) ⦄ {x y}
→ H-Level (PathP S x y) n
H-Level-PathP {n = n} .H-Level.has-hlevel = PathP-is-hlevel' n (hlevel (suc n)) _ _

H-Level-Lift
: ∀ {n} ⦃ s : H-Level T n ⦄ → H-Level (Lift ℓ T) n
H-Level-Lift {n = n} .H-Level.has-hlevel = Lift-is-hlevel n (hlevel n)

H-Level-is-contr : ∀ {n} {ℓ} {T : Type ℓ} → H-Level (is-contr T) (suc n)
H-Level-is-contr = prop-instance is-contr-is-prop

H-Level-is-equiv
: ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {n}
→ H-Level (is-equiv f) (suc n)
H-Level-is-equiv = prop-instance (is-equiv-is-prop _)

positive-hlevel : ∀ {ℓ} (T : Type ℓ) → Nat → Type _
positive-hlevel T n = ∀ {k} → H-Level T (n + k)
{-# INLINE positive-hlevel #-}