Theorem 5.8.2 from the book: characterizations of identity types

[ThomatoTomato]

In this PR we prove that based identity types are characterized by the J-rule or contractible total spaces. This is the contents of lemma 5.8.2.

Many of the results already exists within the library, and the equivalences i) <=> iii) <=> iv) seems useful to have in its own right. The additions that this PR makes is the following implications: i) => ii), i) => iii), ii) => iii), and iii) => iv).

I'm struggling a little to know how to organize the files. The implications that goes through ii) should depend on Pointed.Basics, but nothing else in PathAny requires Pointed. I think it is best to put this somewhere else. It also seems that i) => ii) requires funext.

I'm also not very happy with all my proofs, so I would gladly take some advice on how to improve them. It should be obvious from the comments were I would like to see some improvements, if there are any good improvements to make.

[jdchristensen]

It might be a day or two before I can look at this closely.

I'd be very surprised if you can prove (ii) without funext. To show a function type is contractible, you have to prove that two functions are equal, which will require funext. (It's even needed to show Contr (Empty -> X), for example.) So I think it's perfectly fine that you are using funext here.

Will using Pointed simplify things significantly, or just slightly? (And presumably you meant Pointed.Core?) I agree that requiring Pointed.Core would bring in way too many dependencies for this file. So if it wouldn't simplify things too much, then maybe it's ok as is?

About the overall structure: the proof of (ii) => (iii) seems the hardest. Is it easier to replace it with (ii) => something else, since we know the others are equivalent? (And is it worth dropping any redundant implications? I think it's ok keeping redundant ones if the proofs are short.)

Let's use (ii) rather than ii) consistently.

For the proof that's embedded in HoTTBook.v, maybe it should be put in PathAny.v, since someone will likely look there for the various implications.

[ThomatoTomato]

Will using Pointed simplify things significantly, or just slightly? (And presumably you meant Pointed.Core?) I agree that requiring Pointed.Core would bring in way too many dependencies for this file. So if it wouldn't simplify things too much, then maybe it's ok as is?

It looks like I hallucinated. I believed that pfammap could be retreived as a special case of pForall, but now I don't see how. Defining pfammap could be fine, but if someone wants to use it later, it might be best to move this to pointed, for consistency. That is how we get dependencies. I don't think anything from Pointed can help us.

About the overall structure: the proof of (ii) => (iii) seems the hardest. Is it easier to replace it with (ii) => something else, since we know the others are equivalent? (And is it worth dropping any redundant implications? I think it's ok keeping redundant ones if the proofs are short.)

I tried to prove (ii) => (iv), but I wasn't able to do it. Those two statements seem very close to each other, so I felt like there would be an obvious translation... However, the technique used in (ii) => (iii) should be adaptable to (ii) => (i).

Regarding the implication logic. Since I don't want the whole result to depend on funext, I only want to first prove (i) <=> (iii) <=> (iv). Afterwards we may assume funext to then say that (ii) is logically equivalent. We already have (i) <=> (iii) <=> (iv), and the proofs are pretty short. We will only save 1 implication if we have a smart route through, so I don't think it matters too much 🤷‍♀️

[jdchristensen]

I wonder if it would be helpful to state a funext-free version of (ii), namely that any two maps in the type under consideration are homotopic (in a sense that respects the pointedness). If we call this (ii'), then we could have cyclic implications involving (i), (ii'), (iii) and (iv), and then separately have (ii) <=> (ii'), using funext. (But, as I said, I don't care too much about minimizing the number of implications when there are short proofs. The motivation here is more that it might clean up (i) => (ii) and (ii) => (iii) to factor them through (ii').)

[Alizter]

I would lean on the side of not introducing Pointed here, keeping the base-points explicit for simplicity of reading, and also to avoid the technical debt that relying on Pointed will introduce.

Regarding funext, here is how to drop it:

Definition pathpfammap {A : Type} {a0 : A} {R S : A -> Type} {r0 : R a0} {s0 : S a0} 
  (f g : pfammap R S r0 s0) : Type
  := { p : forall a : A, f.1 a == g.1 a & p a0 r0 = f.2 @ g.2^}.

Definition homocontr_pfammap_identitysystem `{Funext} {A : Type} {a0 : A} 
  (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem R r0} (S : A -> Type) (s0 : S a0) 
  : exists f : pfammap R S r0 s0, forall g, pathpfammap f g.
Proof.
  pose (f := IdentitySystem_ind (fun a _ => S a) s0).
  pose proof (f0 := IdentitySystem_ind_beta (fun a _ => S a) s0).
  snrefine ((f; f0); _).
  intro g; cbn.
  exists (IdentitySystem_ind (fun a r => f a r = g.1 a r) (f0 @ g.2^)).
  snrapply IdentitySystem_ind_beta.
Defined .

We do a similar trick in many other places. Contractibility as asked for in the HoTT book, becomes a corollary of pathpfammap (name isn't great btw). Basically under funext, pathpfammap is equivalent to the path type.

[Alizter]

By the way, the proof of equiv_path_contr_pfammap with the adapted hypothesis to match the new (ii) is a little harder to do. I still think it ought to be possible, but I am having a tricky time going through the algebra. I'll see if I can finish it off when I have some more time.

The reason I believe it can be eliminated is because you apD10 in that proof which heuristically should cancel the path_foralls from the old (ii).

[ThomatoTomato]

We do a similar trick in many other places. Contractibility as asked for in the HoTT book, becomes a corollary of pathpfammap (name isn't great btw). Basically under funext, pathpfammap is equivalent to the path type.

Great! Now, what do you usually name mapping spaces in the library? Taking inspiration from Pointed.Core, I think the best thing would be to call these spaces for pfamMap and path_pfamMap, or possibly pfam_map and path_pfam_map. However, we're not actually using the record type pFam, so maybe it should be uncurry_pfamMap and path_uncurry_pfamMap 🤷‍♀️

By the way, the proof of equiv_path_contr_pfammap with the adapted hypothesis to match the new (ii) is a little harder to do. I still think it ought to be possible, but I am having a tricky time going through the algebra. I'll see if I can finish it off when I have some more time.

Do you think it can be easier to do another direction? If (ii) => (i) is easier to do, then we can maybe change the original structure to get a simpler proof. Anyways, if we get (ii) => (i) then we have enough to state the theorem.

[Alizter]

By the way, the proof of equiv_path_contr_pfammap with the adapted hypothesis to match the new (ii) is a little harder to do. I still think it ought to be possible, but I am having a tricky time going through the algebra. I'll see if I can finish it off when I have some more time.

Do you think it can be easier to do another direction? If (ii) => (i) is easier to do, then we can maybe change the original structure to get a simpler proof. Anyways, if we get (ii) => (i) then we have enough to state the theorem.

I think this direction still works, but should introduce some more general lemmas. Part of the confusion is that a0 = is also an identity system, but at "two different levels".

Let's come back to this point in a bit. Firstly I want to show a more symmetrical lemma that will be useful:

Definition isequiv_identitysystem_ind {A : Type} {a0 : A} 
  (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem R r0}
  (S : A -> Type) (s0 : S a0) `{!IsIdentitySystem S s0}
  : forall (a : A), IsEquiv (IdentitySystem_ind (R:=R) (fun a' _ => S a') s0 a).
Proof.
  intros a.
  snrapply isequiv_adjointify.
  - exact (IdentitySystem_ind (R:=S) (fun a' _ => R a') r0 a).
  - revert a.
    rapply (IdentitySystem_ind (R:=S)).
    lhs nrapply ap.
    1: snrapply IdentitySystem_ind_beta. 
    nrapply IdentitySystem_ind_beta.
  - revert a.
    rapply (IdentitySystem_ind (R:=R)).
    lhs nrapply ap.
    1: snrapply IdentitySystem_ind_beta. 
    nrapply IdentitySystem_ind_beta.
Defined.

The proof is symmetric, but I didn't bother condensing it down further. It can probably be done in half the lines. This general lemma will specialise accordingly without having to treat paths as a special case every time.

Next we have this quite important instance:

Global Instance isidentitysystem_paths {A : Type} {a0 : A}
  : IsIdentitySystem (paths a0) idpath.
Proof.
  snrapply Build_IsIdentitySystem.
  - nrapply paths_ind.
  - reflexivity.
Defined.

This makes the proof of isequiv_transport_IsIdentitySystem much cleaner:

(** Given an identity system, transporting the point [r0] induces a fiber-wise equivalence between the based path type on [a0] and [R]. This is Theorem 5.8.2 (i) => (iii) from the Book. *)
Global Instance isequiv_transport_IsIdentitySystem {A : Type} {a0 : A} 
  (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem R r0} 
  (a : A) : IsEquiv (fun p : a0 = a => transport R p r0).
Proof.
  exact (isequiv_identitysystem_ind (paths a0) idpath R r0 a).
Defined.

What we are doing with pathpfammap is pretty much the usual wildcat game. I think it might be smart to introduce wildcats here and think about the wild category of pointed families which is the most natural home for these statements.

We have identity maps and composition:

Definition pfammap_compose {A : Type} {a0 : A} {R S T : A -> Type} {r0 : R a0} {s0 : S a0} {t0 : T a0}
  : pfammap S T s0 t0 -> pfammap R S r0 s0 -> pfammap R T r0 t0.
Proof.
  intros [f Hf] [g Hg].
  exists (fun a r => f a (g a r)).
  exact (ap (f _) Hg @ Hf).
Defined.

Definition pfammap_id {A : Type} {a0 : A} {R : A -> Type} {r0 : R a0}
  : pfammap R R r0 r0.
Proof.
  exists (fun a r => r).
  reflexivity.
Defined.

this lets us state the more general lemma:

Definition isidentitysystem_pathpfammap {A : Type} {a0 : A}
  (R : A -> Type) (r0 : R a0) (S : A -> Type) s0
  (f : pfammap R S r0 s0)
  (g : pfammap S R s0 r0)
  (f_g : pathpfammap (pfammap_compose f g) pfammap_id)
  (g_f : pathpfammap (pfammap_compose g f) pfammap_id)
  : IsIdentitySystem R r0 -> IsIdentitySystem S s0.
Proof.
  intros H.
  snrapply Build_IsIdentitySystem.
  - intros P P1.
    intros a r.
    pose ((f_g).1 a r) as p.
    cbn in p.
    refine (p # _).
    set (g.1 a r) as x.
    change (P a (f.1 a x)).
    clearbody x; clear r p; revert a x.
    rapply IdentitySystem_ind.
    refine (_^ # P1).
    exact f.2.
  - intros P P1; cbn.
Admitted.

which states that the property of being an identity system is invariant under equivalences in the wild category of pointed families. I didn't finish this quite, but I'm fairly certain it can be done. The final path induction is complicated and needs a clever set up since Coq is too dumb to generalise variables.

Anyway, with that you should have:

Global Instance equiv_path_contr_pfammap {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) 
  (H : forall S : A -> Type, forall s0 : S a0, exists f : pfammap R S r0 s0, forall g, pathpfammap f g)
  (a : A) : IsEquiv (fun p : a0 = a => transport R p r0).
Proof.
  snrapply isequiv_transport_IsIdentitySystem.
  pose (H (paths a0) idpath) as H'.
  srapply isidentitysystem_pathpfammap.
  - exists (fun a p => transport R p r0).
    reflexivity.
  - exact H'.1.

and I think this should be doable.

Wildcat stuff might help you organize things going on. You can just define pfam for now as a sigma type. We can think about sharing this with Pointed later. With regards to naming, just do stuff like path_pfam etc.

[jdchristensen]

@Alizter What you wrote sounds nice, but it seems to add a lot. The current form of the PR already has all implications that are needed, so I'm not sure it's worth getting too fancy, or introducing a dependency on wild categories. (OTOH, with wild categories, some of these results are special cases of general facts, e.g. that any two initial objects are equivalent.) My hope in introducing the non-funext version (ii') of (ii) was to end up with shorter proofs, which worked for (i) => (ii'). So all we need is a short proof of (ii') => something, plus (ii') <=> (ii), which should be easy. I think (ii') => (iii) should be straightforward.

[ThomatoTomato]

With the new definition, (ii') => (iii) became a lot simpler. I don't really know how to use tactics so well for this, so I would take any advice that cleans up the proof.

[Alizter]

Here is a way to do it with tactics.

Proof.
  snrapply isequiv_adjointify.
  - revert a.
    by rapply IdentitySystem_ind.
  - hnf; revert a.
    rapply IdentitySystem_ind.
    apply (ap (fun x => transport R x r0) (y:=1)).
    rapply IdentitySystem_ind_beta.
  - intros p.
    destruct p.
    rapply IdentitySystem_ind_beta.
Defined.

[Alizter]

@Alizter What you wrote sounds nice, but it seems to add a lot. The current form of the PR already has all implications that are needed, so I'm not sure it's worth getting too fancy, or introducing a dependency on wild categories. (OTOH, with wild categories, some of these results are special cases of general facts, e.g. that any two initial objects are equivalent.) My hope in introducing the non-funext version (ii') of (ii) was to end up with shorter proofs, which worked for (i) => (ii'). So all we need is a short proof of (ii') => something, plus (ii') <=> (ii), which should be easy. I think (ii') => (iii) should be straightforward.

Yes, it ends up being too fancy for its own good that way. @ThomatoTomato seems to have found the proof I was looking for before using this way.

All that is left is to clean up the names a bit. I will do another pass in the weekend with some better suggestions.

[jdchristensen]

When this is ready to merge (but not before then), let's squash many of these commits together. Probably everything until this point can be squashed into one, but if @Alizter makes additional commits, they can be kept separate to keep track of authorship. I can do this once it is ready to merge, if @ThomatoTomato doesn't know how.

[jdchristensen]

Style comments: The : that introduces the type of a definition is best on a new line, unless everything fits on one line.

(** This is a comment. *) style comments should end in a period. The only things that don't are section titles.

The file should end in a new line.

There's probably more, so please give it a careful read-through.

[ThomatoTomato]

(iv) => (i) is pretty short and sweet. I removed (i) => (iii) and factored that one through (ii'). I'm not sure if we should still keep (iv) => (iii) around. It is used a couple of other places in the library.

Dan has suggested that we move PathAny.v into the Homotopy subdirectory. I don't know what the file should be called. The contents all resolve around characterizing based path types.

[jdchristensen]

I was thinking we could rename PathAny.v to Homotopy/IdentitySystems.v. That location puts it right beside Homotopy/EncodeDecode.v, which has similar goals, but more dependencies. @Alizter , what do you think?

(I want to get rid of as many things in the top-level theories/ folder as possible.)

[jdchristensen]

(iv) => (i) is pretty short and sweet. I removed (i) => (iii) and factored that one through (ii'). I'm not sure if we should still keep (iv) => (iii) around. It is used a couple of other places in the library.

We should keep the statement of (iv) => (iii), since it is useful. The proof could either be kept as is or it could be a composite of the other implications. Since the proof is fairly short and conceptual, maybe just keeping it the current proof is best? If we do, then I think it will be useful to first have the various implications that together prove 5.8.2, possibly via a cyclic ordering, and then record some of the additional implications that are useful, noting that they also follow by composing earlier results. The other lemmas/tactics in the file could come at the end.

[Alizter]

I was thinking we could rename PathAny.v to Homotopy/IdentitySystems.v. That location puts it right beside Homotopy/EncodeDecode.v, which has similar goals, but more dependencies. @Alizter , what do you think?

That sounds sensible.

[ThomatoTomato]

I think everything should be in order now. I have renamed the functions, removed capitalizations, re-structured and moved the file, and updated every file that should depend on this accordingly. Since it builds, I think I was able to remove all mentions of PathAny.

I have no idea how to squash commits, so unless @jdchristensen wants me to learn how to do it, feel free to do it.

[jdchristensen]

@ThomatoTomato This is looking great! Just a few more comments:

• To really get Thm 5.8.2, we should prove that the weakened form of (ii) (which we called (ii') above) implies (ii) [under Funext], and the converse (which shouldn't need Funext). I think both will be easy.
• Does @Alizter remember the motivation for the name contr_sigma_refl_rel? It was in an earlier PR, but I'm not sure why refl is in the name, for example. Maybe we can come up with a better name?

For the future, we should see if any of the results in this file can be used elsewhere in the library to simplify any arguments.

I will squash some of these commits before merging, but I'll wait until the above two points are addressed.

[ThomatoTomato]

We now have the real Thm 5.8.2. I left the weaker version in contrib, as I think this is how we should be thinking of this theorem.

Regarding the name of contr_sigma_refl_rel, it sounds like the last part means reflexivity relation, which doesn't quite make sense. To keep the name in the same style as the functions defined above, maybe contr_sigma_path_pfamcould be a suitable name?

[Alizter]

I don't recall exactly, but I think it was meant to be "reflexive relation".

[jdchristensen]

Regarding the name of contr_sigma_refl_rel, it sounds like the last part means reflexivity relation, which doesn't quite make sense. To keep the name in the same style as the functions defined above, maybe contr_sigma_path_pfamcould be a suitable name?

I noticed that property (iii) is consistently referred to as "equiv_path" elsewhere in the file, so I switched to that. Now the four cyclic implications have consistent names.

I also isolated the proof of reflexivity of pfammap_homotopy, and tidied a couple more things. I'll partially squash and merge soon unless there are other comments.

[Alizter]

LGTM 👍