Skip to content
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

redefine Bifunctor #1952

Merged
merged 10 commits into from
May 7, 2024
Merged

redefine Bifunctor #1952

Show file tree
Hide file tree
Changes from 1 commit
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
4 changes: 2 additions & 2 deletions theories/Algebra/AbSES/Ext.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,13 +121,13 @@ 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 f C D g.
intros x.
Expand Down
3 changes: 3 additions & 0 deletions theories/Homotopy/Join/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -562,13 +562,16 @@ Section FunctorJoin.

Global Instance is0bifunctor_join : Is0Bifunctor Join.
Proof.
snrapply Build_Is0Bifunctor'.
1,2: exact _.
apply Build_Is0Functor.
intros A B [f g].
exact (functor_join f g).
Defined.

Global Instance is1bifunctor_join : Is1Bifunctor Join.
Proof.
snrapply Build_Is1Bifunctor'.
snrapply Build_Is1Functor.
- intros A B f g [p q].
exact (functor2_join p q).
Expand Down
3 changes: 3 additions & 0 deletions theories/Homotopy/Smash.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,13 +353,16 @@ Defined.

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

Global Instance is1bifunctor_smash : Is1Bifunctor Smash.
Proof.
snrapply Build_Is1Bifunctor'.
snrapply Build_Is1Functor.
- intros [X Y] [A B] [f g] [h i] [p q].
exact (functor_smash_homotopic p q).
Expand Down
Loading
Loading