Homotopy Type Theory set > history (Rev #6, changes)

Showing changes from revision #5 to #6: Added | Removed | Changed



A set consists of

  • A type AA
  • A 0-truncator
    τ 0: (a:A) (b:A) (c:a=b)isProp (d:a=b)( (x:c=d)a (y:c=d)x= y b) \tau_0: \prod_{(a:A)} \prod_{(b:A)} \prod_{(c:a=b)} \mathrm{isProp}(a \prod_{(d:a=b)} = \sum_{(x:c=d)} b) \prod_{(y:c=d)} x=y

As univalent setoids

A set is a setoid TT where the canonical functions

a:T,b:Tidtoiso(a,b):(a= Tb)(ab)a:T, b:T \vdash idtoiso(a,b):(a =_T b) \to (a \equiv b)

are equivalences

p: a:A b:A(a= Tb)(ab)p: \prod_{a:A} \prod_{b:A} (a =_T b) \cong (a \equiv b)


See also


Revision on May 1, 2022 at 21:40:01 by Anonymous?. See the history of this page for a list of all contributions to it.