Evan Cavallo
Evan Cavallo
In case it's useful for diagnosis, I'll repeat the observation from #250 that times can vary drastically depending on how one composes.
In the place you are using `helper`, are the paths `abxy` and `baxy` actually of type `path (path A (abx 0) (abx 1)) abx aby` and `path (path A (abx...
If they do have those stronger types, then this should work: ``` def help (A : type) (abx : 𝕀 → A) (aby : path A (abx 0) (abx 1))...
I too see no reason why it wouldn't work. 👍
Most things is fine.
Made a PR to add some explanation. The [1lab version](https://github.com/plt-amy/1lab/blob/main/src/1Lab/Reflection/Record.agda) might also be clearer, I didn't look closely.
Re: Axiom, the idea was that this would be the place to formulate principles like choice axioms or propositional resizing and prove relationships between them. The stdlib also has such...
Yeah, I think there's already a ``_$a_`` for algebras or something like that. For the graph homomorphisms it might be best to change it to match the Algebra conventions for...
Before we merge, we should have a plan for the changes coming in Agda 2.6.3. In 2.6.2, the interval is in your `Typeᵉ`, but in the development version it lives...
I suppose it would still be possible to use reflection to build the `Partial (i₁ ∨ ~ i₁ ∨ ... ∨ iₙ ∨ ~ iₙ) A` types?