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.

(** * Path groupoids as wild categories *)

(** Not global instances for now *)
Local Instance isgraph_paths (A : Type) : IsGraph A.
A: Type
IsGraph A
Proof.
A: Type
IsGraph A
  constructor.
A: Type
A -> A -> Type
  intros x y; exact (x = y).
Defined.

Local Instance is01cat_paths (A : Type) : Is01Cat A.
A: Type
Is01Cat A
Proof.
A: Type
Is01Cat A
  unshelve econstructor.
A: Type
forall a : A, a $-> a
A: Type
forall a b c : A, (b $-> c) -> (a $-> b) -> a $-> c
  -
A: Type
forall a : A, a $-> a intros a; reflexivity.
  -
A: Type
forall a b c : A, (b $-> c) -> (a $-> b) -> a $-> c intros a b c q p; exact (p @ q).
Defined.

Local Instance is0gpd_paths (A : Type) : Is0Gpd A.
A: Type
Is0Gpd A
Proof.
A: Type
Is0Gpd A
  constructor.
A: Type
forall a b : A, (a $-> b) -> b $-> a
  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.
A: Type
Is1Cat A
Proof.
A: Type
Is1Cat A
  snrapply 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) intros x y z p.
A: Type
x, y, z: A
p: y $-> z
Is0Functor (cat_postcomp x p)
    snrapply Build_Is0Functor.
A: Type
x, y, z: A
p: y $-> z
forall a b : x $-> y,
(a $-> b) -> cat_postcomp x p a $-> cat_postcomp x p b
    intros q r h.
A: Type
x, y, z: A
p: y $-> z
q, r: x $-> y
h: q $-> r
cat_postcomp x p q $-> cat_postcomp x p r
    exact (whiskerR h p).
  -
A: Type
forall (a b c : A) (f : a $-> b),
Is0Functor (cat_precomp c f) intros x y z p.
A: Type
x, y, z: A
p: x $-> y
Is0Functor (cat_precomp z p)
    snrapply Build_Is0Functor.
A: Type
x, y, z: A
p: x $-> y
forall a b : y $-> z,
(a $-> b) -> cat_precomp z p a $-> cat_precomp z p b
    intros q r h.
A: Type
x, y, z: A
p: x $-> y
q, r: y $-> z
h: q $-> r
cat_precomp z p q $-> cat_precomp z p r
    exact (whiskerL p h).
  -
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) intros w x y z p q r.
A: Type
w, x, y, z: A
p: w $-> x
q: x $-> y
r: y $-> z
r $o q $o p $== r $o (q $o p)
    exact (concat_p_pp p q r).
  -
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 intros w x y z p q r.
A: Type
w, x, y, z: A
p: w $-> x
q: x $-> y
r: y $-> z
r $o (q $o p) $== r $o q $o p
    exact (concat_pp_p p q r).
  -
A: Type
forall (a b : A) (f : a $-> b), Id b $o f $== f intros x y p.
A: Type
x, y: A
p: x $-> y
Id y $o p $== p
    exact (concat_p1 p).
  -
A: Type
forall (a b : A) (f : a $-> b), f $o Id a $== f intros x y p.
A: Type
x, y: A
p: x $-> y
p $o Id x $== p
    exact (concat_1p p).
Defined.

Local Instance is1gpd_paths {A : Type} : Is1Gpd A.
A: Type
Is1Gpd A
Proof.
A: Type
Is1Gpd A
  snrapply 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 intros x y p.
A: Type
x, y: A
p: x $-> y
p^$ $o p $== Id x
    exact (concat_pV p).
  -
A: Type
forall (a b : A) (f : a $-> b), f $o f^$ $== Id b intros x y p.
A: Type
x, y: A
p: x $-> y
p $o p^$ $== Id y
    exact (concat_Vp p).
Defined.

Local Instance is21cat_paths {A : Type} : Is21Cat A.
A: Type
Is21Cat A
Proof.
A: Type
Is21Cat A
  snrapply 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),
NatTrans.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),
NatTrans.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),
NatTrans.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,
NatTrans.Is1Natural (cat_postcomp a (Id b)) idmap
  cat_idl
A: Type
forall a b : A,
NatTrans.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)
    snrapply 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 h.
A: Type
x, y, z: A
p: y $-> z
a, b: x $-> y
q, r: a $-> b
h: q $== r
fmap (cat_postcomp x p) q $==
fmap (cat_postcomp x p) r
      exact (ap (fun x => whiskerR x _) h).
    +
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 q r.
A: Type
x, y, z: A
p: y $-> z
a, b, c: x $-> y
q: a $-> b
r: b $-> c
fmap (cat_postcomp x p) (r $o q) $==
fmap (cat_postcomp x p) r $o fmap (cat_postcomp x p) q
      exact (whiskerR_pp p q r).
  -
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)
    snrapply 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 h.
A: Type
x, y, z: A
p: x $-> y
a, b: y $-> z
q, r: a $-> b
h: q $== r
fmap (cat_precomp z p) q $== fmap (cat_precomp z p) r
      exact (ap (whiskerL p) h).
    +
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 q r.
A: Type
x, y, z: A
p: x $-> y
a, b, c: y $-> z
q: a $-> b
r: b $-> c
fmap (cat_precomp z p) (r $o q) $==
fmap (cat_precomp z p) r $o fmap (cat_precomp z p) q
      exact (whiskerL_pp p q r).
  -
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),
NatTrans.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 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),
NatTrans.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 s t h.
A: Type
a, b, c, d: A
q: a $-> b
r: c $-> d
s, t: b $-> c
h: s $-> t
cat_assoc q t r $o
fmap (cat_precomp d q o cat_postcomp b r) h $==
fmap (cat_postcomp a r o cat_precomp c q) h $o
cat_assoc q s r
    apply concat_p_pp_nat_m.
  -
A: Type
forall (a b c d : A) (g : b $-> c) (h : c $-> d),
NatTrans.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 s t h.
A: Type
a, b, c, d: A
q: b $-> c
r: c $-> d
s, t: a $-> b
h: s $-> t
cat_assoc t q r $o fmap (cat_postcomp a (r $o q)) h $==
fmap (cat_postcomp a r o cat_postcomp a q) h $o
cat_assoc s q r
    apply concat_p_pp_nat_l.
  -
A: Type
forall a b : A,
NatTrans.Is1Natural (cat_postcomp a (Id b)) idmap
  cat_idl intros a b p q h; cbn.
A: Type
a, b: A
p, q: a $-> b
h: p $-> q
whiskerR h 1 @ 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)^ @ (whiskerR h 1 @ concat_p1 q) = h
    lhs nrapply concat_p_pp.
A: Type
a, b: A
p, q: a $-> b
h: p $-> q
((concat_p1 p)^ @ whiskerR h 1) @ concat_p1 q = h
    exact (whiskerR_p1 h).
  -
A: Type
forall a b : A,
NatTrans.Is1Natural (cat_precomp b (Id a)) idmap
  cat_idr intros a b 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 nrapply 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.