Module prop::hott

Homotopy Type Theory

Notice! This module is experimental and in early stages of development.

This is a model of Homotopy Type Theory that attempts to be similar to the version in the standard HoTT book.

Structs

• Id
  Identity type.
• IsHType
  Whether some type is a homotopy proposition.
• Refl
  Reflexivity proof of identity type.

Functions

• ap_fun
  (f : x -> y) ⋀ id{x}(a, b) => id{y}(f(a), f(b)).
• ap_lam
  (f : x => y) ⋀ id{x}(a, b) => id{y}(f(a), f(b)).
• from_is_contr
  is_contr(a) => a.
• id_in_left_arg
  (id{x}(a, b) ⋀ id{x}(a, c)) => id{x}(c, b).
• id_in_right_arg
  (id{x}(a, b) ⋀ id{x}(b, c)) => id{x}(a, b).
• id_to_eq
  id{x}(a, b) => (a == b).
• id_ty
  (x : type(n)) ⋀ (a : x) ⋀ (b : x) => id{x}(a, b) : type(n).
• is_groupoid_to_id
  (is_groupoid(x) ⋀ (a : x) ⋀ (b : x) ⋀ (p : id{x}(a, b)) ⋀ (q : id{x}(a, b)) ⋀ (hp : id{id{x}(a, b)}(p, q)) ⋀ (hq : id{id{x}(a, b)}(p, a))) => id{id{id{x}(a, b)}(p, q)}(hp, hq).
• is_groupoid_to_is_set
  (is_groupoid(x) ⋀ (a : x) ⋀ (b : x)) => is_set(id{x}(a, b)).
• is_htype_to_id
  (is_htype(n+1, x) ⋀ (a : x) ⋀ (b : x)) => is_htype(n, id{x}(a, b)).
• is_prop_to_id
  (is_prop(x) ⋀ (a : x) ⋀ (b : x)) => id{x}(a, b).
• is_set_to_id
  (is_set(x) ⋀ (a : x) ⋀ (b : x) ⋀ (p : id{x}(a, b)) ⋀ (q : id{x}(a, b))) => id{id{x}(a, b)}(p, q).
• is_set_to_is_prop
  (is_set(x) ⋀ (a : x) ⋀ (b : x)) => is_prop(id{x}(a, b)).
• refl
  (a : x) => refl{x}(a) : id{x}(a, a).
• to_is_contr
  a => is_contr(a).
• true_is_contr
  is_contr(true).

Type Definitions

• IsContr
  Whether some type is a homotopy proposition of level 0.
• IsGroupoid
  Whether some type is a groupoid.
• IsNGroupoid
  Whether some type is a homotopy n-groupoid.
• IsProp
  Whether some type is a homotopy proposition of level 1.
• IsSet
  Whether some type is a homotopy proposition of level 2.