Emily Riehl

Weird error message saying "expected a pattern"

1

I just submitted a draft pull request [#132 in the sHoTT repository](https://github.com/rzk-lang/sHoTT/pull/132) for the purposes of reporting a weird error message. At the end of the the propositions file there...

In the sHott library we have two closely related definitions: ``` #def Λ : (2 × 2) → TOPE := \ (t , s) → (s ≡ 0₂ ∨ t...

Linux binary does not work on Ubuntu 20.04

2

I can't tell whether the issue is with my computer or with the way I'm trying to typecheck in vscode or both. I can't find our previous discussion so I'm...

feat (Category Theory): redefine and extend mates

3

The mates bijection between natural transformations inhabiting a certain dual pairs of squares (the duality in the sense of a parallel pair of adjunctions) can be defined in a more...