anuyts
anuyts
The file Control/Categorical/Functor.hs seems to require `PolyKinds` to be properly usable. Currently, when I query the kind `Control.Categorical.Functor.Functor` in ghci, I get this: ``` *Control.Categorical.Functor> :k Functor Functor :: (*...
### Checklist - [X] I have used the search function to see if someone else has already submitted the same feature request. - [X] I will describe the problem with...
Is cedille-mode supposed to work out-of-the-box after installing the Debian package? Nothing remarkable seems to be happening when I open a .ced file with emacs. (Ubuntu 18.04 LTS) When pressing...
For a while, I've been quite annoyed by the fact that in the following code, I cannot let Agda solve (C-c C-s) both goals below or just write underscores, even...
When a record (or data?) type is defined inside a module, and then one of its fields (or constructors?) is called outside the module, all module parameters are turned into...
What I'm going to write here is something between a feature request and a research proposal. One of the great advantages of cubical type theory is that the path type...
The following minimal example does _not_ cause a problem: ```agda {-# OPTIONS --cubical #-} open import Agda.Builtin.Cubical.Path open import Agda.Primitive.Cubical record _×_ (A B : Set) : Set where constructor...
Attempts to create a minimal example failed, so I'll have to refer to a bloated example. In [this commit](https://github.com/anuyts/cubical/tree/7005c82f), in [this file](https://github.com/anuyts/cubical/blob/7005c82f8fb593b20f703678014d825abf53d097/Cubical/Categories/Instances/FunctorAlgebras.agda), if you replace the line that says ```agda...
Generalize/factor definition of adjunction (as natural bijection) to include ad hoc (per-object) and relative adjoints.
List operations.