search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
25 stars 5 forks source link

Eliminators for Stdlib Data Typs #55

Open maxsnew opened 9 months ago

maxsnew commented 9 months ago

Cubical.Data.List and Cubical.Data.W.Indexed don't have eliminators defined in them, and they would be convenient to have. These would be analogous to https://github.com/agda/cubical/blob/master/Cubical/Data/Nat/Base.agda#L39