Colimit library #850

SimonBoulier · 2017-01-23T09:43:43Z

Hi everyone,
This PR add the colimit library as described in #845.
Please feel free to comment.
Here are some debatable points on which I could work if you think they prevent merging:

The tactic funext (I find it very convenient, but could be removed if you don't like it.)
The notation ≃ which is utf8
The lack of comments

The file CommutativeSquares.v and a part of the file Diagram.v are from the [hott-limits library](https://github.com/peterlefanulumsdaine/hott-limits/) by Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine.

mikeshulman · 2017-01-23T11:54:41Z

Looks like travis timed out?

I wouldn't block on funext or the lack of comments, but I still think we should keep the library ASCII as much as possible. Would you mind doing a search-and-replace?

mikeshulman · 2017-01-23T11:54:52Z

Oh, and thanks!!

mikeshulman · 2017-01-25T10:17:12Z

Thanks, LGTM once Travis can be fixed. I'm not sure what the problem is; could it be just that the library is now honestly taking too long to compile? Could you attach a timing report?

SimonBoulier · 2017-01-25T12:44:27Z

Here it is: time-of-build-both.log
But it does not explain the 20 min overhead at all ...

JasonGross · 2017-02-04T23:22:48Z

theories/HIT/Colimits/Coequalizer.v

+Require Import Colimits.Diagram Colimits.Colimit.
+Generalizable All Variables.
+
+Context `{Funext}.


You should wrap this development in a section. What you are doing here is declaring a Funext axiom, which is not what we want.

JasonGross · 2017-02-04T23:23:30Z

theories/HIT/Colimits/Colimit.v

+Local Open Scope path_scope.
+Generalizable All Variables.
+
+Context `{Funext}.


This should be inside a section, preferably after the record definition and the Arguments commands, which should stay at top-level

JasonGross · 2017-02-04T23:26:54Z

theories/HIT/Colimits/Colimit.v

+  Definition path_cocone {C1 C2: cocone D X}  
+             (eq1 : forall i,  C1 i == C2 i)
+             (eq2 : forall i j g x, qq C1 i j g x @ eq1 i x = eq1 j (D _f g x) @ qq C2 i j g x)
+    : C1 = C2.


Style nit: I think we generally add Proof. after Definition and Lemma

JasonGross · 2017-02-04T23:27:03Z

theories/HIT/Colimits/Colimit.v

+  Defined.
+
+  Definition postcompose_cocone (C: cocone D X) {Y: Type}
+    : (X -> Y) -> cocone D Y.


Also Proof. here

JasonGross · 2017-02-04T23:28:22Z

theories/HIT/Colimits/Colimit.v

+    := Build_cocone colim pp.
+
+  Lemma is_universal_colimit {G: graph} (D: diagram G)
+    : is_universal (cocone_colimit D).


Add Proof. after Lemma

JasonGross · 2017-02-04T23:39:42Z

theories/HIT/Colimits/Pushout.v

+  (* We show here that the pushout defined as a colimit *)
+  (* is equivalent to the pushout defined as a primitive HIT. *)
+Section is_PO_pushout.
+  Require Import Types.Sum HIT.Pushout.


Require inside Section is unsupported, I think

JasonGross · 2017-02-04T23:41:25Z

theories/Types/Paths.v

 Defined.
-
+           


Nit: any reason for this whitespace change?

JasonGross · 2017-02-04T23:41:36Z

theories/Types/Paths.v

 Defined.

 Definition equiv_moveL_transport_V {A : Type} (P : A -> Type) {x y : A}
  (p : x = y) (u : P x) (v : P y)
 : transport P p u = v <~> u = transport P p^ v
 := BuildEquiv _ _ (moveL_transport_V P p u v) _.

+


Nit: why the extra newline?

JasonGross · 2017-02-04T23:41:44Z

theories/Types/Paths.v

 Defined.

 Definition equiv_moveL_transport_p {A : Type} (P : A -> Type) {x y : A}
  (p : y = x) (u : P x) (v : P y)
 : transport P p^ u = v <~> u = transport P p v
 := BuildEquiv _ _ (moveL_transport_p P p u v) _.

+


Nit: Why the extra newline?

JasonGross · 2017-02-04T23:42:13Z

theories/Types/Sigma.v

+Proof.
+  destruct p, q; reflexivity.
+Defined.
+(* Remark: this is also equals to: *)


Nit: "equal to" not "equals to"

JasonGross · 2017-02-04T23:50:36Z

Regarding travis: the log suggests that the issue is proviola. Comparing the occurrences of "Travis keep-alive spew" to a normal build suggests that it's fine all the way up through running XSLTPROC proviola-xml/HoTT.HIT.Suspension.xml, and then something whacky happens where it doesn't finish when trying to run that command....

andrejbauer · 2017-02-12T00:09:25Z

theories/Basics/Overture.v

@@ -775,6 +775,22 @@ Ltac by_extensionality x :=
    simpl; auto with path_hints
  end.

+


These tactics should be commented so that people can use them even if they don't know how to write tactics themselves.

andrejbauer · 2017-02-12T00:11:03Z

theories/HIT/Colimits/Coequalizer.v

+
+  (* ***************** *)
+  (* ***** Coeq ****** *)
+  (* ***************** *)


What is the purpose of these comments? If you are trying to visually serparate parts of the development, please use the coqdoc sectioning mechanism so that the generated documentation will look reasonable.

andrejbauer · 2017-02-12T00:15:00Z

theories/HIT/Colimits/Colimit.v

+Coercion q : cocone >-> Funclass.
+
+
+(** *** Definition of colimits *** *)


Please use coqdoc sectioning instead. The documentation says: "Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the line) followed by a space. One star is a section, two stars a sub-section, etc. The section title is given on the remaining of the line." So this should be something like:

(** ** Definitions of colimits *)

andrejbauer · 2017-02-12T00:15:40Z

theories/HIT/Colimits/Colimit.v

+
+
+(** *** Existence of colimits *** *)
+(** The existence is given by an HIT. *)


See above, please use coqdoc sectioning.

andrejbauer · 2017-02-12T00:16:04Z

theories/HIT/Colimits/Colimit.v

+
+  Arguments colim {G D} i x.
+
+  Axiom pp : forall {G: graph} {D: diagram G} (i j: G) (f : G i j) (x: D i),


Is pp really the best possible name here?

andrejbauer · 2017-02-12T00:17:01Z

theories/HIT/Colimits/Colimit.v

+    intros i j h x; simpl; hott_simpl. apply ap_compose.
+  Defined.
+
+  (* precompose *)


I would like to request lots of good comments, but I'll already be happy with some good comments that help the reader understand what is what. This particular one is not of that kind :-)

andrejbauer · 2017-02-12T00:18:06Z

theories/HIT/Colimits/Colimit.v

+    f_ap. exact (eisretr (postcompose_cocone HQ1) _)^.
+  Defined.
+
+  (** Here we prove than two equivalent diagrams have equivalent colimits. *)


All we ever do in Coq files is proving, no need to emphasize that. So I would say simply "Two equivalent diagrams have equivalent colimits."

andrejbauer · 2017-02-12T00:20:42Z

Many thanks for your contribution. I would suggest (see also my comments in the code):

Use coqdoc sectioning to delimit parts of development, rather than ad-hoc visually pleasing comments.
Always start proofs with Proof.
Please, please, put in some comments that will help people understand what is in the files. Each section or file should have a short overview of its contents, and non-obvious parts of the code should have comments. If the structure of a proof is not obvious, point that out in a comment and explain what it is.
Whatever @JasonGross says.

spitters · 2017-02-12T21:18:37Z

I did not have the time to look at this very carefully.
However, generally, this looks very nice.
Thanks @SimonBoulier !

spitters · 2017-02-13T15:15:06Z

theories/HIT/Colimits/Colimit_Prod.v

+    : sigma_diag (fun _ : A => D) ~d~ prod_diag.
+  Proof.
+    unshelve econstructor.
+    - serapply Build_diagram_map; cbn.


is `serapply supported already. I do not find it here:
https://coq.inria.fr/refman/tactic-index.html

It was added in the HoTT library: PR #829.
I don't think than it is planed that Coq have such a tactic. Do you have heard something about that?

spitters · 2017-02-13T15:18:56Z

I had a quick look. It looks like you've made the requested changes. Thanks!

SimonBoulier · 2017-02-13T15:20:28Z

Yes! I only hope there is not too many spelling errors in the comments ...

spitters · 2017-02-13T15:21:17Z

Thanks. Fine with me.

…

On Mon, Feb 13, 2017 at 4:19 PM, SimonBoulier ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In theories/HIT/Colimits/Colimit_Prod.v <#850>: > simple refine (Build_diagram _ _ _). exact (fun i => A * (D i)). simpl; intros i j f x. exact (fst x, D _f f (snd x)). Defined. - Definition diagram_map_prod_sigma - : diagram_map (sigma_diag (fun _ : A => D)) prod_diag. - simple refine (Build_diagram_map _ _). - exact (fun i x => (x.1, x.2)). - reflexivity. + Definition diagram_equiv_prod_sigma + : sigma_diag (fun _ : A => D) ~d~ prod_diag. + Proof. + unshelve econstructor. + - serapply Build_diagram_map; cbn. It was added in the HoTT library: PR #829 <#829>. I don't think than it is planed that Coq have such a tactic. Do you have heard something about that? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#850>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAM2zlThbexdV2YShFvvNel4n-SGFLf1ks5rcHSAgaJpZM4Lq1UK> .

SimonBoulier · 2017-02-14T10:07:58Z

Regarding the time out bug. I can reproduce it on my computer: make -j4 proviola never ends and stay stuck on XSLTPROC proviola-xml/HoTT.HIT.Suspension.xml
And indeed, there is a problem with this file: the nested comment just before loop_susp_unit is badly handled and make the whole file corrupted. I propose #852.

SimonBoulier · 2017-02-16T12:57:39Z

The problem for proviola was with make proviola-html/HoTT.HIT.Colimits.Flattening.html which never ends.
I don't understand why but changing the Lets in Definitions at the end of Flattening.v solve the problem (maybe the goals are too long?).
However there are still some errors with the end of this file: the goals generated by proviola are not exactly the same as those I see on Coq.

Anyway, it' ok for me for merging.

andrejbauer · 2017-02-18T09:46:59Z

If I understand correctly, Travis is now happy? Excellent. Many thanks for the PR. That's one pair of eyes from me.

spitters · 2017-02-18T11:10:16Z

I'll let @JasonGross pull this, as I am not sure of the proviola part. It looks good from my perspective.

JasonGross

I'll let Travis be the arbiter of proviola. LGTM modulo adding Proof and either picking more descriptive names where I mentioned, or making those things Local Definition. Thanks!

JasonGross · 2017-02-18T16:04:30Z

theories/HIT/Colimits/Flattening.v

+
+  (** We define here the graph ∫D, also denoted G·D *)
+
+  Definition integral : graph.


Add Proof. after Definition

JasonGross · 2017-02-18T16:04:42Z

theories/HIT/Colimits/Flattening.v

+
+  (** Given a dependent diagram, we can recover a diagram over G by considering the Σ types. *)
+
+  Definition sigma_diagram : diagram G.


Add Proof. after Definition

JasonGross · 2017-02-18T16:04:51Z

theories/HIT/Colimits/Flattening.v

+
+  (** Now, given an equifibered diagram and using univalence, one can define a type family [E' : colimit D -> Type] by recusrion on the colimit. *)
+
+  Definition E' : colimit D -> Type.


Add Proof. after Definition

With such a short name as E', you should make this Local Definition so that the unqualified name never gets exported. (You may also want Local Definition for the other things that were Let s; that's up to you.)

JasonGross · 2017-02-18T16:07:40Z

theories/HIT/Colimits/Flattening.v

+  Context (A0 : A -> Type) (B0 : B -> Type) (C0 : C -> Type)
+          (f0 : forall x, A0 x <~> B0 (f x)) (g0 : forall x, A0 x <~> C0 (g x)).
+
+  Definition P : PO f g -> Type.


Add Proof. after Definition

Also, Local Definition here, or pick a more descriptive name.

JasonGross · 2017-02-18T16:08:47Z

theories/HIT/Colimits/Flattening.v

+    etransitivity. symmetry. apply f0. apply g0.
+  Defined.
+
+  Definition E : dep_diagram (span f g).


Add Proof. after Definition, and make this Local Definition or pick a more descriptive name.

JasonGross · 2017-02-18T16:09:25Z

theories/HIT/Colimits/Flattening.v

+      exact (fun y => p # (g0 x y)).
+  Defined.
+
+  Definition HE : equifibered _ E.


Add Proof. after Definition, and make this Local Definition , or pick a more descriptive name.

SimonBoulier · 2017-02-20T09:45:07Z

Thanks for your attention @JasonGross, I missed this file (for the Proof.). And I didn't know about Local Definition, it' nice.

SimonBoulier · 2017-03-06T15:04:31Z

Anything blocking?

SimonBoulier added 4 commits January 23, 2017 10:09

Adding several coherence lemmas for the colimit library

da10116

Adding a funext tactic

a27a200

The colimit library.

b584ffe

The file CommutativeSquares.v and a part of the file Diagram.v are from the [hott-limits library](https://github.com/peterlefanulumsdaine/hott-limits/) by Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine.

Reference to the blog post on colimits.

ab782ff

Changing the notation ≃ to ~d~ for the equivalence of diagram

9040525

JasonGross requested changes Feb 4, 2017

View reviewed changes

andrejbauer reviewed Feb 12, 2017

View reviewed changes

andrejbauer mentioned this pull request Feb 12, 2017

Integrating hott-colimits library #845

Closed

SimonBoulier added 8 commits February 13, 2017 09:40

Notations are now reserved in theories/Basics/Notations.v

337f088

Instances are now global

e7a6bef

Declaration of Funext in contexts are now in sections

419878d

Proofs now start by ... Proof.

70d308e

Don't Require inside a section

2fc9c34

Spacing and grammar

f826478

Rename pp to colimp

4068742

Documentation for the Colimit library, and minor changes

c13bda7

spitters reviewed Feb 13, 2017

View reviewed changes

Spelling

17d6222

SimonBoulier added 2 commits February 15, 2017 09:34

Merge remote-tracking branch 'upstream/master' into colimit-library

c1e25da

Changing Let to Definition to make proviola happy

cc9b49d

JasonGross requested changes Feb 18, 2017

View reviewed changes

SimonBoulier added 2 commits February 20, 2017 10:11

Proofs now start by ... Proof.

501e527

Naming in Flattening.v

5286d21

andrejbauer mentioned this pull request Feb 20, 2017

Colimits in HoTT nmvdw/Three-HITs#1

Closed

JasonGross merged commit 6712d5e into HoTT:master Mar 8, 2017

		@@ -775,6 +775,22 @@ Ltac by_extensionality x :=
		simpl; auto with path_hints
		end.

		Coercion q : cocone >-> Funclass.


		( * Definition of colimits *** *)



		( * Existence of colimits *** *)
		(** The existence is given by an HIT. *)


		Arguments colim {G D} i x.

		Axiom pp : forall {G: graph} {D: diagram G} (i j: G) (f : G i j) (x: D i),


		(** We define here the graph ∫D, also denoted G·D *)

		Definition integral : graph.


		(** Given a dependent diagram, we can recover a diagram over G by considering the Σ types. *)

		Definition sigma_diagram : diagram G.


		(** Now, given an equifibered diagram and using univalence, one can define a type family [E' : colimit D -> Type] by recusrion on the colimit. *)

		Definition E' : colimit D -> Type.

Colimit library #850

Colimit library #850

Conversation

SimonBoulier commented Jan 23, 2017

mikeshulman commented Jan 23, 2017

mikeshulman commented Jan 23, 2017

mikeshulman commented Jan 25, 2017

SimonBoulier commented Jan 25, 2017

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

JasonGross commented Feb 4, 2017

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

andrejbauer commented Feb 12, 2017

spitters commented Feb 12, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

spitters commented Feb 13, 2017

SimonBoulier commented Feb 13, 2017

spitters commented Feb 13, 2017 via email

SimonBoulier commented Feb 14, 2017

SimonBoulier commented Feb 16, 2017

andrejbauer commented Feb 18, 2017

spitters commented Feb 18, 2017

JasonGross left a 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

Choose a reason for hiding this comment

SimonBoulier commented Feb 20, 2017

SimonBoulier commented Mar 6, 2017