search

rzk-lang / sHoTT

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

Morphisms of Product Types #82

Closed nimarasekh closed 1 year ago

nimarasekh commented 1 year ago

Added Section to file 5 characterizing morphisms in product types as products of morphims

nimarasekh commented 1 year ago

I added a description of morphisms in products. This is not in the paper, but is implicitly in Proposition 8.21 of RS17. I thought it's useful to add it explicitly to Section 5, so it can be used in Section 8, but also other places?

jonweinb commented 1 year ago

Thank you!

This should also be an instance of the axiom of choice for shapes. It's certainly good to have a wrapper for that.

nimarasekh commented 1 year ago

Thank you!

This should also be an instance of the axiom of choice for shapes. It's certainly good to have a wrapper for that.

Yes, it should be (or rather it actually is according to the proof in 8.12). In discussions with Emily she suggested writing down a direct proof, cause really all you're doing is reshuffling the pairs.