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

bifunctor improvements #1925

Merged
merged 2 commits into from
Apr 23, 2024
+170 −22
Merged

bifunctor improvements #1925

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fa70ec2
bifunctor improvements
Alizter Apr 23, 2024
8a95f11
review comments
Alizter Apr 23, 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
192 changes: 170 additions & 22 deletions theories/WildCat/Bifunctor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,21 +4,23 @@ Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans WildCat.

(** * Bifunctors between WildCats *)

(** ** Definition *)

Class Is0Bifunctor {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
(F : A -> B -> C)
:= {
bifunctor_is0functor01 :: forall a, Is0Functor (F a);
bifunctor_is0functor10 :: forall b, Is0Functor (flip F b);
}.
bifunctor_is0functor01 :: forall a, Is0Functor (F a);
bifunctor_is0functor10 :: forall b, Is0Functor (flip F b);
}.

Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F}
:= {
bifunctor_is1functor01 :: forall a : A, Is1Functor (F a);
bifunctor_is1functor10 :: forall b : B, Is1Functor (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_is1functor01 :: forall a : A, Is1Functor (F a);
bifunctor_is1functor10 :: forall b : B, Is1Functor (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
}.

Arguments bifunctor_isbifunctor {A B C} {_ _ _ _ _ _ _ _ _ _ _ _}
F {_ _} {a0 a1} f {b0 b1} g.
Expand Down Expand Up @@ -56,54 +58,180 @@ 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 *)
(** ** Bifunctor lemmas *)

(** *** 1-functorial action *)

(** [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 *)
(** [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. *)
(** [fmap] in both arguments. Note that we made a choice in the order in which to compose, but the bifunctor coherence condition says that both ways agree. *)
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.
:= fmap01 F _ g $o fmap10 F f _.

(** [fmap11] but with the other choice. *)
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.
:= fmap10 F f _ $o fmap01 F _ g.

(** *** Coherence *)

(** The bifunctor coherence condition becomes a 2-cell between the two choices for [fmap11]. *)
Definition fmap11_coh {A B C : Type}
(F : A -> B -> C) `{Is1Bifunctor A B C F}
{a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
: fmap11 F f g $== fmap11' F f g.
Proof.
rapply bifunctor_isbifunctor.
Defined.

(** [fmap11] with right map the identity gives [fmap10]. *)
Definition fmap10_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} (f : a0 $-> a1) (b : B)
: fmap11 F f (Id b) $== fmap10 F f b
:= (fmap_id _ _ $@R _) $@ cat_idl _.

(** [fmap11] with left map the identity gives [fmap01]. *)
Definition fmap01_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
(a : A) {b0 b1 : B} (g : b0 $-> b1)
: fmap11 F (Id a) g $== fmap01 F a g
:= (_ $@L fmap_id _ _) $@ cat_idr _.

(** 2-functorial action *)

Definition fmap02 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
(a : A) {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
: fmap01 F a g $== fmap01 F a g'
:= fmap2 (F a) q.

Definition fmap12 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
: fmap11 F f g $== fmap11 F f g'
:= fmap02 F _ q $@R _.

Definition fmap20 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f') (b : B)
: fmap10 F f b $== fmap10 F f' b
:= fmap2 (flip F b) p.

Definition fmap21 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f') {b0 b1 : B} (g : b0 $-> b1)
: fmap11 F f g $== fmap11 F f' g
:= _ $@L fmap20 F p _.

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')
{a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f')
{b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
: fmap11 F f g $== fmap11 F f' g'
:= fmap2 (flip F _) p $@@ fmap2 (F _) q.
:= fmap20 F p b0 $@@ fmap02 F a1 q.

Global Instance iemap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
(** *** Identity preservation *)

Definition fmap01_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : A) (b : B)
: fmap01 F a (Id b) $== Id (F a b)
:= fmap_id (F a) b.

Definition fmap10_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : A) (b : B)
: fmap10 F (Id a) b $== Id (F a b)
:= fmap_id (flip F b) a.

Definition fmap11_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : A) (b : B)
: fmap11 F (Id a) (Id b) $== Id (F a b).
Proof.
refine ((_ $@@ _) $@ cat_idr _).
1,2: rapply fmap_id.
Defined.

(** *** Composition preservation *)

Definition fmap01_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat 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).
(a : A) {b0 b1 b2 : B} (g : b1 $-> b2) (f : b0 $-> b1)
: fmap01 F a (g $o f) $== fmap01 F a g $o fmap01 F a f
:= fmap_comp (F a) f g.

Definition fmap10_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 a2 : A} (g : a1 $-> a2) (f : a0 $-> a1) (b : B)
: fmap10 F (g $o f) b $== fmap10 F g b $o fmap10 F f b
:= fmap_comp (flip F b) f g.

Definition fmap11_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 a2 : A} (g : a1 $-> a2) (f : a0 $-> a1)
{b0 b1 b2 : B} (k : b1 $-> b2) (h : b0 $-> b1)
: fmap11 F (g $o f) (k $o h) $== fmap11 F g k $o fmap11 F f h.
Proof.
rapply compose_catie'.
exact (iemap (flip F _) f).
refine ((fmap10_comp F _ _ _ $@@ fmap01_comp F _ _ _) $@ _).
refine (cat_assoc _ _ _ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$).
refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ cat_assoc _ _ _).
rapply fmap11_coh.
Defined.

(** *** Equivalence preservation *)

Global Instance iemap10 {A B C : Type} `{HasEquivs A, Is1Cat B, HasEquivs C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} (f : a0 $<~> a1) (b : B)
: CatIsEquiv (fmap10 F f b)
:= iemap (flip F b) f.

Global Instance iemap01 {A B C : Type} `{Is1Cat A, HasEquivs B, HasEquivs C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
(a : A) {b0 b1 : B} (g : b0 $<~> b1)
: CatIsEquiv (fmap01 F a g)
:= iemap (F a) g.

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)
:= compose_catie' _ _.

Definition emap10 {A B C : Type} `{HasEquivs A, Is1Cat B, HasEquivs C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
{a0 a1 : A} (f : a0 $<~> a1) (b : B)
: F a0 b $<~> F a1 b
:= Build_CatEquiv (fmap10 F f b).

Definition emap01 {A B C : Type} `{Is1Cat A, HasEquivs B, HasEquivs C}
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
(a : A) {b0 b1 : B} (g : b0 $<~> b1)
: F a b0 $<~> F a b1
:= Build_CatEquiv (fmap01 F a g).

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).

(** *** Uncurrying *)

(** 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}
Expand Down Expand Up @@ -133,6 +261,26 @@ Proof.
exact (_ $@L bifunctor_isbifunctor F _ _ $@R _).
Defined.

(** ** Flipping bifunctors *)

Definition is0bifunctor_flip {A B C : Type}
(F : A -> B -> C) `{Is0Bifunctor A B C F} : Is0Bifunctor (flip F).
Proof.
snrapply Build_Is0Bifunctor; exact _.
Defined.
Hint Immediate is0bifunctor_flip : typeclass_instances.

Definition is1bifunctor_flip {A B C : Type}
(F : A -> B -> C) `{Is1Bifunctor A B C F} : Is1Bifunctor (flip F).
Proof.
snrapply Build_Is1Bifunctor.
1,2: exact _.
intros a0 a1 f b0 b1 g.
symmetry.
rapply bifunctor_isbifunctor.
Defined.
Hint Immediate is1bifunctor_flip : typeclass_instances.

(** ** Composition of bifunctors *)

(** There are 4 different ways to compose a functor with a bifunctor. *)
Expand Down
Loading