Paths.v

Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core WildCat.TwoOneCat WildCat.NatTrans.

(** * Path groupoids as wild categories *)

(** Not global instances for now *)

(** These are written so that they can be augmented with an existing wildcat structure. For instance, you may partially define a wildcat and ask for paths for the higher cells. *)

(** Any type is a graph with morphisms given by the identity type. *)
Definition isgraph_paths (A : Type) : IsGraph A
  := {| Hom := paths |}.

(** Any graph is a 2-graph with 2-cells given by the identity type. *)
Definition is2graph_paths (A : Type) `{IsGraph A} : Is2Graph A
  := fun _ _ => isgraph_paths _.

(** Any 2-graph is a 3-graph with 3-cells given by the identity type. *)
Definition is3graph_paths (A : Type) `{Is2Graph A} : Is3Graph A
  := fun _ _ => is2graph_paths _.

(** We assume these as instances for the rest of the file with a low priority. *)
Local Existing Instances isgraph_paths is2graph_paths is3graph_paths | 10.

(** Any type has composition and identity morphisms given by path concatenation and reflexivity. *)
Instance is01cat_paths (A : Type) : Is01Cat A
  := {| Id := @idpath _ ; cat_comp := fun _ _ _ x y => concat y x |}.

(** Any type has a 0-groupoid structure with inverse morphisms given by path inversion. *)
Instance is0gpd_paths (A : Type) : Is0Gpd A
  := { gpd_rev := @inverse _ }.

(** Postcomposition is a 0-functor when the 2-cells are paths. *)
Instance is0functor_cat_postcomp_paths (A : Type) `{Is01Cat A}
  (a b c : A) (g : b $-> c)
  : Is0Functor (cat_postcomp a g).A: Type
H: IsGraph A
H0: Is01Cat A
a, b, c: A
g: b $-> c
Is0Functor (cat_postcomp a g)
Proof.A: Type
H: IsGraph A
H0: Is01Cat A
a, b, c: A
g: b $-> c
Is0Functor (cat_postcomp a g)
  snapply Build_Is0Functor.A: Type
H: IsGraph A
H0: Is01Cat A
a, b, c: A
g: b $-> c
forall a0 b0 : a $-> b,
(a0 $-> b0) ->
cat_postcomp a g a0 $-> cat_postcomp a g b0
  exact (@ap _ _ (cat_postcomp a g)).
Defined.

(** Precomposition is a 0-functor when the 2-cells are paths. *)
Instance is0functor_cat_precomp_paths (A : Type) `{Is01Cat A}
  (a b c : A) (f : a $-> b)
  : Is0Functor (cat_precomp c f).A: Type
H: IsGraph A
H0: Is01Cat A
a, b, c: A
f: a $-> b
Is0Functor (cat_precomp c f)
Proof.A: Type
H: IsGraph A
H0: Is01Cat A
a, b, c: A
f: a $-> b
Is0Functor (cat_precomp c f)
  snapply Build_Is0Functor.A: Type
H: IsGraph A
H0: Is01Cat A
a, b, c: A
f: a $-> b
forall a0 b0 : b $-> c,
(a0 $-> b0) ->
cat_precomp c f a0 $-> cat_precomp c f b0
  exact (@ap _ _ (cat_precomp c f)).
Defined.

(** Any type is a 1-category with n-morphisms given by paths. *)
Instance is1cat_paths {A : Type} : Is1Cat A.A: Type
Is1Cat A
Proof.A: Type
Is1Cat A
  snapply Build_Is1Cat.A: Type
forall a b : A, Is01Cat (a $-> b)
A: Type
forall a b : A, Is0Gpd (a $-> b)
A: Type
forall (a b c : A) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A: Type
forall (a b c : A) (f : a $-> b),
Is0Functor (cat_precomp c f)
A: Type
forall (a b c d : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
A: Type
forall (a b c d : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) $== h $o g $o f
A: Type
forall (a b : A) (f : a $-> b), Id b $o f $== f
A: Type
forall (a b : A) (f : a $-> b), f $o Id a $== f
  -A: Type
forall a b : A, Is01Cat (a $-> b) exact _.
  -A: Type
forall a b : A, Is0Gpd (a $-> b) exact _.
  -A: Type
forall (a b c : A) (g : b $-> c),
Is0Functor (cat_postcomp a g) exact _.
  -A: Type
forall (a b c : A) (f : a $-> b),
Is0Functor (cat_precomp c f) exact _.
  -A: Type
forall (a b c d : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f) exact (@concat_p_pp A).
  -A: Type
forall (a b c d : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) $== h $o g $o f exact (@concat_pp_p A).
  -A: Type
forall (a b : A) (f : a $-> b), Id b $o f $== f exact (@concat_p1 A).
  -A: Type
forall (a b : A) (f : a $-> b), f $o Id a $== f exact (@concat_1p A).
Defined.

(** Any type is a 1-groupoid with morphisms given by paths. *)
Instance is1gpd_paths {A : Type} : Is1Gpd A.A: Type
Is1Gpd A
Proof.A: Type
Is1Gpd A
  snapply Build_Is1Gpd.A: Type
forall (a b : A) (f : a $-> b), f^$ $o f $== Id a
A: Type
forall (a b : A) (f : a $-> b), f $o f^$ $== Id b
  -A: Type
forall (a b : A) (f : a $-> b), f^$ $o f $== Id a exact (@concat_pV A).
  -A: Type
forall (a b : A) (f : a $-> b), f $o f^$ $== Id b exact (@concat_Vp A).
Defined.

(** Any type is a 2-category with higher morphisms given by paths. *)
Instance is21cat_paths {A : Type} : Is21Cat A.A: Type
Is21Cat A
Proof.A: Type
Is21Cat A
  snapply Build_Is21Cat.A: Type
forall a b : A, Is1Cat (a $-> b)
A: Type
forall a b : A, Is1Gpd (a $-> b)
A: Type
forall (a b c : A) (g : b $-> c),
Is1Functor (cat_postcomp a g)
A: Type
forall (a b c : A) (f : a $-> b),
Is1Functor (cat_precomp c f)
A: Type
forall (a b c : A) (f f' : a $-> b) (g g' : b $-> c)
(p : f $== f') (p' : g $== g'),
(p' $@R f) $@ (g' $@L p) $== (g $@L p) $@ (p' $@R f')
A: Type
forall (a b c d : A) (f : a $-> b) (g : b $-> c),
Is1Natural (cat_precomp d f o cat_precomp d g)
  (cat_precomp d (g $o f)) (cat_assoc f g)
A: Type
forall (a b c d : A) (f : a $-> b) (h : c $-> d),
Is1Natural (cat_precomp d f o cat_postcomp b h)
  (cat_postcomp a h o cat_precomp c f)
  (fun g : b $-> c => cat_assoc f g h)
A: Type
forall (a b c d : A) (g : b $-> c) (h : c $-> d),
Is1Natural (cat_postcomp a (h $o g))
  (cat_postcomp a h o cat_postcomp a g)
  (fun f : a $-> b => cat_assoc f g h)
A: Type
forall a b : A,
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl
A: Type
forall a b : A,
Is1Natural (cat_precomp b (Id a)) idmap cat_idr
A: Type
forall (a b c d e : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d) (k : d $-> e),
k $@L cat_assoc f g h $o cat_assoc f (h $o g) k $o
cat_assoc g h k $@R f $==
cat_assoc (g $o f) h k $o cat_assoc f g (k $o h)
A: Type
forall (a b c : A) (f : a $-> b) (g : b $-> c),
g $@L cat_idl f $o cat_assoc f (Id b) g $==
cat_idr g $@R f
  -A: Type
forall a b : A, Is1Cat (a $-> b) exact _.
  -A: Type
forall a b : A, Is1Gpd (a $-> b) exact _.
  -A: Type
forall (a b c : A) (g : b $-> c),
Is1Functor (cat_postcomp a g) intros x y z p.A: Type
x, y, z: A
p: y $-> z
Is1Functor (cat_postcomp x p)
    snapply Build_Is1Functor.A: Type
x, y, z: A
p: y $-> z
forall (a b : x $-> y) (f g : a $-> b),
f $== g ->
fmap (cat_postcomp x p) f $==
fmap (cat_postcomp x p) g
A: Type
x, y, z: A
p: y $-> z
forall a : x $-> y,
fmap (cat_postcomp x p) (Id a) $==
Id (cat_postcomp x p a)
A: Type
x, y, z: A
p: y $-> z
forall (a b c : x $-> y) (f : a $-> b) (g : b $-> c),
fmap (cat_postcomp x p) (g $o f) $==
fmap (cat_postcomp x p) g $o fmap (cat_postcomp x p) f
    +A: Type
x, y, z: A
p: y $-> z
forall (a b : x $-> y) (f g : a $-> b),
f $== g ->
fmap (cat_postcomp x p) f $==
fmap (cat_postcomp x p) g intros a b q r.A: Type
x, y, z: A
p: y $-> z
a, b: x $-> y
q, r: a $-> b
q $== r ->
fmap (cat_postcomp x p) q $==
fmap (cat_postcomp x p) r
      exact (ap (fun x => whiskerR x _)).
    +A: Type
x, y, z: A
p: y $-> z
forall a : x $-> y,
fmap (cat_postcomp x p) (Id a) $==
Id (cat_postcomp x p a) reflexivity.
    +A: Type
x, y, z: A
p: y $-> z
forall (a b c : x $-> y) (f : a $-> b) (g : b $-> c),
fmap (cat_postcomp x p) (g $o f) $==
fmap (cat_postcomp x p) g $o fmap (cat_postcomp x p) f intros a b c.A: Type
x, y, z: A
p: y $-> z
a, b, c: x $-> y
forall (f : a $-> b) (g : b $-> c),
fmap (cat_postcomp x p) (g $o f) $==
fmap (cat_postcomp x p) g $o fmap (cat_postcomp x p) f
      exact (whiskerR_pp p).
  -A: Type
forall (a b c : A) (f : a $-> b),
Is1Functor (cat_precomp c f) intros x y z p.A: Type
x, y, z: A
p: x $-> y
Is1Functor (cat_precomp z p)
    snapply Build_Is1Functor.A: Type
x, y, z: A
p: x $-> y
forall (a b : y $-> z) (f g : a $-> b),
f $== g ->
fmap (cat_precomp z p) f $== fmap (cat_precomp z p) g
A: Type
x, y, z: A
p: x $-> y
forall a : y $-> z,
fmap (cat_precomp z p) (Id a) $==
Id (cat_precomp z p a)
A: Type
x, y, z: A
p: x $-> y
forall (a b c : y $-> z) (f : a $-> b) (g : b $-> c),
fmap (cat_precomp z p) (g $o f) $==
fmap (cat_precomp z p) g $o fmap (cat_precomp z p) f
    +A: Type
x, y, z: A
p: x $-> y
forall (a b : y $-> z) (f g : a $-> b),
f $== g ->
fmap (cat_precomp z p) f $== fmap (cat_precomp z p) g intros a b q r.A: Type
x, y, z: A
p: x $-> y
a, b: y $-> z
q, r: a $-> b
q $== r ->
fmap (cat_precomp z p) q $== fmap (cat_precomp z p) r
      exact (ap (whiskerL p)).
    +A: Type
x, y, z: A
p: x $-> y
forall a : y $-> z,
fmap (cat_precomp z p) (Id a) $==
Id (cat_precomp z p a) reflexivity.
    +A: Type
x, y, z: A
p: x $-> y
forall (a b c : y $-> z) (f : a $-> b) (g : b $-> c),
fmap (cat_precomp z p) (g $o f) $==
fmap (cat_precomp z p) g $o fmap (cat_precomp z p) f intros a b c.A: Type
x, y, z: A
p: x $-> y
a, b, c: y $-> z
forall (f : a $-> b) (g : b $-> c),
fmap (cat_precomp z p) (g $o f) $==
fmap (cat_precomp z p) g $o fmap (cat_precomp z p) f
      exact (whiskerL_pp p).
  -A: Type
forall (a b c : A) (f f' : a $-> b) (g g' : b $-> c)
(p : f $== f') (p' : g $== g'),
(p' $@R f) $@ (g' $@L p) $== (g $@L p) $@ (p' $@R f') intros a b c q r s t h g.A: Type
a, b, c: A
q, r: a $-> b
s, t: b $-> c
h: q $== r
g: s $== t
(g $@R q) $@ (t $@L h) $== (s $@L h) $@ (g $@R r)
    exact (concat_whisker q r s t h g)^.
  -A: Type
forall (a b c d : A) (f : a $-> b) (g : b $-> c),
Is1Natural (cat_precomp d f o cat_precomp d g)
  (cat_precomp d (g $o f)) (cat_assoc f g) intros a b c d q r.A: Type
a, b, c, d: A
q: a $-> b
r: b $-> c
Is1Natural (cat_precomp d q o cat_precomp d r)
  (cat_precomp d (r $o q)) (cat_assoc q r)
    snapply Build_Is1Natural.A: Type
a, b, c, d: A
q: a $-> b
r: b $-> c
forall (a0 a' : c $-> d) (f : a0 $-> a'),
cat_assoc q r a' $o
fmap (cat_precomp d q o cat_precomp d r) f $==
fmap (cat_precomp d (r $o q)) f $o cat_assoc q r a0
    intros s t h.A: Type
a, b, c, d: A
q: a $-> b
r: b $-> c
s, t: c $-> d
h: s $-> t
cat_assoc q r t $o
fmap (cat_precomp d q o cat_precomp d r) h $==
fmap (cat_precomp d (r $o q)) h $o cat_assoc q r s
    apply concat_p_pp_nat_r.
  -A: Type
forall (a b c d : A) (f : a $-> b) (h : c $-> d),
Is1Natural (cat_precomp d f o cat_postcomp b h)
  (cat_postcomp a h o cat_precomp c f)
  (fun g : b $-> c => cat_assoc f g h) intros a b c d q r.A: Type
a, b, c, d: A
q: a $-> b
r: c $-> d
Is1Natural (cat_precomp d q o cat_postcomp b r)
  (cat_postcomp a r o cat_precomp c q)
  (fun g : b $-> c => cat_assoc q g r)
    snapply Build_Is1Natural.A: Type
a, b, c, d: A
q: a $-> b
r: c $-> d
forall (a0 a' : b $-> c) (f : a0 $-> a'),
(fun g : b $-> c => cat_assoc q g r) a' $o
fmap (cat_precomp d q o cat_postcomp b r) f $==
fmap (cat_postcomp a r o cat_precomp c q) f $o
(fun g : b $-> c => cat_assoc q g r) a0
    intros s t h.A: Type
a, b, c, d: A
q: a $-> b
r: c $-> d
s, t: b $-> c
h: s $-> t
(fun g : b $-> c => cat_assoc q g r) t $o
fmap (cat_precomp d q o cat_postcomp b r) h $==
fmap (cat_postcomp a r o cat_precomp c q) h $o
(fun g : b $-> c => cat_assoc q g r) s
    apply concat_p_pp_nat_m.
  -A: Type
forall (a b c d : A) (g : b $-> c) (h : c $-> d),
Is1Natural (cat_postcomp a (h $o g))
  (cat_postcomp a h o cat_postcomp a g)
  (fun f : a $-> b => cat_assoc f g h) intros a b c d q r.A: Type
a, b, c, d: A
q: b $-> c
r: c $-> d
Is1Natural (cat_postcomp a (r $o q))
  (cat_postcomp a r o cat_postcomp a q)
  (fun f : a $-> b => cat_assoc f q r)
    snapply Build_Is1Natural.A: Type
a, b, c, d: A
q: b $-> c
r: c $-> d
forall (a0 a' : a $-> b) (f : a0 $-> a'),
(fun f0 : a $-> b => cat_assoc f0 q r) a' $o
fmap (cat_postcomp a (r $o q)) f $==
fmap (cat_postcomp a r o cat_postcomp a q) f $o
(fun f0 : a $-> b => cat_assoc f0 q r) a0
    intros s t h.A: Type
a, b, c, d: A
q: b $-> c
r: c $-> d
s, t: a $-> b
h: s $-> t
(fun f : a $-> b => cat_assoc f q r) t $o
fmap (cat_postcomp a (r $o q)) h $==
fmap (cat_postcomp a r o cat_postcomp a q) h $o
(fun f : a $-> b => cat_assoc f q r) s
    apply concat_p_pp_nat_l.
  -A: Type
forall a b : A,
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl intros a b.A: Type
a, b: A
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl
    snapply Build_Is1Natural.A: Type
a, b: A
forall (a0 a' : a $-> b) (f : a0 $-> a'),
cat_idl a' $o fmap (cat_postcomp a (Id b)) f $==
fmap idmap f $o cat_idl a0
    intros p q h; cbn.A: Type
a, b: A
p, q: a $-> b
h: p $-> q
ap (fun y : a = b => y @ 1) h @ concat_p1 q =
concat_p1 p @ h
    apply moveL_Mp.A: Type
a, b: A
p, q: a $-> b
h: p $-> q
(concat_p1 p)^ @
(ap (fun y : a = b => y @ 1) h @ concat_p1 q) = h
    lhs napply concat_p_pp.A: Type
a, b: A
p, q: a $-> b
h: p $-> q
((concat_p1 p)^ @ ap (fun y : a = b => y @ 1) h) @
concat_p1 q = h
    exact (whiskerR_p1 h).
  -A: Type
forall a b : A,
Is1Natural (cat_precomp b (Id a)) idmap cat_idr intros a b.A: Type
a, b: A
Is1Natural (cat_precomp b (Id a)) idmap cat_idr
    snapply Build_Is1Natural.A: Type
a, b: A
forall (a0 a' : a $-> b) (f : a0 $-> a'),
cat_idr a' $o fmap (cat_precomp b (Id a)) f $==
fmap idmap f $o cat_idr a0
    intros p q h.A: Type
a, b: A
p, q: a $-> b
h: p $-> q
cat_idr q $o fmap (cat_precomp b (Id a)) h $==
fmap idmap h $o cat_idr p
    apply moveL_Mp.A: Type
a, b: A
p, q: a $-> b
h: p $-> q
(cat_idr p)^ @
(cat_idr q $o fmap (cat_precomp b (Id a)) h) =
fmap idmap h
    lhs rapply concat_p_pp.A: Type
a, b: A
p, q: a $-> b
h: p $-> q
((cat_idr p)^ @ fmap (cat_precomp b (Id a)) h) @
cat_idr q = fmap idmap h
    exact (whiskerL_1p h).
  -A: Type
forall (a b c d e : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d) (k : d $-> e),
k $@L cat_assoc f g h $o cat_assoc f (h $o g) k $o
cat_assoc g h k $@R f $==
cat_assoc (g $o f) h k $o cat_assoc f g (k $o h) intros a b c d e p q r s.A: Type
a, b, c, d, e: A
p: a $-> b
q: b $-> c
r: c $-> d
s: d $-> e
s $@L cat_assoc p q r $o cat_assoc p (r $o q) s $o
cat_assoc q r s $@R p $==
cat_assoc (q $o p) r s $o cat_assoc p q (s $o r)
    lhs napply concat_p_pp.A: Type
a, b, c, d, e: A
p: a $-> b
q: b $-> c
r: c $-> d
s: d $-> e
((cat_assoc q r s $@R p) @ cat_assoc p (r $o q) s) @
(s $@L cat_assoc p q r) =
cat_assoc (q $o p) r s $o cat_assoc p q (s $o r)
    exact (pentagon p q r s).
  -A: Type
forall (a b c : A) (f : a $-> b) (g : b $-> c),
g $@L cat_idl f $o cat_assoc f (Id b) g $==
cat_idr g $@R f intros a b c p q.A: Type
a, b, c: A
p: a $-> b
q: b $-> c
q $@L cat_idl p $o cat_assoc p (Id b) q $==
cat_idr q $@R p
    exact (triangulator p q).
Defined.