Add: transport lemmas for morphisms in categories #2298
Conversation
Extract transport lemmas from stable categories formalization (PR HoTT#2288). Changes from original formalization: - Rename file from ZeroMorphismLemmas.v to TransportMorphisms.v to better reflect content - Remove ~150 lines of unused/redundant lemmas, keeping only the 4 transport lemmas actually used - Remove zero-specific sections that weren't actually zero-specific - Place in Categories/Additive/ folder alongside ZeroObjects.v The retained lemmas are: - transport_compose_morphism - transport_compose_both_inverse - transport_inverse_eq - morphism_eq_transport_inverse These lemmas handle how morphisms behave under transport along equality proofs and are essential for proving preservation properties of functors in AdditiveCategories.v and beyond. I verified these are the only lemmas from the original file actually used in the formalization. The file has been tested to compile successfully using: ``` make -f Makefile.coq theories/Categories/Additive/TransportMorphisms.vo ``` Follows lessons learned and style conventions established in PR HoTT#2293 review. @jdchristensen Please let me know if you see any issues or have suggestions for improvement. Sincere apologies if I've overlooked anything from your previous feedback.
| These lemmas are primarily used in AdditiveCategories.v to prove that | ||
| additive functors preserve zero morphisms. |
There was a problem hiding this comment.
I think you should remove these lines. Predictions of future use are likely to become stale.
| From HoTT Require Import Basics Types. | ||
| From HoTT.Categories Require Import Category. |
There was a problem hiding this comment.
You can greatly reduce the dependencies. For the second line, you just need Category.Core, I think. And for the first line, note that Category.Core only needs Basics.Overture and Basics.Notations, so you might get by with something similar (plus Basics.PathGroupoids).
(Reducing dependencies makes it possible to build more files in parallel.)
| Lemma transport_compose_morphism {X Y Z W : object C} (p : X = W) | ||
| (f : morphism C X Y) (g : morphism C Y Z) | ||
| : transport (fun U => morphism C U Z) p (g o f)%morphism = | ||
| (g o transport (fun U => morphism C U Y) p f)%morphism. | ||
| Proof. | ||
| destruct p; reflexivity. | ||
| Qed. |
There was a problem hiding this comment.
This is a special case of ap_transport, but I think it is ok to leave it, since when using ap_transport, Coq can't figure out the function to use.
(For the record, this works:
exact (ap_transport p (fun w k => (g o k)%morphism) f)^.
and p and f can be inferred.)
| (** Convert equations with transport to equations with inverse transport. *) | ||
| Lemma transport_inverse_eq {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. | ||
| Proof. | ||
| intro H. | ||
| rewrite <- H. | ||
| destruct p; reflexivity. | ||
| Qed. |
There was a problem hiding this comment.
This is moveL_transport_V, so should be removed.
| (** Specialized version for morphisms. *) | ||
| Lemma morphism_eq_transport_inverse {W X Y : object C} (p : W = X) | ||
| (f : morphism C W Y) (g : morphism C X Y) | ||
| : transport (fun Z => morphism C Z Y) p f = g -> | ||
| f = transport (fun Z => morphism C Z Y) p^ g. | ||
| Proof. | ||
| intro H. | ||
| rewrite <- H. | ||
| destruct p; reflexivity. | ||
| Qed. |
There was a problem hiding this comment.
Instead of reproving it, we can reuse the general case. And since it's a one-liner, maybe this result isn't worth recording?
| (** Specialized version for morphisms. *) | |
| Lemma morphism_eq_transport_inverse {W X Y : object C} (p : W = X) | |
| (f : morphism C W Y) (g : morphism C X Y) | |
| : transport (fun Z => morphism C Z Y) p f = g -> | |
| f = transport (fun Z => morphism C Z Y) p^ g. | |
| Proof. | |
| intro H. | |
| rewrite <- H. | |
| destruct p; reflexivity. | |
| Qed. | |
| Definition morphism_eq_transport_inverse {W X Y : object C} (p : W = X) | |
| (f : morphism C W Y) (g : morphism C X Y) | |
| : transport (fun Z => morphism C Z Y) p f = g -> | |
| f = transport (fun Z => morphism C Z Y) p^ g | |
| := moveL_transport_V _ p _ _. |
There was a problem hiding this comment.
BTW, one of the reasons we tend to use Definition instead of Lemma, Theorem, etc, is that it is then easy to switch to := notation, which only works for definitions.
| @@ -0,0 +1,56 @@ | |||
| (** * Transport lemmas for morphisms in categories | |||
There was a problem hiding this comment.
These results don't belong in the Additive folder, since they are general results about transporting morphisms. And since only two results are left, each having a one line proof, I think you should just add those two to the end of Category/Core.v.
|
Closing to move these to Core.v per review by @jdchristensen |
Move transport lemmas from separate file to Core.v per PR HoTT#2298 review - @jdchristensen Changes: - Add transport_compose_morphism and transport_compose_both_inverse to Category/Core.v - Remove TransportMorphisms.v from Additive folder - Use Definition with pattern matching instead of Lemma with destruct - Drop redundant lemmas (moveL_transport_V already exists) Extracted from stable categories formalization (PR HoTT#2288). Tested with: make -f Makefile.coq
2 participants
Extract transport lemmas from stable categories formalization (PR #2288).
Changes from original formalization:
The retained lemmas are:
These lemmas handle how morphisms behave under transport along equality proofs and are essential for proving preservation properties of functors in AdditiveCategories.v and beyond. I verified these are the only lemmas from the original file actually used in the formalization.
The file has been tested to compile successfully using:
Follows lessons learned and style conventions established in PR #2293 review.
@jdchristensen Please let me know if you see any issues or have suggestions for improvement.
Sincere apologies if I've overlooked anything from your previous feedback.