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

Update bifunctors #1886

Merged
merged 25 commits into from
Mar 14, 2024
Merged

Update bifunctors #1886

Changes from 1 commit
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
63e3847
Move bifunctor coherence to Is1Bifunctor
gio256 Mar 7, 2024
783f5b9
WildCat/Bifunctor.v: Remove bifunctor_hom lemmas
gio256 Mar 8, 2024
a95509d
AbSES/BaerSum.v: fix proof of is1bifunctor_abses
gio256 Mar 8, 2024
1046b48
WildCat/Bifunctor.v: simplify uncurried proofs
gio256 Mar 8, 2024
62b8d2b
AbGroups/AbHom.v: prove is1bifunctor_ab_hom
gio256 Mar 8, 2024
720075a
AbSES/Ext.v: rough proofs of Is1Bifunctor
gio256 Mar 8, 2024
56d82e7
AbSES/Ext.v: simplify bifunctor proofs for ab_ext
gio256 Mar 9, 2024
2c9fce6
AbSES/Ext.v: remove universe annotations
gio256 Mar 9, 2024
d78a876
Simplify building of bifunctors
gio256 Mar 9, 2024
e19d81e
WildCat/Yoneda.v: Add bifunctor instances for hom
gio256 Mar 9, 2024
f5e4d86
WildCat/Prod.v: add product inclusions
gio256 Mar 9, 2024
192a786
WildCat/Bifunctor.v: remove comment
gio256 Mar 9, 2024
beed14d
AbSES/Ext.v: remove universe annotations
gio256 Mar 9, 2024
f930232
WildCat/Yoneda.v: add comment
gio256 Mar 9, 2024
da5cb5a
WildCat/Monoidal: tensor product is a 1-bifunctor
gio256 Mar 9, 2024
c41d397
WildCat equivs: add compose_catie'
gio256 Mar 10, 2024
2ae47ce
Move bifunctor lemmas from Prod.v to Bifunctor.v
gio256 Mar 10, 2024
1426fd9
WildCat/Bifunctor.v: clean up two proofs
gio256 Mar 11, 2024
b662a72
WildCat equivs: re-define compose_catie'
gio256 Mar 11, 2024
f902579
WildCat equivs fix: cate_homotopic to catie_homotopic
gio256 Mar 12, 2024
c2616da
WildCat/Yoneda.v: opyon_0gpd bifunctor instances
gio256 Mar 13, 2024
07b6ff4
contrib/SetoidRewrite.v: formatting
gio256 Mar 13, 2024
2ed1065
WildCat/Yoneda.v: clean up is0functor_hom_0gpd
gio256 Mar 13, 2024
6c975c1
WildCat/Bifunctor.v: formatting
gio256 Mar 14, 2024
31562d0
WildCat/Yoneda.v: add comment
gio256 Mar 14, 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
39 changes: 37 additions & 2 deletions theories/WildCat/Yoneda.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,12 +44,12 @@ Proof.
Defined.

Global Instance is0bifunctor_hom {A} `{Is01Cat A}
: @Is0Bifunctor A^op A Type _ _ _ (@Hom A _)
: Is0Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _)
:= is0bifunctor_functor_uncurried _.

(** While it is possible to prove the bifunctor coherence condition from [Is1Cat_Strong], 1-functoriality requires morphism extensionality.*)
Global Instance is1bifunctor_hom {A} `{Is1Cat A} `{HasMorExt A}
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you also prove the 0gpd versions which appear further down? Those won't require MorphismExtensionality IIUC.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What do you think about proving is?functor_opyon using the bifunctor instances instead of the explicit proof that is there now? It seems like a repeated proof, but maybe an instructive one.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not certain. I think for now lets keep it repeated and merge it at another point if we think it would be slicker.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe @jdchristensen will have an opinion when he is available.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know exactly what is being discussed, but I'm all in favour of reusing proofs instead of repeating them (if it works smoothly).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tried proving is?functor_opyon using the bifunctor instances, but it leads to a proliferation of extra identity maps in inconvenient places. I will play with it some more, but there might be a reason these weren't proven from the is?functor_hom instances previously, in which case maybe best just to leave a comment explaining why it is proven explicitly.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have added a comment for this now, though I debated leaving no comment instead. It's a bit misleading, because there are really a number of reasons that we prove is0functor_opyon explicitly:

  1. The reason stated in the comment, that using the bifunctor instance leads to extra identity maps in certain places.
  2. It's an important functor, and it's instructive to prove explicitly and useful to control the resulting terms precisely.
  3. It makes it easier to prove is0functor_yon as is0functor_opyon (A:=A^op), which is consistent with how the rest of the contravariant lemmas are proven.
  4. That's the way it is now, and changing it breaks things

: @Is1Bifunctor A^op A Type _ _ _ _ _ _ _ _ _ _ _ _ (@Hom A _) _
: Is1Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _)
:= is1bifunctor_functor_uncurried _.

Definition fun01_hom {A} `{Is01Cat A}
Expand Down Expand Up @@ -229,6 +229,41 @@ Defined.
Definition opyon_0gpd {A : Type} `{Is1Cat A} (a : A) : A -> ZeroGpd
:= fun b => Build_ZeroGpd (a $-> b) _ _ _.

Global Instance is0functor_hom_0gpd {A : Type} `{Is1Cat A}
: Is0Functor (A:=A^op*A) (B:=ZeroGpd) (uncurry (opyon_0gpd (A:=A))).
Proof.
nrapply Build_Is0Functor.
intros [a1 a2] [b1 b2] [f1 f2]; cbn in *.
snrapply Build_Morphism_0Gpd.
- exact (cat_postcomp _ f2 o cat_precomp _ f1).
- rapply (is0functor_compose _ _).
+ apply is0functor_precomp.
+ apply is0functor_postcomp.
jdchristensen marked this conversation as resolved.
Show resolved Hide resolved
Defined.

Global Instance is1functor_hom_0gpd {A : Type} `{Is1Cat A}
: Is1Functor (A:=A^op*A) (B:=ZeroGpd) (uncurry (opyon_0gpd (A:=A))).
Proof.
nrapply Build_Is1Functor.
- intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [p q] h.
exact (h $@L p $@@ q).
- intros [a1 a2] h.
exact (cat_idl _ $@ cat_idr _).
- intros [a1 a2] [b1 b2] [c1 c2] [f1 f2] [g1 g2] h.
refine (cat_assoc _ _ _ $@ _).
refine (g2 $@L _).
refine (_ $@L (cat_assoc_opp _ _ _) $@ _).
exact (cat_assoc_opp _ _ _).
Defined.

Global Instance is0bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
: Is0Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A))
:= is0bifunctor_functor_uncurried _.

Global Instance is1bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
: Is1Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A))
:= is1bifunctor_functor_uncurried _.

Global Instance is0functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
: Is0Functor (opyon_0gpd a).
Proof.
Expand Down
Loading