issues
search
rzk-lang
/
sHoTT
Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44
stars
12
forks
source link
more on left orthogonal calculus
#123
Closed
TashiWalde
closed
1 year ago
TashiWalde
commented
1 year ago
Left orthogonal shape inclusions are closed under
transposing the two arguments in a subshape of a product of cubes
product from the right (previously only from the left)
pushout product from the left and right.
Left orthogonal shape inclusions are closed under