alternative defintion of slice and coslice as extension types

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

https://rzk-lang.github.io/sHoTT/

44 stars 12 forks source link

alternative defintion of slice and coslice as extension types #69

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

Define coslice' A a and slice A a as extension types (arrows in A with start/end a) and compare them to previous version (defined as total types of representables).

emilyriehl commented 1 year ago

Merging now but @TashiWalde is there an rzk issue you wanted to raise about the η-reduction?