Fredrik Bakke
Fredrik Bakke
> > When I attempt to goto-definition, F12, on ≤-suc it only recognises ≤ or suc, wherever the cursor is currently over. > > This is because the language server...
We could reconcile 1 and 2 by introducing some modifier symbol like `ᴾ` for operators that take values in propositions. Although this does not feel very agda-unimathy to me, we...
I want to note that there is still a conflict that arises when considering the current usage of `∃`. There is also a conflict with the hypothetical `_∈_`. This leads...
We also do this for pointed types I just realized.
Here's an example usage for size: ```agda is-dedekind-cut-Prop : Prop (l1 ⊔ l2) is-dedekind-cut-Prop = ( ∃ᴾ ℚ L ∧ᴾ ∃ᴾ ℚ U) ∧ᴾ ( ∀ᴾ ℚ (λ q →...
Sentence-casing? :)
Oh, I thought the issue was about header capitalization. The issue does not specify.
Hey! I'd just like to note that the notion of isomorphisms in precategories is not incoherent. Rather, it is coherent, but the definition is only coherent for set-level structures and...
Oh, yes, I am not yet convinced by this idea either; I should have phrased the issue text differently. I still think this refactoring makes a lot of sense, though.
Feel free to edit the main comment btw!