We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b37062c commit 25635d0Copy full SHA for 25635d0
src/Cat/Displayed/Cartesian/Joint.lagda.md
@@ -212,7 +212,7 @@ cartesian→jointly-cartesian {u = u} {f = f} ix-contr f-cart = f-joint-cart whe
212
f.unique other (p (ix-contr .centre))
213
```
214
215
-Conversely, if the constant family $\lambda i\. f$ is a jointly cartesian
+Conversely, if the constant family $\lambda i.\; f$ is a jointly cartesian
216
$I$-indexed family over a merely inhabited type $I$, then $f$ is cartesian.
217
218
```agda
0 commit comments