We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 8686f08 commit 4322650Copy full SHA for 4322650
1 file changed
README.md
@@ -161,6 +161,12 @@ hcompⁱ (♭ A) [φ ↦ ♭-unit u] (♭-unit u₀) = ♭-unit (hcompⁱ A [φ
161
hсomp-Fillⁱ A [φ ↦ u] u₀ = hcompʲ A [φ ↦ u(i/i∧j), (i=0) ↦ u₀] u₀ : A
162
```
163
164
+Next Versions
165
+-------------
166
+
167
+* Simplicial Type Theory (Modal Pi and Twisted primitives)
168
+* Simplicial version of Yoneda Embedding
169
170
MLTT
171
----
172
0 commit comments