This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The homotopy preorder of types

module
  foundation.homotopy-preorder-of-types
  where
Imports 
open import foundation.dependent-pair-types
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