🚧 🦆 Inductive Types

[TOTBWF]

[favonia]

Can we replace all [FIXME] Basis.Basis.enact_rigid_... with explicit exception raising?

[TOTBWF]

The plan is to go back through once the rest of the work is done and actually implement those, so FIXME makes for an easy grep.

[TOTBWF]

So bundling up all of the individual motives is proving tricky! My initial plan was to use the classic

  infixl 2 _▶_
  data Con : Set where
    ∙   : Con
    _▶_ : Con → Ty → Con

  data Var : Con → Ty → Set where
    vz : ∀ {Γ A} → Var (Γ ▶ A) A
    vs : ∀ {Γ A B} → Var Γ A → Var (Γ ▶ B) A

and then have the bundle of motives be of the form

  Methods : ∀ {Γ} → Motive Γ → Set
  Methods {Γ} P = ∀ {A} (x : Var Γ A) → Method P (var x)

However, elaborating to this is an absolute nightmare, as the indexing in Var makes for a pretty gnarly elimination form. Therefore, it seems like a better idea to bundle these up using a sig instead, but that brings it's own host of issues. In particular, we need a way of taking some ctx and constructing a sig type. However, this ties quite nicely into the first class telescope stuff that's been on our collective minds, so it seems like we could get 2 birds with a single stone!