Skip to content

redefine Bifunctor #1952

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 10 commits into from
May 7, 2024
Merged

redefine Bifunctor #1952

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
b0266b6
redefine Bifunctor
Alizter May 5, 2024
10940ca
AbSES/Ext: adjust universe variables to make it build
jdchristensen May 5, 2024
fddabf6
review comments, more simplification, cleanup commented out proofs
Alizter May 6, 2024
988faaa
best-of-both-worlds bifunctor definition
Alizter May 6, 2024
dd7d652
cleanup dead code and revert changes in AbSES
Alizter May 6, 2024
bc36433
whitespace
Alizter May 6, 2024
a9a5761
Bifunctor.v: add comments and simplify some proofs
jdchristensen May 7, 2024
10bcb54
typo
Alizter May 7, 2024
01daaf6
abstract out fmap_pair in Prod.v
Alizter May 7, 2024
f235f53
adjust spacing
Alizter May 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions theories/Algebra/AbGroups/AbHom.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,13 +92,13 @@ Defined.
Global Instance is0bifunctor_ab_hom `{Funext}
: Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
Proof.
rapply Build_Is0Bifunctor.
rapply Build_Is0Bifunctor''.
Defined.

Global Instance is1bifunctor_ab_hom `{Funext}
: Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
Proof.
nrapply Build_Is1Bifunctor.
nrapply Build_Is1Bifunctor''.
1,2: exact _.
intros A A' f B B' g phi; cbn.
by apply equiv_path_grouphomomorphism.
Expand Down
8 changes: 4 additions & 4 deletions theories/Algebra/AbSES/BaerSum.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,13 +54,13 @@ Defined.
Global Instance is0bifunctor_abses' `{Univalence}
: Is0Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
Proof.
rapply Build_Is0Bifunctor.
rapply Build_Is0Bifunctor''.
Defined.

Global Instance is1bifunctor_abses' `{Univalence}
: Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
Proof.
snrapply Build_Is1Bifunctor.
snrapply Build_Is1Bifunctor''.
1,2: exact _.
intros ? ? g ? ? f E; cbn.
exact (abses_pushout_pullback_reorder E f g).
Expand Down Expand Up @@ -232,13 +232,13 @@ Defined.
Global Instance is0bifunctor_abses `{Univalence}
: Is0Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
Proof.
rapply Build_Is0Bifunctor.
rapply Build_Is0Bifunctor''.
Defined.

Global Instance is1bifunctor_abses `{Univalence}
: Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
Proof.
snrapply Build_Is1Bifunctor.
snrapply Build_Is1Bifunctor''.
1,2: exact _.
intros ? ? f ? ? g.
rapply hspace_phomotopy_from_homotopy.
Expand Down
20 changes: 12 additions & 8 deletions theories/Algebra/AbSES/Ext.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,9 +63,9 @@ Defined.

(** ** The bifunctor [ab_ext] *)

Definition ab_ext `{Univalence} (B A : AbGroup@{u}) : AbGroup.
Definition ab_ext@{u v|u < v} `{Univalence} (B : AbGroup@{u}^op) (A : AbGroup@{u}) : AbGroup@{v}.
Proof.
snrapply (Build_AbGroup (grp_ext B A)).
snrapply (Build_AbGroup (grp_ext@{u v} B A)).
intros E F.
strip_truncations; cbn.
apply ap.
Expand Down Expand Up @@ -121,16 +121,20 @@ Defined.
Global Instance is0bifunctor_abext `{Univalence}
: Is0Bifunctor (A:=AbGroup^op) ab_ext.
Proof.
rapply Build_Is0Bifunctor.
rapply Build_Is0Bifunctor''.
Defined.

Global Instance is1bifunctor_abext `{Univalence}
: Is1Bifunctor (A:=AbGroup^op) ab_ext.
Proof.
snrapply Build_Is1Bifunctor.
snrapply Build_Is1Bifunctor''.
1,2: exact _.
intros A B.
exact (bifunctor_isbifunctor (Ext : AbGroup^op -> AbGroup -> pType)).
intros A B f C D g.
intros x.
strip_truncations; cbn.
pose proof (bifunctor_coh (Ext : AbGroup^op -> AbGroup -> pType) f g (tr x)) as X.
cbn in X.
exact X.
Defined.

(** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)
Expand All @@ -139,10 +143,10 @@ Definition abses_pushout_ext `{Univalence}
: GroupHomomorphism (ab_hom A G) (ab_ext B G).
Proof.
snrapply Build_GroupHomomorphism.
1: exact (fun f => fmap01 (A:=AbGroup^op) Ext' _ f (tr E)).
1: exact (fun f => fmap (Ext' (_ : AbGroup^op)) f (tr E)).
intros f g; cbn.
nrapply (ap tr).
exact (baer_sum_distributive_pushouts f g).
exact (baer_sum_distributive_pushouts (E:=E) f g).
Defined.

(** ** Extensions ending in a projective are trivial *)
Expand Down
3 changes: 2 additions & 1 deletion theories/Algebra/AbSES/SixTerm.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,8 @@ Proof.
destruct g as [g k].
exists g.
apply path_sigma_hprop; cbn.
exact k^.
elim k^.
by apply equiv_path_grouphomomorphism.
Defined.

(** *** Exactness of [ab_hom A G -> Ext1 B G -> Ext1 E G]. *)
Expand Down
5 changes: 3 additions & 2 deletions theories/Homotopy/Join/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -562,7 +562,8 @@ Section FunctorJoin.

Global Instance is0bifunctor_join : Is0Bifunctor Join.
Proof.
rapply Build_Is0Bifunctor'.
snrapply Build_Is0Bifunctor'.
1,2: exact _.
apply Build_Is0Functor.
intros A B [f g].
exact (functor_join f g).
Expand All @@ -571,7 +572,7 @@ Section FunctorJoin.
Global Instance is1bifunctor_join : Is1Bifunctor Join.
Proof.
snrapply Build_Is1Bifunctor'.
nrapply Build_Is1Functor.
snrapply Build_Is1Functor.
- intros A B f g [p q].
exact (functor2_join p q).
- intros A; exact functor_join_idmap.
Expand Down
15 changes: 1 addition & 14 deletions theories/Homotopy/Join/JoinAssoc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -266,20 +266,7 @@ Proof.
- intros A B C.
apply join_assoc.
- intros [[A B] C] [[A' B'] C'] [[f g] h]; cbn.
(* This is awkward because Monoidal.v works with a tensor that is separately a functor in each variable. *)
intro x.
rhs_V nrapply functor_join_compose.
rhs_V nrapply functor2_join.
2: reflexivity.
2: nrapply functor_join_compose.
cbn.
rhs_V nrapply join_assoc_nat; cbn.
apply ap.
lhs_V nrapply functor_join_compose.
lhs_V nrapply functor_join_compose.
apply functor2_join.
1: reflexivity.
symmetry; nrapply functor_join_compose.
apply join_assoc_nat.
Defined.

(** ** The Triangle Law *)
Expand Down
3 changes: 2 additions & 1 deletion theories/Homotopy/Smash.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,7 +353,8 @@ Defined.

Global Instance is0bifunctor_smash : Is0Bifunctor Smash.
Proof.
rapply Build_Is0Bifunctor'.
snrapply Build_Is0Bifunctor'.
1,2: exact _.
nrapply Build_Is0Functor.
intros [X Y] [A B] [f g].
exact (functor_smash f g).
Expand Down
Loading