Differences

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

Link to this comparison view

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]]
Link to graph
Log In
Improvements of the human condition