The join construction

[Alizter]

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]

@EgbertRijke will know more...

[Alizter]

Here is the formalization in Arend.

[Alizter]

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]

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.