Library HoTT.WildCat.Paths
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.
Require Import WildCat.Core WildCat.TwoOneCat.
Require Import WildCat.Core WildCat.TwoOneCat.
Local Instance isgraph_paths (A : Type) : IsGraph A.
Proof.
constructor.
intros x y; exact (x = y).
Defined.
Local Instance is01cat_paths (A : Type) : Is01Cat A.
Proof.
unshelve econstructor.
- intros a; reflexivity.
- intros a b c q p; exact (p @ q).
Defined.
Local Instance is0gpd_paths (A : Type) : Is0Gpd A.
Proof.
constructor.
intros x y p; exact (p^).
Defined.
Local Instance is2graph_paths (A : Type) : Is2Graph A := fun _ _ ⇒ _.
Local Instance is3graph_paths (A : Type) : Is3Graph A := fun _ _ ⇒ _.
Local Instance is1cat_paths {A : Type} : Is1Cat A.
Proof.
snrapply Build_Is1Cat.
- exact _.
- exact _.
- intros x y z p.
snrapply Build_Is0Functor.
intros q r h.
exact (whiskerR h p).
- intros x y z p.
snrapply Build_Is0Functor.
intros q r h.
exact (whiskerL p h).
- intros w x y z p q r.
exact (concat_p_pp p q r).
- intros w x y z p q r.
exact (concat_pp_p p q r).
- intros x y p.
exact (concat_p1 p).
- intros x y p.
exact (concat_1p p).
Defined.
Local Instance is1gpd_paths {A : Type} : Is1Gpd A.
Proof.
snrapply Build_Is1Gpd.
- intros x y p.
exact (concat_pV p).
- intros x y p.
exact (concat_Vp p).
Defined.
Local Instance is21cat_paths {A : Type} : Is21Cat A.
Proof.
snrapply Build_Is21Cat.
- exact _.
- exact _.
- intros x y z p.
snrapply Build_Is1Functor.
+ intros a b q r h.
exact (ap (fun x ⇒ whiskerR x _) h).
+ reflexivity.
+ intros a b c q r.
exact (whiskerR_pp p q r).
- intros x y z p.
snrapply Build_Is1Functor.
+ intros a b q r h.
exact (ap (whiskerL p) h).
+ reflexivity.
+ intros a b c q r.
exact (whiskerL_pp p q r).
- intros a b c q r s t h g.
exact (concat_whisker q r s t h g)^.
- intros a b c d q r s t h.
apply concat_p_pp_nat_r.
- intros a b c d q r s t h.
apply concat_p_pp_nat_m.
- intros a b c d q r s t h.
apply concat_p_pp_nat_l.
- intros a b p q h; cbn.
apply moveL_Mp.
lhs nrapply concat_p_pp.
exact (whiskerR_p1 h).
- intros a b p q h.
apply moveL_Mp.
lhs rapply concat_p_pp.
exact (whiskerL_1p h).
- intros a b c d e p q r s.
lhs nrapply concat_p_pp.
exact (pentagon p q r s).
- intros a b c p q.
exact (triangulator p q).
Defined.
Proof.
constructor.
intros x y; exact (x = y).
Defined.
Local Instance is01cat_paths (A : Type) : Is01Cat A.
Proof.
unshelve econstructor.
- intros a; reflexivity.
- intros a b c q p; exact (p @ q).
Defined.
Local Instance is0gpd_paths (A : Type) : Is0Gpd A.
Proof.
constructor.
intros x y p; exact (p^).
Defined.
Local Instance is2graph_paths (A : Type) : Is2Graph A := fun _ _ ⇒ _.
Local Instance is3graph_paths (A : Type) : Is3Graph A := fun _ _ ⇒ _.
Local Instance is1cat_paths {A : Type} : Is1Cat A.
Proof.
snrapply Build_Is1Cat.
- exact _.
- exact _.
- intros x y z p.
snrapply Build_Is0Functor.
intros q r h.
exact (whiskerR h p).
- intros x y z p.
snrapply Build_Is0Functor.
intros q r h.
exact (whiskerL p h).
- intros w x y z p q r.
exact (concat_p_pp p q r).
- intros w x y z p q r.
exact (concat_pp_p p q r).
- intros x y p.
exact (concat_p1 p).
- intros x y p.
exact (concat_1p p).
Defined.
Local Instance is1gpd_paths {A : Type} : Is1Gpd A.
Proof.
snrapply Build_Is1Gpd.
- intros x y p.
exact (concat_pV p).
- intros x y p.
exact (concat_Vp p).
Defined.
Local Instance is21cat_paths {A : Type} : Is21Cat A.
Proof.
snrapply Build_Is21Cat.
- exact _.
- exact _.
- intros x y z p.
snrapply Build_Is1Functor.
+ intros a b q r h.
exact (ap (fun x ⇒ whiskerR x _) h).
+ reflexivity.
+ intros a b c q r.
exact (whiskerR_pp p q r).
- intros x y z p.
snrapply Build_Is1Functor.
+ intros a b q r h.
exact (ap (whiskerL p) h).
+ reflexivity.
+ intros a b c q r.
exact (whiskerL_pp p q r).
- intros a b c q r s t h g.
exact (concat_whisker q r s t h g)^.
- intros a b c d q r s t h.
apply concat_p_pp_nat_r.
- intros a b c d q r s t h.
apply concat_p_pp_nat_m.
- intros a b c d q r s t h.
apply concat_p_pp_nat_l.
- intros a b p q h; cbn.
apply moveL_Mp.
lhs nrapply concat_p_pp.
exact (whiskerR_p1 h).
- intros a b p q h.
apply moveL_Mp.
lhs rapply concat_p_pp.
exact (whiskerL_1p h).
- intros a b c d e p q r s.
lhs nrapply concat_p_pp.
exact (pentagon p q r s).
- intros a b c p q.
exact (triangulator p q).
Defined.