Set . HoTT

Type

${\mathrm{isSet}}(A):={\large\Pi}_{x,y:A}\,isProp(Id_A(x,y))$

Discussion

Elaboration

See the last lines of univalence axiom.

Alternative definitions

${\mathrm{isSet}}(A):={\large\Pi}_{x,y:A}\,{\large\Pi}_{p,q: {\mathrm {Id}}_A(x,y)}\,{\mathrm {Id}}_{{\mathrm {Id}}_A(x,y)}(p,q)$

${\mathrm{isSet}}(A):={\large\Pi}(x,y:A)\,{\large\Pi}(p,q: {\mathrm {Id}}_A(x,y))\,{\mathrm {Id}}_{{\mathrm {Id}}_A(x,y)}(p,q)$

Reference

Parents

Requirements

Link to graph
Log In
Improvements of the human condition