search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.26k stars 193 forks source link

The join construction #1239

Open Alizter opened 4 years ago

Alizter commented 4 years ago

With the merge of #1238 we should think about formalizing the Join construction. AFAIK this hasn't been done in any proof assistant apart from Arend.

spitters commented 4 years ago

@EgbertRijke will know more...

Alizter commented 4 years ago

Here is the formalization in Arend.

Alizter commented 3 years ago

Just noticed that we are using the join construction in Seperated.v: https://github.com/HoTT/HoTT/blob/79d57970d33eec1295126a779d2867c23e2d82e4/theories/Modalities/Separated.v#L194-L205 but we don't actually prove anything there. We should definitely prove this at some point.

jdchristensen commented 3 years ago

I also have work in progress that relies on the join construction. Incidentally, all of the above axioms follow from a more basic consequence of the join construction, which is the axiom I'm using in my work in progress:

Definition jc_surjection@{i j k} (A : Type@{i}) (X : Type@{j})
           (ls : IsLocallySmall@{i j k} 1 X)
           (f : A -> X) (s : IsSurjection@{k} f) : IsSmall@{i j} X.
Admitted.

IsLocallySmall@{i j k} 1 X means that the identity types of X are equivalent to types in the universe i.

To prove the things admitted above, just do the factorization in any universe, and use jc_surjection to replace the image by an equivalent small type.