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

Better Elimination principles for Local Sections? #70

Closed maxsnew closed 4 weeks ago

maxsnew commented 7 months ago

Constructions like elim in Cubical.Categories.Constructions.Free.Category.Quiver are naturally formulated as constructing a global section over the free category. We can use reindex to make an elim that constructs a global section but this involves transports, so we should consider making a version that uses Reindex.Eq for cases where the functor is definitionally functorial.

maxsnew commented 4 weeks ago

We can just do this as needed