Zigzag Construction#34
Conversation
Co-authored-by: Dan Christensen <jdc+github@uwo.ca>
Colimit: generalize functor_Colimit_homotopy
| Require Import Diagram. | ||
| Require Import Types. | ||
|
|
||
| (** * Suppose we have sequences [A_i] and [B_i]. An interleaving from [A_i] to [B_i] consists of two natural transformations [d : A_i => B_i] ([d] for down) and [u : B_i => A_i+1] ([u] for up), such that the following diagram is commutative: |
There was a problem hiding this comment.
Comments of the form (** *... are meant for short headings. The provide a table of contents in the generated documentation, so they need to be brief, and not end in periods. You should create a top-level heading here, but maybe the rest should just be converted to regular comments.
| @@ -0,0 +1,296 @@ | |||
| Require Import Basics. | |||
| Require Import Colimits.Pushout. | |||
| Require Import Basics.Tactics. | |||
There was a problem hiding this comment.
Basics.Tactics is redundant.
The rest should be reordered: Basics, Types, Diagrams., Colimits.
| apply ap. | ||
| exact (L n x)^. |
There was a problem hiding this comment.
My next commit will change this, saving one line in the later proof.
| (** Construct a better section for the equivalence which is needed in the proof of the induction principle. *) | ||
| Local Definition better_section : zigzag_glue_map_inf o zigzag_glue_map_inv_inf == idmap. |
There was a problem hiding this comment.
This definition isn't constructing a section, it is proving that a certain map is a section. So the comment and the name need updating.
| snrapply Colimit_ind. | ||
| - intros n x. | ||
| simpl. | ||
| rhs nrapply (@colimp _ B n (S n) idpath x)^. |
There was a problem hiding this comment.
rhs already needs to invert the given path, so since you provided an inverted path, it is double-inverted. Instead, use rhs_V, which doesn't invert its path. (In general, lhs and rhs_V are the good ones, and lhs_V and rhs need to invert the path.) Using the _V versions when appropriate often also saves underscores and parentheses. BTW, this fix should simplify the proof below.
| apply ap. | ||
| exact (L n x)^. |
There was a problem hiding this comment.
You should check whether putting the inverse on the outside of the ap saves a step below.
jdchristensen
left a comment
jdchristensen
left a comment
There was a problem hiding this comment.
Feel free to notice the types of fixes I'm making and insert your own clean up commits to save me some work...
| Require Import Types. | ||
|
|
||
| (** * Suppose we have sequences [A_i] and [B_i]. An interleaving from [A_i] to [B_i] consists of two natural transformations [d : A_i => B_i] ([d] for down) and [u : B_i => A_i+1] ([u] for up), such that the following diagram is commutative: | ||
| (** * Suppose we have sequences [A_i] and [B_i]. An interleaving from [A_i] to [B_i] consists of two natural transformations [f : A_i => B_i] and [g : B_i => A_i+1] such that the following diagram is commutative: |
There was a problem hiding this comment.
u and d didn't match the actual names you used below.
| snrapply Build_DiagramMap. | ||
| - exact f. | ||
| - intros n m [] x. | ||
| - intros n _ [] x. |
There was a problem hiding this comment.
m ends up "free", so better to not introduce it at all. (If you cbn the edge before destructing it, it goes away, but this is a cheap way to achieve it.)
|
|
||
| Context (n : nat). | ||
|
|
||
| Definition zigzag_comp_eisretr (a : A n) : (eisretr equiv_zigzag_glue (@colim _ A n a)) = (ap (@colim _ A n.+1%nat) (U n a)^) @ (@colimp _ A n _ _ a). |
There was a problem hiding this comment.
Please remove unneeded parentheses throughout. E.g. (lhs) = (rhs) doesn't need parens, and (path1) @ (path2) doesn't either. Both = and @ have low precedence. Same with <~>.
2 participants
This PR adds the rest of the stuff completed (or nearly completed) for the zigzag construction: the zigzag construction itself, the supporting machinery in
Interleaving, the almost-finished induction principle, and the concluding application of Kraus-von Raumer.As noted in my other PR, the results in
Sequential.vshould eventually be superseded by a full rewrite of that file when colimits are redone, i.e. don't look too closely at it.