school/type-theory
2
0
Fork 0
Code Issues 11 Pull requests Projects 1 Releases Packages Wiki Activity Actions

details

Browse source
This commit is contained in:
Michael Zhang 2023-03-22 00:32:28 -05:00
parent d79909bfd6
commit 3f89a07add
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Path2.lagda.md
View file

@ -1,6 +1,8 @@
Path2
===
<details>
<summary>Basics (Path, transport, ap, etc.)</summary>
```
{-# OPTIONS --without-K --rewriting #-}
@ -70,6 +72,7 @@ apd {A} {B} f p = path-ind D d p
d : (x : A) → D x x (refl x)
d x = refl (f x)
```
</details>
```
-- Path products