Skip to content

Commit

Permalink
more wip
Browse files Browse the repository at this point in the history 
Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: ea4d147b-49fe-4961-8d80-a28e0e471e74 -->
  • Loading branch information
@Alizter
Alizter committed Apr 13, 2024
1 parent dabe0af commit 518a5ad
Show file tree
Hide file tree
Showing 2 changed files with 193 additions and 22 deletions.
8 changes: 8 additions & 0 deletions theories/WildCat/Bifunctor.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,14 @@ Definition fmap01_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
: fmap01 F a g $== fmap11 F (Id a) g
:= ((_ $@L fmap_id _ _) $@ cat_idr _)^$.

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.

(** 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
207 changes: 185 additions & 22 deletions theories/WildCat/Monoidal.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -168,11 +168,7 @@ Section TwistConstruction.
twist a' b' c' $o fmap11 cat_tensor f (fmap11 cat_tensor g h)
$== fmap11 cat_tensor g (fmap11 cat_tensor f h) $o twist a b c)

{left_unitor : LeftUnitor cat_tensor cat_tensor_unit}
{right_unitor : RightUnitor cat_tensor cat_tensor_unit}

(swap_unitor : forall a, cate_fun (left_unitor a)
$== right_unitor a $o swap cat_tensor_unit a)
(right_unitor : RightUnitor cat_tensor cat_tensor_unit)
(twist_unitor : forall a b, fmap01 cat_tensor a (right_unitor b)
$== swap b a $o fmap01 cat_tensor b (right_unitor a) $o twist a b cat_tensor_unit)

Expand All @@ -197,7 +193,6 @@ Section TwistConstruction.
nrefine (swape _ _ $oE _).
nrefine (twiste _ _ _ $oE _).
exact (emap01 cat_tensor a (swape _ _)).
Show Proof.
Defined.

Local Definition associator_twist'_unfold a b c
Expand Down Expand Up @@ -241,7 +236,40 @@ Section TwistConstruction.
apply swap_nat.
Defined.

(** We can prove the triangle identity using two simpler coherences. The first is called [swap_unitor] and asserts that the the left unitor is the right unitor when composed with the [symmetor]. The second is called [twist_unitor] and asserts a reduced version of the triangle identity only mentioning [right_unitor], [swap] and [twist]. *)
Local Instance symmetor_twist : Symmetor cat_tensor.
Proof.
snrapply Build_Symmetor.
- exact swape.
- intros [a b] [c d] [f g].
nrefine ((cate_buildequiv_fun _ $@R _) $@ _).
refine (_ $@ (_ $@L (cate_buildequiv_fun _)^$)).
nrefine (swap_nat _ _ _ _ _ _ $@ (_ $@R _)).
rapply bifunctor_isbifunctor.
Defined.

Local Instance left_unitor_twist : LeftUnitor cat_tensor cat_tensor_unit.
Proof.
snrapply Build_NatEquiv.
- exact (fun a => right_unitor a $oE swape cat_tensor_unit a).
- intros a b f.
change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
nrapply hconcatL.
1: apply cate_buildequiv_fun.
nrapply hconcatR.
2: apply cate_buildequiv_fun.
nrapply vconcat.
2: rapply (isnat right_unitor f).
nrapply hconcatL.
1: apply cate_buildequiv_fun.
nrapply hconcatR.
2: apply cate_buildequiv_fun.
nrapply vconcatL.
1: rapply fmap01_is_fmap11.
nrapply vconcatR.
2: rapply fmap10_is_fmap11.
rapply swap_nat.
Defined.

Local Instance triangle_twist : TriangleIdentity cat_tensor cat_tensor_unit.
Proof.
intros a b.
Expand All @@ -253,8 +281,7 @@ Section TwistConstruction.
nrefine (_ $@L (emap_inv _ _ $@ cate_buildequiv_fun _) $@ _).
refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ _).
{ apply cate_moveR_eV.
refine (_ $@ (_ $@L (cate_buildequiv_fun _)^$)).
apply swap_unitor. }
apply cate_buildequiv_fun. }
refine (_ $@ ((_ $@ (_ $@L (cate_buildequiv_fun _)^$)) $@R _)).
2: { refine (_ $@ ((fmap10_is_fmap11 _ _ _)^$ $@R _)).
apply swap_nat. }
Expand All @@ -268,25 +295,161 @@ Section TwistConstruction.
Proof.
hnf.
intros a b c d.
(** We probably want to unfold equivalences here but we might need to move them around, not quite sure. *)
(* refine ((_ $@@ _) $@ _ $@ (_ $@@ (_ $@R _))^$). *)

Infix "⊗" := cat_tensor (at level 40).
Infix "⊗R" := (fmap01 cat_tensor) (at level 40).
Infix "⊗L" := (fmap10 cat_tensor) (at level 40).
Notation σ := swap.
Notation τ := twist.
Notation α := associator_twist.
Notation "f ∘ g" := (f $o g) (at level 60).

refine (_ $@ (_^$ $@R _)).
2: { refine ((_ $@L associator_twist'_unfold _ _ _) $@ _).
refine ((cat_assoc _ _ _)^$ $@ _).
refine (_ $@R _).
refine ((_ $@R _) $@ _^$).
1: rapply fmap10_is_fmap11.
refine (_ $@ _).
2: apply swap_nat.
refine (_ $@L _).
rapply fmap01_is_fmap11. }

refine (_ $@ ((cat_assoc _ _ _)^$ $@R _)).
refine (_ $@ (cat_assoc _ _ _)^$).

refine ((_ $@R _) $@ _).
1: apply associator_twist'_unfold.
refine (cat_assoc _ _ _ $@ _).
refine (_ $@L _).

refine (_ $@ (_ $@L (fmap2 _ _ $@ _)^$)).
2: apply associator_twist'_unfold.
2: rapply fmap_comp.

refine (_ $@ cat_assoc _ _ _).
refine (_ $@ (_^$ $@R _)).
2: { refine (cat_assoc _ _ _ $@ (_ $@L _)).
refine (cat_assoc _ _ _ $@ _).
refine ((_ $@L _) $@ cat_idr _).
refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
apply swap_swap. }

refine ((_ $@L _) $@ _).
1: apply associator_twist'_unfold.

refine (_ $@ (_ $@L _^$)).
2: rapply fmap_comp.

change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).

refine (_ $@ cat_assoc _ _ _).
refine ((cat_assoc _ _ _)^$ $@ _).
refine ((cat_assoc _ _ _)^$ $@ _).

(** Now we move the first (right-most) symmetry on the RHS to the left. *)
apply (cate_epic_equiv (emap01 cat_tensor a (emap01 cat_tensor b (swape d c)))).
(** Cancelling on the right. *)
refine (_ $@ (cat_assoc _ _ _)^$).
refine (_ $@ (cat_idr _)^$ $@ (_ $@L _^$)).
2: { refine ((_ $@L _) $@ _).
{ refine (cate_buildequiv_fun _ $@ fmap2 _ _).
refine (cate_buildequiv_fun _ $@ fmap2 _ _).
apply cate_buildequiv_fun. }
refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
apply swap_swap. }

refine ((_ $@L _) $@ _).
{ refine (cate_buildequiv_fun _ $@ fmap2 _ _).
refine (cate_buildequiv_fun _ $@ fmap2 _ _).
apply cate_buildequiv_fun. }

do 2 change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).

refine (cat_assoc _ _ _ $@ _).
refine ((_ $@L _) $@ _).
{ refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _).
refine ((_ $@L _) $@ _).
1: rapply fmap01_is_fmap11.
refine (_ $@ _).
1: apply swap_nat.
refine (_^$ $@R _).
rapply fmap10_is_fmap11. }
refine ((_ $@L _) $@ _).
1: rapply fmap_comp.

change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).
refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _).
{ refine (cat_assoc _ _ _ $@ (_ $@L _)).
refine ((_ $@L _) $@ twist_nat _ _ _ _ _ _ _ _ _).
refine (fmap2 _ _ $@ fmap01_is_fmap11 _ _ _).
refine (fmap10_is_fmap11 _ _ _). }
refine (((_ $@L (_^$ $@R _)) $@R _) $@ _).
{ refine (_ $@ fmap22 _ (Id _) _^$).
2: rapply fmap11_id.
rapply fmap10_is_fmap11. }

(** Moving a swap inwards and cancelling. *)
refine ((_ $@R _) $@ _).
{ refine ((cat_assoc _ _ _)^$ $@ _).
refine (_ $@R _).
refine ((cat_assoc _ _ _) $@ _).
refine ((_ $@L _) $@ _).
{ refine ((_ $@L _) $@ _).
1: rapply fmap10_is_fmap11.
refine (_ $@ _).
1: nrapply swap_nat.
refine (_^$ $@R _).
rapply fmap01_is_fmap11. }
refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)).
refine (cat_assoc _ _ _ $@ _).
refine ((_ $@L _) $@ cat_idr _).
refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
rapply swap_swap. }

refine (_ $@ (cat_assoc _ _ _)^$).

refine (_ $@ (_^$ $@R _)).
2: { refine (fmap2 _ _ $@ _).
1: apply associator_twist'_unfold.
refine (fmap_comp _ _ _ $@ _).
refine (_ $@L _).
refine (fmap_comp _ _ _). }
change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).

refine (_ $@ (cat_assoc _ _ _)^$).
refine (_ $@ (_ $@L _)).
2: { refine ((_ $@L _) $@ (cat_assoc _ _ _)^$).
refine (_ $@ cat_assoc _ _ _).
refine (_ $@ (_ $@R _)).
2: { refine (_ $@ (_^$ $@R _)).
2: { refine (fmap01_is_fmap11 _ _ _ $@ fmap22 _ (Id _) _).
rapply fmap01_is_fmap11. }
apply twist_nat. }
refine ((_ $@L _) $@R _).
refine (fmap2 _ _ $@ fmap01_is_fmap11 _ _ _).
rapply fmap01_is_fmap11. }
change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).

refine (_ $@ (_ $@L (_ $@L _))).
2: refine (cat_assoc _ _ _)^$.
refine (_ $@ cat_assoc _ _ _).
refine (_ $@ cat_assoc _ _ _).

(** Goal looks like:

((τ (a ⊗ b) d c ∘ σ (d ⊗ c) (a ⊗ b)) ∘ τ a (d ⊗ c) b) ∘ a ⊗R σ b (d ⊗ c) $==
((d ⊗R σ c (a ⊗ b) ∘ d ⊗R τ a c b) ∘ τ a d (c ⊗ b)) ∘ (a ⊗R (d ⊗R σ b c) ∘ a ⊗R τ b d c)

Not sure if we can simplify any further with naturality. I'm looking for a way to compose something to get this goal out of simpler pieces. If nothing can be found then this might just be the pentagon analgoue of twist. *)

Admitted.

Local Instance ismonoidal_twist
: IsMonoidal A cat_tensor cat_tensor_unit
:= {}.

Local Instance symmetor_twist : Symmetor cat_tensor.
Proof.
snrapply Build_Symmetor.
- exact swape.
- intros [a b] [c d] [f g].
nrefine ((cate_buildequiv_fun _ $@R _) $@ _).
refine (_ $@ (_ $@L (cate_buildequiv_fun _)^$)).
nrefine (swap_nat _ _ _ _ _ _ $@ (_ $@R _)).
rapply bifunctor_isbifunctor.
Defined.

Local Instance hexagon_twist : HexagonIdentity cat_tensor.
Proof.
intros a b c.
Expand Down

0 comments on commit 518a5ad

Please sign in to comment.