Reed Mullanix

Yeah, I roughly see where I need to use the associators and unitors. The reason I am using this degenerate version is that during reflection, I plan on splitting the...

@sstucki This is great! I think we might have ourselves a solver pretty soon :). WRT commiting to the branch, this is the most annoying thing about git IMO. I'll...

Looks like using explicit equalities might be the right move after all. This lemma would be waaaaaay easier if we could pattern match on equality proofs. ``` invert-resp-≈ : ∀...

Ok, more progress. `⌊⌋-α` is done, and all that remains of the associator case is a gnarly reassociation. What are everyones thoughts on using the category tactic to implement this...

The proofs are finally done! Now all that remains is writing the reflection code, and figuring out what needs to get factored out. @sstucki After checking through the relevant sections...

Ok, I've done some more thinking on this, and I have a idea for how we can normalize non-discrete things. If we update our `Expr` to: ```agda data Expr :...

We can still represent those morphisms with this encoding actually! ``` example : ∀ {V W X Y Z} (f : W ⊗₀ X ⇒ Y) → (g : Z...

Yeah, that example worked out fine by coincidence. You run into trouble when you want to start composing onto associators/unitors. You were definitely right when you stated that the domain/codomain...

Ok, I have a possible solution: During reflection, we insert quoting/unquoting morphisms when needed: ``` quot : Expr A ((reify A) ′) unquot : Expr ((reify A) ′) A ```...

I've done a lot of stewing on this over the past 2 weeks, and I keep running into walls whenever I try to add non-structural morphisms. I think that this...