Christian Sattler

The suggestion from the previous post doesn't work in the following example: ```agda postulate A : Set _,_,_ : (X : A → Set) (a : A) (x : X...

The proper solution is to use let-bindings instead of β-redexes. Consider a function F of arity I (finite total order). Consider a section (application with potential placeholders) F((a_i)_{i∈I}) where a_i...

Here is a smaller example of this bug. ```agda postulate A B : Set _&_ : A → A → B f : A → B f = _& {!!}...

Better example: ```agda postulate A : Set data _≡_ : (x y : A) → Set where refl : (a : A) → a ≡ a x : let P...

This is a scoping bug (even before type-checking). The precise desugaring of `a •_` is `λ b → a[weaken] • b` where `weaken` is the weakening substitution lifting `a` to...

Here is a version where the confluence check triggers an internal error similar to #7034. Maybe there is a connection? ```agda {-# OPTIONS --two-level --rewriting --confluence-check #-} module Issue7034-2 where...

> We could also have a declaration `higher-inductive` before the constructors (or maybe anywhere in the list), similar to the `record` flavors (like `no-eta-equality`). > > I suppose this declaration...

> So, maybe, > > ```agda > higher data Nat : Set > ... > higher data Nat : Set where -- higher is optional here > Z : ......

If we use "cubical data" as a keyword like that, I feel we would be forced to repeat it. I'm not a fan of repetition, so as a separate proposal,...

> Instead of `higher` or `cubical` one could perhaps use a more descriptive name which indicates that the type has an hcomp constructor, maybe simply `hcomp`: > > ```agda >...