(* -*- mode: coq; mode: visual-line -*-  *)

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

(** ** Indexed product of categories *)

Global Instance isgraph_forall (A : Type) (B : A -> Type)
  `{forall a, IsGraph (B a)}
  : IsGraph (forall a, B a).
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
IsGraph (forall a : A, B a)
Proof.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
IsGraph (forall a : A, B a)
  srapply Build_IsGraph.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
(forall a : A, B a) -> (forall a : A, B a) -> Type
  intros x y; exact (forall (a : A), x a $-> y a).
Defined.

Global Instance is01cat_forall (A : Type) (B : A -> Type)
  `{forall a, IsGraph (B a)} `{forall a, Is01Cat (B a)}
  : Is01Cat (forall a, B a).
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
Is01Cat (forall a : A, B a)
Proof.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
Is01Cat (forall a : A, B a)
  srapply Build_Is01Cat.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
forall a : forall a : A, B a, a $-> a
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
forall (a : forall a : A, B a)
(b c : forall a0 : A, B a0),
(b $-> c) -> (a $-> b) -> a $-> c
  +
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
forall a : forall a : A, B a, a $-> a intros x a; exact (Id (x a)).
  +
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
forall (a : forall a : A, B a)
(b c : forall a0 : A, B a0),
(b $-> c) -> (a $-> b) -> a $-> c intros x y z f g a; exact (f a $o g a).
Defined.

Global Instance is0gpd_forall (A : Type) (B : A -> Type)
  (* Apparently when there's a [forall] there, Coq can't automatically add the [Is01Cat] instance from the [Is0Gpd] instance. *)
  `{forall a, IsGraph (B a)} `{forall a, Is01Cat (B a)} `{forall a, Is0Gpd (B a)}
  : Is0Gpd (forall a, B a).
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
Is0Gpd (forall a : A, B a)
Proof.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
Is0Gpd (forall a : A, B a)
  constructor.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
forall (a : forall a : A, B a)
(b : forall a0 : A, B a0), (a $-> b) -> b $-> a
  intros f g p a; exact ((p a)^$).
Defined.

Global Instance is2graph_forall (A : Type) (B : A -> Type)
  `{forall a, IsGraph (B a)} `{forall a, Is2Graph (B a)}
  : Is2Graph (forall a, B a).
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is2Graph (B a)
Is2Graph (forall a : A, B a)
Proof.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is2Graph (B a)
Is2Graph (forall a : A, B a)
  intros x y; srapply Build_IsGraph.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is2Graph (B a)
x, y: forall a : A, B a
(x $-> y) -> (x $-> y) -> Type
  intros f g; exact (forall a, f a $-> g a).
Defined.

Global Instance is1cat_forall (A : Type) (B : A -> Type)
  `{forall a, IsGraph (B a)} `{forall a, Is01Cat (B a)}
  `{forall a, Is2Graph (B a)} `{forall a, Is1Cat (B a)}
  : Is1Cat (forall a, B a).
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
Is1Cat (forall a : A, B a)
Proof.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
Is1Cat (forall a : A, B a)
  srapply Build_Is1Cat.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b c : forall a0 : A, B a0) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b c : forall a0 : A, B a0) (f : a $-> b),
Is0Functor (cat_precomp c f)
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b c d : forall a0 : A, B a0) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b c d : forall a0 : A, B a0) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o (g $o f) $== h $o g $o f
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b : forall a0 : A, B a0) (f : a $-> b),
Id b $o f $== f
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b : forall a0 : A, B a0) (f : a $-> b),
f $o Id a $== f
  +
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b c : forall a0 : A, B a0) (g : b $-> c),
Is0Functor (cat_postcomp a g) intros x y z h; srapply Build_Is0Functor.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
x, y, z: forall a : A, B a
h: y $-> z
forall a b : x $-> y,
(a $-> b) -> cat_postcomp x h a $-> cat_postcomp x h b
    intros f g p a.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
x, y, z: forall a : A, B a
h: y $-> z
f, g: x $-> y
p: f $-> g
a: A
cat_postcomp x h f a $-> cat_postcomp x h g a
    exact (h a $@L p a).
  +
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b c : forall a0 : A, B a0) (f : a $-> b),
Is0Functor (cat_precomp c f) intros x y z h; srapply Build_Is0Functor.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
x, y, z: forall a : A, B a
h: x $-> y
forall a b : y $-> z,
(a $-> b) -> cat_precomp z h a $-> cat_precomp z h b
    intros f g p a.
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
x, y, z: forall a : A, B a
h: x $-> y
f, g: y $-> z
p: f $-> g
a: A
cat_precomp z h f a $-> cat_precomp z h g a
    exact (p a $@R h a).
  +
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b c d : forall a0 : A, B a0) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f) intros w x y z f g h a; apply cat_assoc.
  +
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b c d : forall a0 : A, B a0) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o (g $o f) $== h $o g $o f intros w x y z f g h a; apply cat_assoc_opp.
  +
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b : forall a0 : A, B a0) (f : a $-> b),
Id b $o f $== f intros x y f a; apply cat_idl.
  +
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is2Graph (B a)
H2: forall a : A, Is1Cat (B a)
forall (a : forall a : A, B a)
(b : forall a0 : A, B a0) (f : a $-> b),
f $o Id a $== f intros x y f a; apply cat_idr.
Defined.