search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

Local types terminal map #110

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

Characterize local types as those types A for which the terminal map A -> Unit is right orthogonal.

TashiWalde commented 1 year ago

@fredrik-bakke Is it ok if I go ahead and merge this PR now that all checkmarks are green? Or am I supposed to wait for someone else to do it?

fredrik-bakke commented 1 year ago

It can be merged now, I was just waiting to hear from you to merge it :)