10 lines
360 B
Plaintext
10 lines
360 B
Plaintext
|
App. 2 in HoTT gives typing rule for pathJ including a computational
|
||
|
|
rule for it.
|
||
|
|
|
||
|
|
If you have this computational rule definitionally, then you wouldn't
|
||
|
|
need to use `pathJprop`.
|
||
|
|
|
||
|
|
In discussion-section I mention HITs. I should remove this or come up
|
||
|
|
with a more elaborate example of something you could do, e.g.
|
||
|
|
something with pushouts in the category of sets.
|