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
+446 −206
Merged

Update bifunctors #1886

Show file tree
Hide file tree
Changes from 4 commits
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
35 changes: 3 additions & 32 deletions contrib/SetoidRewrite.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ Proof.
intros f1 f2.
apply (is0functor_postcomp a b c g ).
Defined.

#[export] Instance IsProper_catcomp {A : Type} `{Is1Cat A}
{a b c : A}
: CMorphisms.Proper (GpdHom ==> GpdHom ==> GpdHom)
Expand All @@ -111,43 +111,14 @@ Proof.
exact eq_g.
Defined.

#[export] Instance gpd_hom_to_hom_proper {A B: Type} `{Is0Gpd A}
#[export] Instance gpd_hom_to_hom_proper {A B: Type} `{Is0Gpd A}
gio256 marked this conversation as resolved.
Show resolved Hide resolved
{R : Relation B} (F : A -> B)
`{CMorphisms.Proper _ (GpdHom ==> R) F}
: CMorphisms.Proper (Hom ==> R) F.
Proof.
intros a b eq_ab; apply H2; exact eq_ab.
Defined.

#[export] Instance Is1Functor_uncurry_bifunctor {A B C : Type}
jdchristensen marked this conversation as resolved.
Show resolved Hide resolved
`{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C)
`{!Is0Bifunctor F, !Is1Bifunctor F}
: Is1Functor (uncurry F).
Proof.
nrapply Build_Is1Functor.
- intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [eq_fg1 eq_fg2];
cbn in f1, f2, g1, g2, eq_fg1, eq_fg2. cbn.
rewrite eq_fg1, eq_fg2.
reflexivity.
- intros [a b]; cbn.
(* rewrite fmap_id generates an extra goal. Not sure how to get typeclass resolution to figure this out automatically. *)
rewrite (fmap_id _).
rewrite (fmap_id _).
rewrite cat_idl.
reflexivity.
- intros [a1 b1] [a2 b2] [a3 b3] [f1 f2] [g1 g2];
cbn in f1, f2, g1, g2.
cbn.
rewrite (fmap_comp _).
rewrite (fmap_comp _).
rewrite cat_assoc.
rewrite <- (cat_assoc _ (fmap (F a1) g2)).
rewrite <- (bifunctor_isbifunctor F f1 g2).
rewrite ! cat_assoc.
reflexivity.
Defined.

#[export] Instance gpd_hom_is_proper1 {A : Type} `{Is0Gpd A}
: CMorphisms.Proper
(Hom ==> Hom ==> CRelationClasses.arrow) Hom.
Expand Down Expand Up @@ -192,7 +163,7 @@ Defined.

Proposition nat_equiv_faithful {A B : Type}
{F G : A -> B} `{Is1Functor _ _ F}
`{!Is0Functor G, !Is1Functor G}
`{!Is0Functor G, !Is1Functor G}
`{!HasEquivs B} (tau : NatEquiv F G)
: Faithful F -> Faithful G.
Proof.
Expand Down
107 changes: 71 additions & 36 deletions theories/WildCat/Bifunctor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Require Import Basics.Overture Basics.Tactics.
Require Import Types.Forall.
Require Import WildCat.Core WildCat.Prod.
Require Import WildCat.Core WildCat.Prod WildCat.Equiv.

(** * Bifunctors between WildCats *)

Expand Down Expand Up @@ -56,18 +56,84 @@ Definition Build_Is1Bifunctor' {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
: Is1Bifunctor F
:= is1bifunctor_functor_uncurried (uncurry F).

(* fmap in the first argument *)
Definition fmap10 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
(** [fmap] in the first argument *)
Definition fmap10 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
(F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1) (b : B)
: (F a0 b) $-> (F a1 b)
:= fmap (flip F b) f.

(* fmap in the second argument *)
Definition fmap01 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
(** [fmap] in the second argument *)
Definition fmap01 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
(F : A -> B -> C) `{!Is0Bifunctor F} (a : A) {b0 b1 : B} (g : b0 $-> b1)
: F a b0 $-> F a b1
:= fmap (F a) g.

(** There are two ways to [fmap] in both arguments of a bifunctor. The bifunctor coherence condition ([bifunctor_isbifunctor]) states precisely that these two routes agree. *)
Alizter marked this conversation as resolved.
Show resolved Hide resolved
Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1)
{b0 b1 : B} (g : b0 $-> b1)
: F a0 b0 $-> F a1 b1
:= fmap (F _) g $o fmap (flip F _) f.

Definition fmap11' {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1)
{b0 b1 : B} (g : b0 $-> b1)
: F a0 b0 $-> F a1 b1
:= fmap (flip F _) f $o fmap (F _) g.

Definition fmap22 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} {f : a0 $-> a1} {f' : a0 $-> a1}
{b0 b1 : B} {g : b0 $-> b1} {g' : b0 $-> b1}
(p : f $== f') (q : g $== g')
: fmap11 F f g $== fmap11 F f' g'
:= fmap2 (F _) q $@R _ $@ (_ $@L fmap2 (flip F _) p).
jdchristensen marked this conversation as resolved.
Show resolved Hide resolved

Global Instance iemap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} (f : a0 $<~> a1) {b0 b1 : B} (g : b0 $<~> b1)
: CatIsEquiv (fmap11 F f g).
Proof.
rapply compose_catie'.
exact (iemap (flip F _) f).
Defined.

Definition emap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} (f : a0 $<~> a1) {b0 b1 : B} (g : b0 $<~> b1)
: F a0 b0 $<~> F a1 b1
:= Build_CatEquiv (fmap11 F f g).

(** Any 0-bifunctor [A -> B -> C] can be made into a functor from the product category [A * B -> C] in two ways. *)
Global Instance is0functor_uncurry_bifunctor {A B C : Type}
`{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}
: Is0Functor (uncurry F).
Proof.
nrapply Build_Is0Functor.
intros a b [f g].
exact (fmap11 F f g).
Defined.

(** Any 1-bifunctor defines a canonical functor from the product category. *)
Global Instance is1functor_uncurry_bifunctor {A B C : Type}
`{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
`{!Is0Bifunctor F, !Is1Bifunctor F}
: Is1Functor (uncurry F).
Proof.
nrapply Build_Is1Functor.
- intros x y f g [p q].
exact (fmap22 F p q).
- intros x.
refine (fmap_id (F _) _ $@R _ $@ _).
refine (_ $@L fmap_id (flip F _) _ $@ cat_idl _).
- intros x y z f g.
refine (fmap_comp (F _) _ _ $@R _ $@ _).
refine (_ $@L fmap_comp (flip F _) _ _ $@ _).
nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
nrefine (cat_assoc _ _ _ $@R _ $@ _ $@ (cat_assoc_opp _ _ _ $@R _)).
exact (_ $@L bifunctor_isbifunctor F _ _ $@R _).
Defined.

(** Restricting a functor along a bifunctor yields a bifunctor. *)
Global Instance is0bifunctor_compose {A B C D : Type}
`{IsGraph A, IsGraph B, Is1Cat C, Is1Cat D}
Expand Down Expand Up @@ -108,34 +174,3 @@ Proof.
rapply fmap2.
exact (bifunctor_isbifunctor F f g).
Defined.

(** Any 0-bifunctor [A -> B -> C] can be made into a functor from the product category [A * B -> C] in two ways. The bifunctor coherence condition ([bifunctor_isbifunctor]) states precisely that these two routes agree. *)
Global Instance is0functor_uncurry_bifunctor {A B C : Type}
`{IsGraph A, IsGraph B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}
: Is0Functor (uncurry F).
Proof.
nrapply Build_Is0Functor.
intros [a b] [c d] [f g].
exact (fmap (flip F d) f $o fmap (F a) g).
Defined.

(** Any 1-bifunctor defines a canonical functor from the product category. *)
Global Instance is1functor_uncurry_bifunctor {A B C : Type}
`{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
`{!Is0Bifunctor F, !Is1Bifunctor F}
: Is1Functor (uncurry F).
Proof.
nrapply Build_Is1Functor.
- intros x y f g [p q].
refine (fmap2 (flip F _) p $@R _ $@ _).
exact (_ $@L fmap2 (F _) q).
- intros x.
refine (fmap_id (flip F _) _ $@R _ $@ _).
refine (_ $@L fmap_id (F _) _ $@ cat_idl _).
- intros x y z f g.
refine (fmap_comp (flip F _) _ _ $@R _ $@ _).
refine (_ $@L fmap_comp (F _) _ _ $@ _).
refine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
refine (cat_assoc _ _ _ $@R _ $@ _ $@ (cat_assoc_opp _ _ _ $@R _)).
exact (_ $@L (bifunctor_isbifunctor F _ _)^$ $@R _).
Defined.
44 changes: 33 additions & 11 deletions theories/WildCat/DisplayedEquiv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,23 +172,43 @@ Global Instance reflexive_dcate {A} {D : A -> Type} `{DHasEquivs A D} {a : A}
:= did_cate.

(** Equivalences can be composed. *)
Global Instance dcompose_catie {A} {D : A -> Type} `{DHasEquivs A D}
{a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
(g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
: DCatIsEquiv (dcate_fun g' $o' f').
Global Instance dcompose_catie' {A} {D : A -> Type} `{DHasEquivs A D}
{a b c : A} {g : b $-> c} `{!CatIsEquiv g} {f : a $-> b} `{!CatIsEquiv f}
{a' : D a} {b' : D b} {c' : D c}
(g' : DHom g b' c') `{ge' : !DCatIsEquiv g'}
(f' : DHom f a' b') `{fe' : !DCatIsEquiv f'}
: DCatIsEquiv (fe:=compose_catie' g f) (g' $o' f').
Proof.
snrapply dcatie_adjointify.
- exact (dcate_fun f'^-1$' $o' g'^-1$').
- refine (_ $o' _).
1: nrapply (Build_DCatEquiv f')^-1$'; exact fe'.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Having to introduce various "buildequiv" constructions is a little annoying. One thing that would help would be to use pose or set to put these in the context. This also has the advantage of a smaller proof term, since they will be shared. This applies to other parts of the recent changes as well.

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'm having trouble figuring out what exactly to pose in this case. Maybe I'm misinterpreting your suggestion, but I haven't been able to make things cleaner using pose here so far.

I also have a tangential question: when we talk about wanting smaller proof terms, is the goal more readable terms, terms that are easier for coq to handle, or both?

Copy link
Collaborator

Choose a reason for hiding this comment

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

For example, you can add pose (feq' := Build_DCatEquiv f' (fe':=fe')). at the start of the proof, since that term is used twice in the proof. Same for other repeated terms.

In this case, it makes the tactic script easier to read, and also should produce a proof term that is easier for Coq to handle.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Oh I see. I think my confusion was really around the second question in this case, so thank you for clarifying.

Copy link
Collaborator

Choose a reason for hiding this comment

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

If you look at Coq's proof term when the pose command is used, it starts with let feq' := Build_DCatEquiv f' in ..., which shows that this has been factored out. It turns out that feq' appears 40 more times in the proof term (with implicit arguments shown), so this is a non-trivial savings. (BTW, this proof term is around 4000 lines long!)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Interesting. It's very unintuitive to me that this would improve coq's performance, so I greatly appreciate the suggestions.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This comment and the one below also raise two thorny issues with displayed categories I'd like to improve on:

  1. Unification and typeclass search are clearly hindered (e.g. we need exact isd0gpd. everywhere). I would imagine there are more tricks like the above that can be used to help coq along here.
  2. Every change to WildCat/Core.v or WildCat/Equiv.v now needs to be reflected in WildCat/Displayed.v or WildCat/DisplayedEquiv.v, respectively.

nrapply (Build_DCatEquiv g')^-1$'; exact ge'.
- refine (dcat_assoc _ _ _ $@' _).
refine (_ $@L' ((dcate_buildequiv_fun f')^$' $@R' _ ) $@' _).
1: exact isd0gpd_hom.
refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
refine (_ $@L' (dcate_isretr _ $@R' _) $@' _).
refine (_ $@L' (dcate_isretr (Build_DCatEquiv f') $@R' _) $@' _).
refine (_ $@L' dcat_idl _ $@' _).
apply dcate_isretr.
refine ((dcate_buildequiv_fun g')^$' $@R' _ $@' _).
1: exact isd0gpd_hom.
nrapply dcate_isretr.
- refine (dcat_assoc _ _ _ $@' _).
refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
refine (_ $@L' (dcate_issect _ $@R' _) $@' _).
refine (_ $@L' (_ $@L' (dcate_buildequiv_fun g')^$' $@R' _) $@' _).
1: exact isd0gpd_hom.
refine (_ $@L' (dcate_issect (Build_DCatEquiv g') $@R' _) $@' _).
refine (_ $@L' dcat_idl _ $@' _).
apply dcate_issect.
refine (_ $@L' (dcate_buildequiv_fun f')^$' $@' _).
1: exact isd0gpd_hom.
nrapply dcate_issect.
Defined.

Global Instance dcompose_catie {A} {D : A -> Type} `{DHasEquivs A D}
{a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
(g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
: DCatIsEquiv (dcate_fun g' $o' f').
Proof.
rapply dcompose_catie'.
Defined.

Definition dcompose_cate {A} {D : A -> Type} `{DHasEquivs A D}
Expand Down Expand Up @@ -387,8 +407,10 @@ Definition dcate_inv_compose {A} {D : A -> Type} `{DHasEquivs A D}
(dcate_fun (f' $oE' e')^-1$') (dcate_fun (e'^-1$' $oE' f'^-1$')).
Proof.
refine (_ $@' (dcompose_cate_fun e'^-1$' f'^-1$')^$').
- snrapply dcate_inv_adjointify.
- exact isd0gpd_hom.
2: exact isd0gpd_hom.
refine (dcate_inv_adjointify _ _ _ _ $@' _).
refine (dcate_inv2 (dcate_buildequiv_fun _) $@R' _ $@' _).
exact (_ $@L' dcate_inv2 (dcate_buildequiv_fun _)).
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 just skimming this, but I'm seeing lots of proofs getting longer. Can you explain in general what the latest changes are doing?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The idea was to introduce compose_catie' (dcompose_catie'), which is a variant of compose_catie that I think will make it slightly easier to prove when a specific map is an equivalence. The proof is the same, but slightly longer because we need to insert all the Build_CatEquiv terms.

This makes compose_catie a one-liner, but it also made the proof of cate_inv_compose longer as now there are two Build_CatEquiv terms to deal with there. Because of this, dcate_inv_compose also had to get longer.

I thought compose_catie' would be useful in the future (as well as for proving Bifunctor.iemap11), but if it's not strictly better we should revert it. I have also needed it before e.g. to prove that 2-of-6 holds for equivalences.

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 see why factoring compose_catie' out of compose_catie should make subsequent things harder to prove. I suspect that if you prove compose_catie' nicely, it should reduce to the same proof of compose_catie that you had before. But maybe the issue is that if you start with an equivalence, and then build a new equivalence with the same underlying map and same proof that it is an equivalence, you don't get back the equivalence you had? Unfortunately, I'm very busy for the next few days, so I won't have time to look into this, but I encourage you to see if there is a way to make this work out more simply. One obvious alternative is to revert to the old proof of compose_catie, and then define compose_catie' using it, instead of the other way around.

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 will have a look. I suppose I wasn't sure which way around was preferable, but I think it's all resolvable with something like a cate_homotopic lemma.

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 used cate_homotopic to redefine compose_catie' in terms of compose_catie as you suggested. It would also be straightforward to remove one or both of these definitions if it's just simpler to avoid touching equivalences in this PR.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Thanks, that looks reasonable. I thought about this a bit more, and my first intuition was that your previous approach would be better, since normally we first prove IsEquiv and then use that to prove Equiv. But with wild categories, it's trickier, since just from the CatIsEquiv type, you don't have access to any data, such as the inverse. You first have to build the element of CatEquiv, and even then, that gives you a retraction and section for a potentially different map (which is homotopic to the one you started with, but not definitionally equal). So this makes working with CatIsEquiv assumptions awkward. We could (1) throw up our hands and avoid making CatIsEquiv assumptions, instead having CatEquiv assumptions. (2) Add some lemmas that given a map f and a proof of CatIsEquiv f, return the inverse g and the proofs that f itself is a section and a retraction of g. (This is an idiom that you are using in a few places.) (3) Think hard about the definition of HasEquivs and see if there is a way to make this work better. There's a lot of redundancy in HasEquivs, and it's there to try to accommodate different settings, so it might not be possible to do better.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Is (2) something worth a small refactor to make CatIsEquiv assumptions a better default? I guess maybe best to spend some time on (3) first.

Do you know if anyone has tried to factor CatEquiv out of HasEquivs? I'm thinking of whether it's possible to provide the simplicity of a $<~> b without directly including it in HasEquivs.

Copy link
Collaborator

Choose a reason for hiding this comment

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

(3) is definitely something that would take some thought and experimenting, not as part of this PR. I don't know what people have tried. Some "obvious" things, like just getting rid of CatEquiv as data, and instead defining it to be { e : a $-> b & CatIsEquiv e } won't work because we want to be able to use wild categories is situations where there is already an existing notion of equivalence. I'm not sure if that's what you meant by factoring CatEquiv out of HasEquivs`. If you have another idea, please share it.

In the meantime, something like (2) could be part of this PR, since I think it would just mean taking a few repeated idioms and factor them out into lemmas. But it could also be left as something to think about later, and this PR could stay like it is.

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 am happy with leaving this to think on and potentially include in a separate PR for now (assuming others feel the same).

Defined.

Definition dcate_inv_V {A} {D : A -> Type} `{DHasEquivs A D}
Expand Down
44 changes: 28 additions & 16 deletions theories/WildCat/Equiv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ Defined.

Notation "f ^-1$" := (cate_inv f).

Definition cate_issect {A} `{HasEquivs A} {a b} (f : a $<~> b)
Definition cate_issect {A} `{HasEquivs A} {a b} (f : a $<~> b)
: f^-1$ $o f $== Id a.
Proof.
refine (_ $@ cate_issect' a b f).
Expand Down Expand Up @@ -152,23 +152,33 @@ Global Instance symmetric_cate {A} `{HasEquivs A}
:= fun a b f => cate_inv f.

(** Equivalences can be composed. *)
Global Instance compose_catie {A} `{HasEquivs A} {a b c : A}
(g : b $<~> c) (f : a $<~> b)
Definition compose_catie' {A} `{HasEquivs A} {a b c : A}
(g : b $-> c) `{!CatIsEquiv g} (f : a $-> b) `{!CatIsEquiv f}
: CatIsEquiv (g $o f).
Proof.
refine (catie_adjointify _ (f^-1$ $o g^-1$) _ _).
- refine (cat_assoc _ _ _ $@ _).
refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
refine ((_ $@L (cate_isretr _ $@R _)) $@ _).
refine ((_ $@L cat_idl _) $@ _).
apply cate_isretr.
- refine (cat_assoc _ _ _ $@ _).
refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
refine ((_ $@L (cate_issect _ $@R _)) $@ _).
refine ((_ $@L cat_idl _) $@ _).
apply cate_issect.
snrapply catie_adjointify.
- exact ((Build_CatEquiv f)^-1$ $o (Build_CatEquiv g)^-1$).
- nrefine (cat_assoc _ _ _ $@ _).
refine (_ $@L ((cate_buildequiv_fun f)^$ $@R _ ) $@ _).
nrefine (_ $@L cat_assoc_opp _ _ _ $@ _).
nrefine (_ $@L (cate_isretr (Build_CatEquiv f) $@R _) $@ _).
nrefine (_ $@L cat_idl _ $@ _).
refine ((cate_buildequiv_fun g)^$ $@R _ $@ _).
nrapply cate_isretr.
- nrefine (cat_assoc _ _ _ $@ _).
nrefine (_ $@L cat_assoc_opp _ _ _ $@ _).
refine (_ $@L (_ $@L (cate_buildequiv_fun g)^$ $@R _) $@ _).
nrefine (_ $@L (cate_issect (Build_CatEquiv g) $@R _) $@ _).
nrefine (_ $@L cat_idl _ $@ _).
refine (_ $@L (cate_buildequiv_fun f)^$ $@ _).
nrapply cate_issect.
Defined.

Global Instance compose_catie {A} `{HasEquivs A} {a b c : A}
(g : b $<~> c) (f : a $<~> b)
: CatIsEquiv (g $o f)
:= compose_catie' g f.

Definition compose_cate {A} `{HasEquivs A} {a b c : A}
(g : b $<~> c) (f : a $<~> b) : a $<~> c
:= Build_CatEquiv (g $o f).
Expand All @@ -190,7 +200,7 @@ Proof.
apply cate_buildequiv_fun.
Defined.

Definition id_cate_fun {A} `{HasEquivs A} (a : A)
Definition id_cate_fun {A} `{HasEquivs A} (a : A)
: cate_fun (id_cate a) $== Id a.
Proof.
apply cate_buildequiv_fun.
Expand Down Expand Up @@ -325,7 +335,9 @@ Definition cate_inv_compose {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b
: cate_fun (f $oE e)^-1$ $== cate_fun (e^-1$ $oE f^-1$).
Proof.
refine (_ $@ (compose_cate_fun _ _)^$).
apply cate_inv_adjointify.
nrefine (cate_inv_adjointify _ _ _ _ $@ _).
nrefine (cate_inv2 (cate_buildequiv_fun _) $@R _ $@ _).
exact (_ $@L cate_inv2 (cate_buildequiv_fun _)).
jdchristensen marked this conversation as resolved.
Show resolved Hide resolved
Defined.

Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
Expand Down
2 changes: 1 addition & 1 deletion theories/WildCat/Monoidal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Section Monoidal.
Context `{Is1Cat C}.
Context `{HasEquivs C}.
Context (tensor : C -> C -> C).
Context `{!Is0Bifunctor tensor}.
Context `{!Is0Bifunctor tensor, !Is1Bifunctor tensor}.

Definition left_assoc : C -> C -> C -> C :=
fun a b c => tensor (tensor a b) c.
Expand Down
Loading
Loading