Russoul/Nova

Design and implement indexed quotient inductive types

Russoul opened this issue · 0 comments

We already have a design ready borrowed mostly from the cubical generalisation/alternative. Iron it out and implement.