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

Indexed products and coproducts #1878

Merged
merged 14 commits into from
Mar 8, 2024
Merged

Indexed products and coproducts #1878

Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
d6f7896
indexed products
Alizter Feb 21, 2024
753f213
Indexed products and coproducts
gio256 Feb 26, 2024
d97df59
Fix product functor, specialize to binary product
gio256 Mar 5, 2024
c79a7e6
Add Is1Bifunctor, use bifunctor for binary product
gio256 Mar 6, 2024
5a6b776
WildCat/Bifunctor.v: is1functor_uncurry_bifunctor
gio256 Mar 7, 2024
41bfa82
WildCat/Products.v: replace pick2 with (Bool_rec A)
gio256 Mar 7, 2024
fa7b5c6
WildCat/Bifunctor.v: remove uncurried lemmas
gio256 Mar 7, 2024
146b677
WildCat/Products.v: clean up verbose instances
gio256 Mar 7, 2024
d81bbb5
WildCat/Core.v: remove homotopic functor instances
gio256 Mar 7, 2024
3dec36f
WildCat/Products.v: Cleanup
gio256 Mar 7, 2024
282babf
WildCat/Coproducts.v: clean up imports
gio256 Mar 8, 2024
919fa3d
WildCat/ZeroGroupoid.v: add comments for products
gio256 Mar 8, 2024
63860f1
WildCat/Coproducts.v: show Type has all coproducts
gio256 Mar 8, 2024
eac9352
Clean up proofs of products/coproducts in Type
gio256 Mar 8, 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
63 changes: 57 additions & 6 deletions theories/WildCat/Bifunctor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,19 +8,23 @@ Class IsBifunctor {A B C : Type} `{IsGraph A, IsGraph B, Is1Cat C}
(F : A -> B -> C)
:= {
bifunctor_isfunctor_10 : forall a, Is0Functor (F a);
bifunctor_isfunctor_01 :
forall b, Is0Functor (flip F b);
bifunctor_isbifunctor :
forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
fmap (F _) g $o fmap (flip F _) f $==
fmap (flip F _) f $o fmap (F _) g
bifunctor_isfunctor_01 : forall b, Is0Functor (flip F b);
bifunctor_isbifunctor : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
fmap (F _) g $o fmap (flip F _) f $== fmap (flip F _) f $o fmap (F _) g
}.
jdchristensen marked this conversation as resolved.
Show resolved Hide resolved

#[export] Existing Instance bifunctor_isfunctor_10.
#[export] Existing Instance bifunctor_isfunctor_01.
Arguments bifunctor_isbifunctor {A B C} {_ _ _ _ _ _}
F {_} {a0 a1} f {b0 b1} g.

Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!IsBifunctor F}
:= {
bifunctor_is1functor_10 :: forall a : A, Is1Functor (F a);
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 followed the convention above here, but IMO it's more consistent to remove the final underscores and switch the 10 / 01 suffixes. In my mind bifunctor_is0functor01 should mean that you can fmap in the second argument.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Rather than using indexes maybe we could write _fst and _snd? The index is not immediately understandably IMO.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think either 01/10 without the underscore or _fst/_snd are both fine.

bifunctor_is1functor_01 :: forall b : B, Is1Functor (flip F b);
jdchristensen marked this conversation as resolved.
Show resolved Hide resolved
}.

Definition bifunctor_hom {C : Type} `{IsGraph C}
: C^op -> C -> Type := @Hom C _.

Expand Down Expand Up @@ -73,6 +77,33 @@ Proof.
apply P.
Defined.

Global Instance is1bifunctor_compose {A B C D : Type}
`{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
(F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
`{!IsBifunctor F, !Is1Bifunctor F}
: Is1Bifunctor (fun a b => G (F a b)).
Proof.
nrapply Build_Is1Bifunctor.
- intros x; nrapply Build_Is1Functor.
+ intros a b f g p.
exact (fmap2 G (fmap2 (F x) p)).
+ intros b.
refine (fmap2 G (fmap_id (F x) b) $@ _).
exact (fmap_id G _).
+ intros a b c f g.
refine (fmap2 G (fmap_comp (F x) f g) $@ _).
exact (fmap_comp G _ _).
- intros y; nrapply Build_Is1Functor.
+ intros a b f g p.
exact (fmap2 G (fmap2 (flip F y) p)).
+ intros a.
refine (fmap2 G (fmap_id (flip F y) a) $@ _).
exact (fmap_id G _).
+ intros a b c f g.
refine (fmap2 G (fmap_comp (flip F y) f g) $@ _).
exact (fmap_comp G _ _).
Defined.

(** There are two possible ways to define this, which will only agree in the event that F is a bifunctor. *)
#[export] Instance Is0Functor_uncurry_bifunctor {A B C : Type}
`{IsGraph A, IsGraph B, Is1Cat C}
Expand All @@ -85,3 +116,23 @@ Proof.
unfold uncurry; cbn.
exact ((fmap (flip F b2) f) $o (fmap (F a1) g)).
Defined.

Global Instance is1functor_uncurry_bifunctor {A B C : Type}
`{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
`{!IsBifunctor 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.
Loading
Loading