search

rzk-lang / sHoTT

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

Embeddings and propositional fibers #132

Closed emilyriehl closed 1 year ago

emilyriehl commented 1 year ago

This proves that a function f : A -> B is an embedding iff its fibers are propositions.

It then considers a motivating example, the projection first : (Σ (x : A), P x) -> A where P is what I call a "predicate" but which elsewhere in this file is called a "propositional-family". We should discuss terminology. In Rijke, the Sigma type is called a "subtype."

The final result is the intended application, using inv-ap-is-emb to build an identification between terms in the subtype from an identification between their first components.

In trying to define this final function I encountered some weird error messages that I thought I should bring to @fizruk's attention. Thus this function is currently defined four times, two of which compile and two of which don't. Until that is resolved, this should be tagged as a draft pull request.

emilyriehl commented 1 year ago

For those following along at home the errors that @fizruk and I were discussing above have been resolved.