Post #2049527

@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.