Universe.v

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

(** ** The (1-)category of types *)

Instance isgraph_type@{u v} : IsGraph@{v u} Type@{u}
  := Build_IsGraph Type@{u} (fun a b => a -> b).

Instance is01cat_type : Is01Cat Type.Is01Cat Type
Proof.Is01Cat Type
  econstructor.forall a : Type, a $-> a
forall a b c : Type, (b $-> c) -> (a $-> b) -> a $-> c
  +forall a : Type, a $-> a intro; exact idmap.
  +forall a b c : Type, (b $-> c) -> (a $-> b) -> a $-> c exact (fun a b c g f => g o f).
Defined.

Instance is2graph_type : Is2Graph Type
  := fun x y => Build_IsGraph _ (fun f g => f == g).

Instance is01cat_arrow {A B : Type} : Is01Cat (A $-> B).A, B: Type
Is01Cat (A $-> B)
Proof.A, B: Type
Is01Cat (A $-> B)
  econstructor.A, B: Type
forall a : A $-> B, a $-> a
A, B: Type
forall a b c : A $-> B,
(b $-> c) -> (a $-> b) -> a $-> c
  -A, B: Type
forall a : A $-> B, a $-> a exact (fun f a => idpath).
  -A, B: Type
forall a b c : A $-> B,
(b $-> c) -> (a $-> b) -> a $-> c exact (fun f g h p q a => q a @ p a).
Defined.

Instance is0gpd_arrow {A B : Type}: Is0Gpd (A $-> B).A, B: Type
Is0Gpd (A $-> B)
Proof.A, B: Type
Is0Gpd (A $-> B)
  apply Build_Is0Gpd.A, B: Type
forall a b : A $-> B, (a $-> b) -> b $-> a
  intros f g p a ; exact (p a)^.
Defined.

Instance is0functor_type_postcomp {A B C : Type} (h : B $-> C):
  Is0Functor (cat_postcomp A h).A, B, C: Type
h: B $-> C
Is0Functor (cat_postcomp A h)
Proof.A, B, C: Type
h: B $-> C
Is0Functor (cat_postcomp A h)
  apply Build_Is0Functor.A, B, C: Type
h: B $-> C
forall a b : A $-> B,
(a $-> b) -> cat_postcomp A h a $-> cat_postcomp A h b
  intros f g p a; exact (ap h (p a)).
Defined.

Instance is0functor_type_precomp {A B C : Type} (h : A $-> B):
  Is0Functor (cat_precomp C h).A, B, C: Type
h: A $-> B
Is0Functor (cat_precomp C h)
Proof.A, B, C: Type
h: A $-> B
Is0Functor (cat_precomp C h)
  apply Build_Is0Functor.A, B, C: Type
h: A $-> B
forall a b : B $-> C,
(a $-> b) -> cat_precomp C h a $-> cat_precomp C h b
  intros f g p a; exact (p (h a)).
Defined.

Instance is1cat_strong_type : Is1Cat_Strong Type.Is1Cat_Strong Type
Proof.Is1Cat_Strong Type
  srapply Build_Is1Cat_Strong; cbn; intros; reflexivity.
Defined.

Instance hasmorext_type `{Funext} : HasMorExt Type.H: Funext
HasMorExt Type
Proof.H: Funext
HasMorExt Type
  intros A B f g; cbn in *.H: Funext
A, B: Type
f, g: A -> B
IsEquiv GpdHom_path
  refine (isequiv_homotopic (@apD10 A (fun _ => B) f g) _).H: Funext
A, B: Type
f, g: A -> B
apD10 == GpdHom_path
  intros p.H: Funext
A, B: Type
f, g: A -> B
p: f = g
apD10 p = GpdHom_path p
  destruct p; reflexivity.
Defined.

Instance hasequivs_type : HasEquivs Type.HasEquivs Type
Proof.HasEquivs Type
  srefine (Build_HasEquivs Type _ _ _ _ Equiv (@IsEquiv) _ _ _ _ _ _ _ _); intros A B.A, B: Type
A <~> B -> A $-> B
A, B: Type
forall f : A <~> B,
IsEquiv ((fun A B : Type => ?Goal) A B f)
A, B: Type
forall f : A $-> B, IsEquiv f -> A <~> B
A, B: Type
forall (f : A $-> B) (fe : IsEquiv f),
(fun A B : Type => ?Goal) A B
  ((fun A B : Type => ?Goal1) A B f fe) $== f
A, B: Type
A <~> B -> B $-> A
A, B: Type
forall f : A <~> B,
(fun A B : Type => ?Goal3) A B f $o
(fun A B : Type => ?Goal) A B f $== Id A
A, B: Type
forall f : A <~> B,
(fun A B : Type => ?Goal) A B f $o
(fun A B : Type => ?Goal3) A B f $== Id B
A, B: Type
forall (f : A $-> B) (g : B $-> A),
f $o g $== Id B -> g $o f $== Id A -> IsEquiv f
  all:intros f.A, B: Type
f: A <~> B
A $-> B
A, B: Type
f: A <~> B
IsEquiv
  ((fun (A B : Type) (f : A <~> B) => ?Goal) A B f)
A, B: Type
f: A $-> B
IsEquiv f -> A <~> B
A, B: Type
f: A $-> B
forall fe : IsEquiv f,
(fun (A B : Type) (f : A <~> B) => ?Goal) A B
  ((fun (A B : Type) (f : A $-> B) => ?Goal1) A B f fe) $==
f
A, B: Type
f: A <~> B
B $-> A
A, B: Type
f: A <~> B
(fun (A B : Type) (f : A <~> B) => ?Goal3) A B f $o
(fun (A B : Type) (f : A <~> B) => ?Goal) A B f $==
Id A
A, B: Type
f: A <~> B
(fun (A B : Type) (f : A <~> B) => ?Goal) A B f $o
(fun (A B : Type) (f : A <~> B) => ?Goal3) A B f $==
Id B
A, B: Type
f: A $-> B
forall g : B $-> A,
f $o g $== Id B -> g $o f $== Id A -> IsEquiv f
  -A, B: Type
f: A <~> B
A $-> B exact f.
  -A, B: Type
f: A <~> B
IsEquiv
  ((fun (A B : Type) (f : A <~> B) => equiv_fun f) A B
     f) exact _.
  -A, B: Type
f: A $-> B
IsEquiv f -> A <~> B apply Build_Equiv.
  -A, B: Type
f: A $-> B
forall fe : IsEquiv f,
(fun (A B : Type) (f : A <~> B) => equiv_fun f) A B
  ((fun (A B : Type) (f : A $-> B) =>
    Build_Equiv A B f) A B f fe) $== f intros; reflexivity.
  -A, B: Type
f: A <~> B
B $-> A intros; exact (f^-1).
  -A, B: Type
f: A <~> B
(fun (A B : Type) (f : A <~> B) => f^-1) A B f $o
(fun (A B : Type) (f : A <~> B) => equiv_fun f) A B f $==
Id A cbn.A, B: Type
f: A <~> B
(fun x : A => f^-1 (f x)) == idmap intros ?; apply eissect.
  -A, B: Type
f: A <~> B
(fun (A B : Type) (f : A <~> B) => equiv_fun f) A B f $o
(fun (A B : Type) (f : A <~> B) => f^-1) A B f $==
Id B cbn.A, B: Type
f: A <~> B
(fun x : B => f (f^-1 x)) == idmap intros ?; apply eisretr.
  -A, B: Type
f: A $-> B
forall g : B $-> A,
f $o g $== Id B -> g $o f $== Id A -> IsEquiv f intros g r s; exact (isequiv_adjointify f g r s).
Defined.

Instance hasmorext_core_type `{Funext} : HasMorExt (core Type) := _.

Definition catie_isequiv {A B : Type} {f : A $-> B}
       `{IsEquiv A B f} : CatIsEquiv f.A, B: Type
f: A $-> B
H: IsEquiv f
CatIsEquiv f
Proof.A, B: Type
f: A $-> B
H: IsEquiv f
CatIsEquiv f
  assumption.
Defined.

#[export]
Hint Immediate catie_isequiv : typeclass_instances.

Instance isinitial_zero : IsInitial (A:=Type) Empty.IsInitial Empty
Proof.IsInitial Empty
  intro A.A: Type
{f : Empty $-> A & forall g : Empty $-> A, f $== g}
  exists (Empty_rec _).A: Type
forall g : Empty $-> A, Empty_rec A $== g
  intros g.A: Type
g: Empty $-> A
Empty_rec A $== g
  rapply Empty_ind.
Defined.

Instance isterminal_unit : IsTerminal (A:=Type) Unit.IsTerminal Unit
Proof.IsTerminal Unit
  intros A.A: Type
{f : A $-> Unit & forall g : A $-> Unit, f $== g}
  exists (fun _ => tt).A: Type
forall g : A $-> Unit, (fun _ : A => tt) $== g
  intros f x.A: Type
f: A $-> Unit
x: A
tt = f x
  by destruct (f x).
Defined.

(** ** The 2-category of types *)

Instance is3graph_type : Is3Graph Type.Is3Graph Type
Proof.Is3Graph Type
  intros A B f g.A, B: Type
f, g: A $-> B
IsGraph (f $-> g)
  apply Build_IsGraph.A, B: Type
f, g: A $-> B
(f $-> g) -> (f $-> g) -> Type
  intros p q.A, B: Type
f, g: A $-> B
p, q: f $-> g
Type
  exact (p == q).
Defined.

Instance is1cat_type_hom A B : Is1Cat (A $-> B).A, B: Type
Is1Cat (A $-> B)
Proof.A, B: Type
Is1Cat (A $-> B)
  repeat unshelve esplit.A, B: Type
a, b: A $-> B
forall a0 b0 c : a $-> b,
(b0 $-> c) -> (a0 $-> b0) -> a0 $-> c
A, B: Type
a, b: A $-> B
forall a0 b0 : a $-> b, (a0 $-> b0) -> b0 $-> a0
A, B: Type
a, b, c: A $-> B
g: b $-> c
forall a0 b0 : a $-> b,
(a0 $-> b0) ->
cat_postcomp a g a0 $-> cat_postcomp a g b0
A, B: Type
a, b, c: A $-> B
f: a $-> b
forall a0 b0 : b $-> c,
(a0 $-> b0) ->
cat_precomp c f a0 $-> cat_precomp c f b0
A, B: Type
forall (a b c d : A $-> B) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
A, B: Type
forall (a b c d : A $-> B) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) $== h $o g $o f
A, B: Type
forall (a b : A $-> B) (f : a $-> b), Id b $o f $== f
A, B: Type
forall (a b : A $-> B) (f : a $-> b), f $o Id a $== f
  -A, B: Type
a, b: A $-> B
forall a0 b0 c : a $-> b,
(b0 $-> c) -> (a0 $-> b0) -> a0 $-> c intros f g h p q x.A, B: Type
a, b: A $-> B
f, g, h: a $-> b
p: g $-> h
q: f $-> g
x: A
f x = h x
    exact (q x @ p x).
  -A, B: Type
a, b: A $-> B
forall a0 b0 : a $-> b, (a0 $-> b0) -> b0 $-> a0 intros; by symmetry.
  -A, B: Type
a, b, c: A $-> B
g: b $-> c
forall a0 b0 : a $-> b,
(a0 $-> b0) ->
cat_postcomp a g a0 $-> cat_postcomp a g b0 intros f h p x.A, B: Type
a, b, c: A $-> B
g: b $-> c
f, h: a $-> b
p: f $-> h
x: A
cat_postcomp a g f x = cat_postcomp a g h x
    exact (p x @@ 1).
  -A, B: Type
a, b, c: A $-> B
f: a $-> b
forall a0 b0 : b $-> c,
(a0 $-> b0) ->
cat_precomp c f a0 $-> cat_precomp c f b0 intros g h p x.A, B: Type
a, b, c: A $-> B
f: a $-> b
g, h: b $-> c
p: g $-> h
x: A
cat_precomp c f g x = cat_precomp c f h x
    exact (1 @@ p x).
  -A, B: Type
forall (a b c d : A $-> B) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f) intros ? ? ? ? ? ? ? ?; apply concat_p_pp.
  -A, B: Type
forall (a b c d : A $-> B) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) $== h $o g $o f intros ? ? ? ? ? ? ? ?; apply concat_pp_p.
  -A, B: Type
forall (a b : A $-> B) (f : a $-> b), Id b $o f $== f intros ? ? ? ?.A, B: Type
a, b: A $-> B
f: a $-> b
x: A
(Id b $o f) x = f x apply concat_p1.
  -A, B: Type
forall (a b : A $-> B) (f : a $-> b), f $o Id a $== f intros ? ? ? ?.A, B: Type
a, b: A $-> B
f: a $-> b
x: A
(f $o Id a) x = f x apply concat_1p.
Defined.

Instance is1gpd_type_hom (A B : Type) : Is1Gpd (A $-> B).A, B: Type
Is1Gpd (A $-> B)
Proof.A, B: Type
Is1Gpd (A $-> B)
  repeat unshelve esplit.A, B: Type
forall (a b : A $-> B) (f : a $-> b),
f^$ $o f $== Id a
A, B: Type
forall (a b : A $-> B) (f : a $-> b),
f $o f^$ $== Id b
  -A, B: Type
forall (a b : A $-> B) (f : a $-> b),
f^$ $o f $== Id a intros ? ? ? ?; apply concat_pV.
  -A, B: Type
forall (a b : A $-> B) (f : a $-> b),
f $o f^$ $== Id b intros ? ? ? ?; apply concat_Vp.
Defined.

Instance is1functor_cat_postcomp {A B C : Type} (g : B $-> C)
  : Is1Functor (cat_postcomp A g).A, B, C: Type
g: B $-> C
Is1Functor (cat_postcomp A g)
Proof.A, B, C: Type
g: B $-> C
Is1Functor (cat_postcomp A g)
  repeat unshelve esplit.A, B, C: Type
g: B $-> C
forall (a b : A $-> B) (f g0 : a $-> b),
f $== g0 ->
fmap (cat_postcomp A g) f $==
fmap (cat_postcomp A g) g0
A, B, C: Type
g: B $-> C
forall (a b c : A $-> B) (f : a $-> b) (g0 : b $-> c),
fmap (cat_postcomp A g) (g0 $o f) $==
fmap (cat_postcomp A g) g0 $o
fmap (cat_postcomp A g) f
  -A, B, C: Type
g: B $-> C
forall (a b : A $-> B) (f g0 : a $-> b),
f $== g0 ->
fmap (cat_postcomp A g) f $==
fmap (cat_postcomp A g) g0 intros ? ? ? ? p ?; exact (ap _ (p _)).
  -A, B, C: Type
g: B $-> C
forall (a b c : A $-> B) (f : a $-> b) (g0 : b $-> c),
fmap (cat_postcomp A g) (g0 $o f) $==
fmap (cat_postcomp A g) g0 $o
fmap (cat_postcomp A g) f intros ? ? ? ? ? ?; cbn; apply ap_pp.
Defined.

Instance is1functor_cat_precomp {A B C : Type} (f : A $-> B)
  : Is1Functor (cat_precomp C f).A, B, C: Type
f: A $-> B
Is1Functor (cat_precomp C f)
Proof.A, B, C: Type
f: A $-> B
Is1Functor (cat_precomp C f)
  repeat unshelve esplit.A, B, C: Type
f: A $-> B
forall (a b : B $-> C) (f0 g : a $-> b),
f0 $== g ->
fmap (cat_precomp C f) f0 $== fmap (cat_precomp C f) g
  intros ? ? ? ? p ?; exact (p _).
Defined.

Instance is21cat_type : Is21Cat Type.Is21Cat Type
Proof.Is21Cat Type
  snapply Build_Is21Cat.forall a b : Type, Is1Cat (a $-> b)
forall a b : Type, Is1Gpd (a $-> b)
forall (a b c : Type) (g : b $-> c),
Is1Functor (cat_postcomp a g)
forall (a b c : Type) (f : a $-> b),
Is1Functor (cat_precomp c f)
forall (a b c : Type) (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')
forall (a b c d : Type) (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)
forall (a b c d : Type) (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)
forall (a b c d : Type) (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)
forall a b : Type,
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl
forall a b : Type,
Is1Natural (cat_precomp b (Id a)) idmap cat_idr
forall (a b c d e : Type) (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)
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
g $@L cat_idl f $o cat_assoc f (Id b) g $==
cat_idr g $@R f
  1-4, 6-7: exact _.forall (a b c : Type) (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')
forall (a b c d : Type) (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)
forall a b : Type,
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl
forall a b : Type,
Is1Natural (cat_precomp b (Id a)) idmap cat_idr
forall (a b c d e : Type) (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)
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
g $@L cat_idl f $o cat_assoc f (Id b) g $==
cat_idr g $@R f
  -forall (a b c : Type) (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 f g h k p q x; cbn.a, b, c: Type
f, g: a $-> b
h, k: b $-> c
p: f $== g
q: h $== k
x: a
q (f x) @ ap k (p x) = ap h (p x) @ q (g x)
    symmetry.a, b, c: Type
f, g: a $-> b
h, k: b $-> c
p: f $== g
q: h $== k
x: a
ap h (p x) @ q (g x) = q (f x) @ ap k (p x)
    apply concat_Ap.
  -forall (a b c d : Type) (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 f g.a, b, c, d: Type
f: b $-> c
g: c $-> d
Is1Natural (cat_postcomp a (g $o f))
  (cat_postcomp a g o cat_postcomp a f)
  (fun f0 : a $-> b => cat_assoc f0 f g)
    snapply Build_Is1Natural.a, b, c, d: Type
f: b $-> c
g: c $-> d
forall (a0 a' : a $-> b) (f0 : a0 $-> a'),
(fun f1 : a $-> b => cat_assoc f1 f g) a' $o
fmap (cat_postcomp a (g $o f)) f0 $==
fmap (cat_postcomp a g o cat_postcomp a f) f0 $o
(fun f1 : a $-> b => cat_assoc f1 f g) a0
    intros h i p x; cbn.a, b, c, d: Type
f: b $-> c
g: c $-> d
h, i: a $-> b
p: h $-> i
x: a
ap (fun x : b => g (f x)) (p x) @ 1 =
1 @ ap g (ap f (p x))
    exact (concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
  -forall a b : Type,
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl intros a b.a, b: Type
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl
    snapply Build_Is1Natural.a, b: Type
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 f g p x; cbn.a, b: Type
f, g: a $-> b
p: f $-> g
x: a
ap idmap (p x) @ 1 = 1 @ p x
    exact (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
  -forall a b : Type,
Is1Natural (cat_precomp b (Id a)) idmap cat_idr intros a b.a, b: Type
Is1Natural (cat_precomp b (Id a)) idmap cat_idr
    snapply Build_Is1Natural.a, b: Type
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 f g p x; cbn.a, b: Type
f, g: a $-> b
p: f $-> g
x: a
p x @ 1 = 1 @ p x
    exact (concat_p1 _ @ (concat_1p _)^).
  -forall (a b c d e : Type) (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) reflexivity.
  -forall (a b c : Type) (f : a $-> b) (g : b $-> c),
g $@L cat_idl f $o cat_assoc f (Id b) g $==
cat_idr g $@R f reflexivity.
Defined.