join construction #1860

Alizter · 2024-02-19T00:14:59Z

Here is a formalization of the basic results in the join construction. We can now construct essentially small homotopy images of maps and define the propositional truncation from simpler HITs.

This was quite tricky to formalize as I had to constantly wrestle with the universe constraints, but I managed to get somewhere in the end.

I've left this as a draft for now as it is missing the theory about image factorizations, embeddings etc. I'm looking to get some feedback on what I have so far before I continue.

Previous discussion on the join construction here:

The join construction #1239

TODO:

Move construction of propositional truncation to Metatheory
Add theory of Smallness.v from https://github.com/jdchristensen/NonAccessible/blob/main/Smallness.v?rgh-link-date=2024-02-19T00%3A54%3A15Z to library and rebase on that.
Fix universes for GraphQuotient
Address review comments

Signed-off-by: Ali Caglayan <[email protected]>

jdchristensen · 2024-02-19T00:48:39Z

theories/Homotopy/JoinConstruction.v

+  snrapply Join_rec.
+  - exact f.
+  - exact IHn.
+  - intros ? ?; nrapply path_ishprop; exact _.


This part could also use equiv_into_hprop from Join.Core.

jdchristensen · 2024-02-19T00:54:15Z

theories/Homotopy/JoinConstruction.v

+Definition himage@{i j} {A : Type@{i}} {B : Type@{j}} (f : A -> B) : Type@{j}
+  := {y : B & merely@{j j} (hfiber f y)}.
+
+(** ** Essentially Small and Locally Small Types *)


This might be a good time to merge the file https://github.com/jdchristensen/NonAccessible/blob/main/Smallness.v,
which proves a lot of things about smallness (but relies on the join construction stated as an axiom). We might want a folder with (a) a short file with the main definitions, like the beginning of Smallness.v, (b) a file containing this new material, (c) the rest of Smallness.v. Or maybe some other arrangement.

I can take the stuff that doesn't rely on the join construction first and rebase the work here on that. I'll do that in another PR.

This was done, but I guess I'll leave this unresolved until the commented out IsEssentiallySmall is removed.

theories/Homotopy/JoinConstruction.v

jdchristensen · 2024-02-19T01:03:30Z

theories/Homotopy/JoinConstruction.v

+Proof.
+  nrapply Pushout@{k k k k}.
+  - exact (pullback_pr1@{_ _ _ k} (f := f) (g := g)).
+  - exact (pullback_pr2@{_ _ _ k}(f := f) (g := g)).


Suggested change

- exact (pullback_pr2@{_ _ _ k}(f := f) (g := g)).

- exact (pullback_pr2@{_ _ _ k} (f := f) (g := g)).

jdchristensen · 2024-02-19T01:09:23Z

theories/Homotopy/JoinConstruction.v

+Definition himage@{i j} {A : Type@{i}} {B : Type@{j}} (f : A -> B) : Type@{j}
+  := {y : B & merely@{j j} (hfiber f y)}.


A priori, the image of a map from A : Type@{i} to B : Type@{j} should live in Type@{max(i,j)}. Here you constrain i <= j, but I don't think that makes sense for what could be a general definition.

Yes, that makes more sense.

jdchristensen · 2024-02-19T01:10:16Z

theories/Homotopy/JoinConstruction.v

+(** Instead of using the propositional truncation defined in Truncations.Core, we instead give a simpler definition here out of simple HITs. This way we can break dependencies and also manage universe levels better. *)
+(** TODO: this should be used in Truncations.Core instead of the other definition. *)
+
+Definition merely@{i j} (A : Type@{i}) : Type@{j}.


Shouldn't this just take one universe variable, with the output universe the same as the input universe?

I'm also not sure why this is needed. Can't you just use (Tr -1) from Truncations.Core? It's separately interesting that pushouts and sequential colimits suffice for defining propositional truncation, but for the goal of proving that appropriate images are small, it isn't needed. I'd be inclined to make this part a separate file, maybe in the metatheory folder. But I could be convinced otherwise.

My original thinking was that I wanted to make propositional truncations definable before we touch ReflectiveSubuniverse/ since Seperated.v would use it. I guess this isn't really necessary in the end. I'll move it to a metatheory file.

jdchristensen · 2024-02-19T01:11:31Z

theories/Homotopy/JoinConstruction.v

+Theorem isessentiallysmall_infinite_fiberwise_join_power@{u v k | u <= v, v < k}
+  `{Funext} {A : Type@{u}} {X : Type@{v}} (f : A -> X)
+  (ils_X : IsLocallySmall@{v k} X)
+  : IsEssentiallySmall@{v k} (himage@{u v} f).


I'm not sure why u and v are independent here. Shouldn't the constraint on how small A is (u) be the same as the constraint on how small the path types of B are (v)?

Also, this suffers from the same problems as the result about sigma types. It's a tautology and can be proved with exact (_; equiv_idmap).. And if you fix the universe variables, then the proof below won't go through, since it requires X to be small on the second line.

jdchristensen · 2024-02-19T01:22:16Z

theories/Homotopy/JoinConstruction.v

+Definition FiberwiseJoin@{a b x k}
+  {A : Type@{a}} {B : Type@{b}} (X : Type@{x}) (f : A -> X) (g : B -> X)
+  : Type@{k}.


I had to work a lot with fiberwise joins in work on projective spaces and tangent spaces (no public repo yet), and it was much cleaner there to work with type families instead of maps. Then the fiberwise join of P : X -> Type and Q : X -> Type is simply the pointwise join: fun x => Join (P x) (Q x). This gets rid of the things you had to deal with involving bundling of data. OTOH, it would mean having to take sigma types at the end. I think it's worth thinking about, though.

That sounds like a good idea. I didn't want to diverge too much from the setup in Egbert's thesis so I wasn't courageous enough to try defining fiberwise joins too differently. I think this is the better thing to do, as it means we can reuse stuff we have for Joins for the fiberwise version.

jdchristensen · 2024-02-19T01:22:34Z

It's great to see this! I've given it a quick look over, and can review again later, maybe after some restructuring.

One meta-comment is that we can't really trust this until the universe issues with GraphQuotient are worked out, since they put the result in the wrong universe, and the colimits defined here use that construction. I don't think there will be a problem, but technically speaking we can't consider this complete until that is resolved.

Another comment is that the parts of this file that are general facts about joins should probably go into the Join folder, in new or existing files.

jdchristensen · 2024-02-19T01:31:25Z

theories/Homotopy/JoinConstruction.v

+Definition isessentiallysmall_sigma@{u v k | u <= v, v < k}
+  `{Funext} (A : Type@{u}) (P : A -> Type@{v})
+  (ies_A : IsEssentiallySmall@{u k} A)
+  (ies_P : forall x, IsEssentiallySmall@{v k} (P x))
+  : IsEssentiallySmall@{v k} {x : A & P x}.


This something wrong here. You start with A in universe u, and also assume that A is u-small, which is automatic. Similarly, P lands in universe v, but you also assume that it is v small. Since u <= v, this result is then a tautology, and can be proved with exact (_; equiv_idmap).

Alizter · 2024-02-19T01:40:23Z

One meta-comment is that we can't really trust this until the universe issues with GraphQuotient are worked out, since they put the result in the wrong universe, and the colimits defined here use that construction. I don't think there will be a problem, but technically speaking we can't consider this complete until that is resolved.

FTR, when developing this file locally, it is based on top of my other patches, that includes the universe levels for GraphQuotient being fixed. So I am a little bit more certain the universes are correct here. However as you have noticed, my grip on the universe levels is not good and I probably have quite a few mistakes in this file.

Another comment is that the parts of this file that are general facts about joins should probably go into the Join folder, in new or existing files.

Yes, this is something that I need to do. One question I have about organisation is do we want the define the propositional truncation this way? I kept everything in one file to keep it mostly self contained, but ideally we would use the join construction in Seperated.v, I will have to think about how to organize things.

Alizter · 2024-02-19T18:55:22Z

It seems that 2 years ago I wrote a file called Metatheory/PropTrunc.v with the construction of propositional truncation using the join construction. I'd completely forgotten about that, so I don't need to do that.

…truction

jdchristensen · 2024-09-26T14:11:11Z

I've updated https://github.com/jdchristensen/NonAccessible to work with the current library. Part of the file Smallness.v from that repo has now been merged into Coq-HoTT via #1867 , and I've updated the remaining part of Smallness.v to work with the new naming and other conventions. The part of Smallness.v that remains is the part that depends on the join construction, so that's why I'm mentioning this in this PR.

Alizter · 2024-09-27T18:10:14Z

I've tried to update this PR using the new smallness stuff, but for whatever reason I cannot get the smallness of joins to typecheck. The statement is:

Global Instance issmall_join@{u k l big+ | k < big, u <= l, k <= l}
  (A : Type@{k}) (B : Type@{k})
  (sA : IsSmall@{u k} A) (sB : IsSmall@{u k} B)
  : IsSmall@{u k} (Join@{k k k} A B).
Proof.

But if you observe the term that fills it:

  Check( 
fun   (A : Type@{k}) (B : Type@{k})
  (sA : IsSmall@{u k} A) (sB : IsSmall@{u k} B)
=>   
    Build_IsSmall@{u k}
      (Join@{k k k} A B)
      (Join@{u u u} (smalltype@{u k} A) (smalltype@{u k} B))
      (equiv_functor_join@{u k u k l big}
      (equiv_smalltype@{u k} A : Equiv@{u k} _ _)
      (equiv_smalltype@{u k} B : Equiv@{u k} _ _)
    
  )).

It forces the universes u and k to be equal. I have no idea why it is being collapsed however.

FTR the universe big comes from the wildcat Type which stems from how we defined Join_rec. My intention for l was to be max(u,k) since I didn't want to impose any relations between them.

jdchristensen · 2024-09-27T20:57:01Z

I can see why it is happening, but can't find a simple solution.

The first thing is that Join@{u u l} is not definitionally equal to Join@{u u u}. And equiv_functor_join produces an equivalence from Join@{k k l} to Join@{u u l}. So this only matches the goal of an equivalence from Join@{k k k} to Join@{u u u} when both k and u equal l (and therefore equal each other).

I tried a few tweaks to make equiv_functor_join and isequiv_functor_join more flexible, but they didn't work. It should be possible to decouple the third universe in Join@{u1 u2 u3} from the universe level of the equivalence.

Signed-off-by: Ali Caglayan <[email protected]>

Alizter · 2024-09-28T12:32:44Z

I tried a few tweaks to make equiv_functor_join and isequiv_functor_join more flexible, but they didn't work. It should be possible to decouple the third universe in Join@{u1 u2 u3} from the universe level of the equivalence.

I managed to get it to work by making the universes in the functoriality of join more flexible.

jdchristensen · 2024-09-28T13:01:52Z

I managed to get it to work by making the universes in the functoriality of join more flexible.

Great! BTW, this kind of problem should go away with algebraic universes, since that third universe variable wouldn't even be there in that case.

Signed-off-by: Ali Caglayan <[email protected]>

Alizter · 2024-09-28T19:07:19Z

I've pushed my partial adaptation of the join construction to the new smallness stuff. Unfortunately I couldn't finish the proof about smallness of colimits since I found the number of universe variables involved far too overwhelming to keep track of. It's likely I've introduced some mistakes in this push, so we will need to be careful of the universe levels and check they make sense.

jdchristensen · 2024-09-28T19:56:29Z

I've pushed my partial adaptation of the join construction to the new smallness stuff. Unfortunately I couldn't finish the proof about smallness of colimits since I found the number of universe variables involved far too overwhelming to keep track of. It's likely I've introduced some mistakes in this push, so we will need to be careful of the universe levels and check they make sense.

It's too bad that the changes to equiv_functor_join required so many universe annotations. Do you think it's worth waiting for algebraic universes, which I expect will simplify a lot of things here?

Alizter · 2024-09-28T20:34:11Z

@jdchristensen It's possible it can already be simplified, but I spent a lot of time fighting Coq this time around to get it to work. I can see about removing some annotations when I get some more time.

I'm not sure if algebraic universes will come around soon, but if development there speeds up I wouldn't mind waiting.

join construction

9caf5b0

Signed-off-by: Ali Caglayan <[email protected]>

Alizter requested a review from jdchristensen February 19, 2024 00:15

jdchristensen reviewed Feb 19, 2024

View reviewed changes

theories/Homotopy/JoinConstruction.v Show resolved Hide resolved

jdchristensen reviewed Feb 19, 2024

View reviewed changes

Merge remote-tracking branch 'origin/master' into ps/branch/join_cons…

18b2df0

…truction

more flexible universes for functoriality of join

1a3413d

Signed-off-by: Ali Caglayan <[email protected]>

wip adapting join construction to new smallness

a2ba147

Signed-off-by: Ali Caglayan <[email protected]>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

join construction #1860

join construction #1860

Alizter commented Feb 19, 2024 •

edited

Loading

jdchristensen Feb 19, 2024

jdchristensen Feb 19, 2024 •

edited

Loading

Alizter Feb 19, 2024

jdchristensen Sep 28, 2024

jdchristensen Feb 19, 2024

jdchristensen Feb 19, 2024

Alizter Feb 19, 2024

jdchristensen Feb 19, 2024

jdchristensen Feb 19, 2024

Alizter Feb 19, 2024

jdchristensen Feb 19, 2024 •

edited

Loading

jdchristensen Feb 19, 2024

jdchristensen Feb 19, 2024

Alizter Feb 19, 2024

jdchristensen commented Feb 19, 2024

jdchristensen Feb 19, 2024

Alizter commented Feb 19, 2024 •

edited

Loading

Alizter commented Feb 19, 2024

jdchristensen commented Sep 26, 2024

Alizter commented Sep 27, 2024

jdchristensen commented Sep 27, 2024

Alizter commented Sep 28, 2024

jdchristensen commented Sep 28, 2024

Alizter commented Sep 28, 2024

jdchristensen commented Sep 28, 2024

Alizter commented Sep 28, 2024 •

edited

Loading

	- exact (pullback_pr2@{_ _ _ k}(f := f) (g := g)).
	- exact (pullback_pr2@{_ _ _ k} (f := f) (g := g)).

		Definition himage@{i j} {A : Type@{i}} {B : Type@{j}} (f : A -> B) : Type@{j}
		:= {y : B & merely@{j j} (hfiber f y)}.

join construction #1860

Are you sure you want to change the base?

join construction #1860

Conversation

Alizter commented Feb 19, 2024 • edited Loading

Choose a reason for hiding this comment

jdchristensen Feb 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jdchristensen Feb 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jdchristensen commented Feb 19, 2024

Choose a reason for hiding this comment

Alizter commented Feb 19, 2024 • edited Loading

Alizter commented Feb 19, 2024

jdchristensen commented Sep 26, 2024

Alizter commented Sep 27, 2024

jdchristensen commented Sep 27, 2024

Alizter commented Sep 28, 2024

jdchristensen commented Sep 28, 2024

Alizter commented Sep 28, 2024

jdchristensen commented Sep 28, 2024

Alizter commented Sep 28, 2024 • edited Loading

Alizter commented Feb 19, 2024 •

edited

Loading

jdchristensen Feb 19, 2024 •

edited

Loading

jdchristensen Feb 19, 2024 •

edited

Loading

Alizter commented Feb 19, 2024 •

edited

Loading

Alizter commented Sep 28, 2024 •

edited

Loading