Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
set_._hott [2014/11/11 22:30] nikolaj |
set_._hott [2016/01/16 18:27] nikolaj |
||
---|---|---|---|
Line 1: | Line 1: | ||
===== Set . HoTT ===== | ===== Set . HoTT ===== | ||
==== Type ==== | ==== Type ==== | ||
- | $isSet(A):={\large\Pi}_{x,y:A}\,isProp(Id_A(x,y))$ | + | ${\mathrm{isSet}}(A):={\large\Pi}_{x,y:A}\,isProp(Id_A(x,y))$ |
==== Discussion ==== | ==== Discussion ==== | ||
=== Elaboration === | === Elaboration === | ||
Line 7: | Line 7: | ||
=== Alternative definitions === | === Alternative definitions === | ||
- | $isSet(A):={\large\Pi}_{x,y:A}{\large\Pi}_{p,q:Id_A(x,y)}\,Id_{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)$ |
+ | |||
+ | ${\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 === | === Reference === | ||
==== Parents ==== | ==== Parents ==== | ||
=== Requirements === | === Requirements === | ||
- | [[Identity type]] | + | [[Mere proposition]] |