The homotopy preorder of types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.
Last modified on 2026-05-02.

module
  foundation.homotopy-preorder-of-types
  where
Imports 
open import foundation.dependent-pair-types
open import foundation.dependent-products-propositions
open import foundation.empty-types
open import foundation.identity-types
open import foundation.mere-functions
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import order-theory.large-preorders
open import order-theory.posets
open import order-theory.preorders

Idea

The homotopy preorder of types is the (large) preorder whose objects are types, and whose ordering relation is defined by mere functions, i.e. by the propositional truncation of the function types:

  A ≤ B := ║(A → B)║₋₁.

Definitions

The large homotopy preorder of types

Homotopy-Type-Large-Preorder : Large-Preorder lsuc (_⊔_)
Homotopy-Type-Large-Preorder =
  λ where
  .type-Large-Preorder l → UU l
  .leq-prop-Large-Preorder → prop-mere-function
  .refl-leq-Large-Preorder → refl-mere-function
  .transitive-leq-Large-Preorder X Y Z → transitive-mere-function

The small homotopy preorder of types

Homotopy-Type-Preorder : (l : Level) → Preorder (lsuc l) l
Homotopy-Type-Preorder = preorder-Large-Preorder Homotopy-Type-Large-Preorder

Recent changes