# Differences

This shows you the differences between two versions of the page.

 set_._hott [2014/11/17 19:16]nikolaj set_._hott [2016/01/16 18:27] (current)nikolaj Both sides previous revision Previous revision 2016/01/16 18:27 nikolaj 2014/11/17 19:16 nikolaj 2014/11/11 22:30 nikolaj 2014/11/11 22:16 nikolaj 2014/11/11 22:16 nikolaj 2014/11/11 18:31 nikolaj 2014/11/10 21:12 nikolaj 2014/11/10 21:12 nikolaj 2014/11/10 20:03 nikolaj 2014/11/10 20:03 nikolaj 2014/11/10 20:03 nikolaj 2014/11/10 18:13 nikolaj created 2016/01/16 18:27 nikolaj 2014/11/17 19:16 nikolaj 2014/11/11 22:30 nikolaj 2014/11/11 22:16 nikolaj 2014/11/11 22:16 nikolaj 2014/11/11 18:31 nikolaj 2014/11/10 21:12 nikolaj 2014/11/10 21:12 nikolaj 2014/11/10 20:03 nikolaj 2014/11/10 20:03 nikolaj 2014/11/10 20:03 nikolaj 2014/11/10 18:13 nikolaj created 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 ===