 |
Post AvLnKl3Y1i9aJLBwSu by [email protected] |
 |
More posts by [email protected] |
|
Post #AvLnKkugYf43rr2reS by [email protected] |
|
0 likes, 0 repeats |
|
|
|
The Fundamental Lemma of transport along equivalences.Thread on HoTT/UF in the … |
|
|
|
Post #AvLnKl3Y1i9aJLBwSu by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo which language is that code on? |
|
|
|
Post #AvLnKl9DgcgsavqTJ2 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jesusmargar asks "which language is that code on?"The language is Ag… |
|
|
|
Post #AvLnKlJV4Ouj6oegKW by [email protected] |
|
0 likes, 0 repeats |
|
|
|
In the presence of univalence, we can transport along equivalences in the follo… |
|
|
|
Post #AvLnKlhbcmCEJZvvu4 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Because the above uses univalence as a hypothesis, it is difficult to reason wi… |
|
|
|
Post #AvLnKm5MCTC9VF2tvM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
The Fundamental Lemma of transport along equivalences says that, for any given … |
|
|
|
Post #AvLnKmTojWlEj6UR3A by [email protected] |
|
0 likes, 0 repeats |
|
|
|
I am not sure if this lemma has been formulated and proved before, but I won… |
|
|
|
Post #AvLnKmsdFGbty46FjE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
In the above, we discussed a particular kind of transport which we found to be … |
