Reed Mullanix

Type Theory/Category Theory

I like proof assistants and make them too!

Last Notes

2025-12-28 14:57:02 UTC

- reply

@nprofile…rrqe Yeah, elaboration on the fly is such a misfeature IMO. This becomes really apparent when you have to do any sort of heavy unification: a problem with bunch of unsolved constraints takes *much* longer to finish than one that has a solution!

2025-11-17 23:02:37 UTC

- reply

@nprofile…rrqe I think you run into trouble here.
What you've outlined is equivalent to pulling back Fam(C) along the inclusion `FinSet⁺ → Sets`. If we want the inclusion to preserve the initial object, then the constant family `Const 0 : [1] → C` has to be initial. However, there are two maps `Const 0 → Const 0 + Const 0`

2025-11-17 22:21:34 UTC

- reply

@nprofile…rrqe Very much so! The categories I'm looking to complete are the walking parallel arrow categories, so they are directed as well.

2025-11-17 22:15:34 UTC

Is there a clean way of completing a category $C$ with an initial object under *binary* coproducts such that the inclusion of $C$ into the completion preserves the initial object?

2025-10-08 19:53:21 UTC

Complexity theory is so cursed because people like to pretend that your model of computation doesn't matter so long as it's "reasonable" but like, it does??

2025-05-03 15:29:25 UTC

It’s sort of funny how HoTT-as-a-metatheory seems completely allergic to any sort of categorical homotopy theory. All the basic notions require your (∞,1) categories to have a _set_ of objects, which always ends up presenting some insurmountable barrier (or forcing you back to square 1 to build a universe of hSets that’s an hSet)