Post #2049524

2026-05-05 20:06 UTC

@amy @ncf @totbwf After looking at the gist I have a couple questions: 1. You write "types living in `Typeω` do not yet support the Kan operations `transp` and `hcomp`", and the last time I checked there was a similar message in the Agda documentation. I'm very curious what "yet" means in this context. The gist makes it sound infeasible at the moment, but the following paragraphs suggest there is reason to believe that these operations will eventually be worked out. Do you have thoughts in the direction of an implementation, or perhaps good pointers if one wished to take a stab at it? I've long wished to have a large path type, as it would allow for a nice implementation of large category theory. However, I don't have much experience with the Agda internals, so I do not know where to begin 2. Re "Rewrite rules are actually pretty useful!": The title of this section led me to believe that Mikan would encourage usage of rewrite rules, but the content of the section seems to suggest that rewrite rules must be dropped to preserve safety. Is this correct? Meaning that the correct interpretation of the second paragraph in this section is that in the absence of `--rewriting`, one can safely emulate their interface by using `J` on path constructors of a HIT? I have been working almost exclusively in the `--cubical` fragment of Agda, so I'm excited to see where this project goes! Best of luck!

Replies (1)

@totbwf@types.pl 2026-05-05 22:43

@stschaef @amy @ncf There are two things blocking Kan ops for Typeω. The first is a technical problem: for small hcomps, we can use universe polymorphism to have a single primitive `primHComp : ∀ {ℓ} {A : Type ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A`. This trick does not work for Typeωᵢ. Possible solutions are: (a) have universe polymorphism in Typeωᵢ which just kicks the problem up a dimension or (b) have users bind primitives for `primHCompω₀, primHCompω₁, ...` The second blocker is a somewhat sillier one: the 1lab actually relies on the fact that Typeω does not have Kan operations for performance reasons! In particular, we put some indexed inductives in Typeω to avoid generating the extra cubical code. This is definitely a capital-H Hack, but it does make a huge difference for performance. We have dropped support for rewrite rules (see https://codeberg.org/1lab/mikan/pulls/68). They are a really cool feature for transforming your proof assistant into another type theory, but they add a large amount of complexity and overhead.

Open ##2049527