Displayed.v

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

Class IsDGraph {A : Type} `{IsGraph A} (D : A -> Type)
  := DHom : forall {a b : A}, (a $-> b) -> D a -> D b -> Type.

Class IsD01Cat {A : Type} `{Is01Cat A} (D : A -> Type) `{!IsDGraph D} :=
{
  DId : forall {a : A} (a' : D a), DHom (Id a) a' a';
  dcat_comp : forall {a b c : A} {g : b $-> c} {f : a $-> b}
              {a' : D a} {b' : D b} {c' : D c},
              DHom g b' c' -> DHom f a' b' -> DHom (g $o f) a' c';
}.

Notation "g '$o'' f" := (dcat_comp g f).

Definition dcat_postcomp {A : Type} {D : A -> Type} `{IsD01Cat A D} {a b c : A}
  {g : b $-> c} {a' : D a} {b' : D b} {c' : D c} (g' : DHom g b' c')
  : forall (f : a $-> b), DHom f a' b' -> DHom (g $o f) a' c'
  := fun _ f' => g' $o' f'.

Definition dcat_precomp {A : Type} {D : A -> Type} `{IsD01Cat A D} {a b c : A}
  {f : a $-> b} {a' : D a} {b' : D b} {c' : D c} (f' : DHom f a' b')
  : forall (g : b $-> c), DHom g b' c' -> DHom (g $o f) a' c'
  := fun _ g' => g' $o' f'.

Class IsD0Gpd {A : Type} `{Is0Gpd A} (D : A -> Type)
  `{!IsDGraph D, !IsD01Cat D}
  := dgpd_rev : forall {a b : A} {f : a $== b} {a' : D a} {b' : D b},
                DHom f a' b' -> DHom (f^$) b' a'.

Notation "p ^$'" := (dgpd_rev p).

Definition DGpdHom {A : Type} {D : A -> Type} `{IsD0Gpd A D} {a b : A}
  (f : a $== b) (a' : D a) (b' : D b)
  := DHom f a' b'.

(** Diagrammatic order to match gpd_comp *)
Definition dgpd_comp {A : Type} {D : A -> Type} `{IsD0Gpd A D} {a b c : A}
  {f : a $== b} {g : b $== c} {a' : D a} {b' : D b} {c' : D c}
  : DGpdHom f a' b' -> DGpdHom g b' c' -> DGpdHom (g $o f) a' c'
  := fun f' g' => g' $o' f'.

Notation "p '$@'' q" := (dgpd_comp p q).

Definition DHom_path {A : Type} {D : A -> Type} `{IsD01Cat A D} {a b : A}
  (p : a = b) {a' : D a} {b': D b} (p' : transport D p a' = b')
  : DHom (Hom_path p) a' b'.A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
a, b: A
p: a = b
a': D a
b': D b
p': transport D p a' = b'
DHom (Hom_path p) a' b'
Proof.A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
a, b: A
p: a = b
a': D a
b': D b
p': transport D p a' = b'
DHom (Hom_path p) a' b'
  destruct p, p'; apply DId.
Defined.

Definition DGpdHom_path {A : Type} {D : A -> Type} `{IsD0Gpd A D} {a b : A}
  (p : a = b) {a' : D a} {b': D b} (p' : transport D p a' = b')
  : DGpdHom (GpdHom_path p) a' b'
  := DHom_path p p'.

Instance reflexive_DHom {A} {D : A -> Type} `{IsD01Cat A D} {a : A}
  : Reflexive (DHom (Id a))
  := fun a' => DId a'.

Instance reflexive_DGpdHom {A} {D : A -> Type} `{IsD0Gpd A D} {a : A}
  : Reflexive (DGpdHom (Id a))
  := fun a' => DId a'.

(** A displayed 0-functor [F'] over a 0-functor [F] acts on displayed objects and 1-cells and satisfies no axioms. *)
Class IsD0Functor {A : Type} {B : Type}
  {DA : A -> Type} `{IsDGraph A DA} {DB : B -> Type} `{IsDGraph B DB}
  (F : A -> B) `{!Is0Functor F} (F' : forall (a : A), DA a -> DB (F a))
  := dfmap : forall {a b : A} {f : a $-> b} {a' : DA a} {b' : DA b},
              DHom f a' b' -> DHom (fmap F f) (F' a a') (F' b b').

Arguments dfmap {A B DA _ _ DB _ _} F {_} F' {_ _ _ _ _ _} f'.

Class IsD2Graph {A : Type} `{Is2Graph A}
  (D : A -> Type) `{!IsDGraph D}
  := isdgraph_hom :: forall {a b} {a'} {b'},
                      IsDGraph (fun (f:a $-> b) => DHom f a' b').

#[global] Typeclasses Transparent IsD2Graph.

Class IsD1Cat {A : Type} `{Is1Cat A}
  (D : A -> Type) `{!IsDGraph D, !IsD2Graph D, !IsD01Cat D} :=
{
  isd01cat_hom :: forall {a b : A} {a' : D a} {b' : D b},
                 IsD01Cat (fun f => DHom f a' b');
  isd0gpd_hom :: forall {a b : A} {a' : D a} {b' : D b},
                IsD0Gpd (fun f => DHom f a' b');
  isd0functor_postcomp :: forall {a b c : A} {g : b $-> c} {a' : D a}
                         {b' : D b} {c' : D c} (g' : DHom g b' c'),
                         @IsD0Functor _ _ (fun f => DHom f a' b')
                         _ _ (fun gf => DHom gf a' c')
                         _ _ (cat_postcomp a g) _ (dcat_postcomp g');
  isd0functor_precomp :: forall {a b c : A} {f : a $-> b} {a' : D a}
                        {b' : D b} {c' : D c} (f' : DHom f a' b'),
                        @IsD0Functor _ _ (fun g => DHom g b' c')
                        _ _ (fun gf => DHom gf a' c')
                        _ _ (cat_precomp c f) _ (dcat_precomp f');
  dcat_assoc : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
               {a' : D a} {b' : D b} {c' : D c} {d' : D d}
               (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
               DHom (cat_assoc f g h) ((h' $o' g') $o' f')
               (h' $o' (g' $o' f'));
  dcat_assoc_opp : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
               {a' : D a} {b' : D b} {c' : D c} {d' : D d}
               (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
               DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f'))
               ((h' $o' g') $o' f');
  dcat_idl : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
             (f' : DHom f a' b'), DHom (cat_idl f) (DId b' $o' f') f';
  dcat_idr : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
             (f' : DHom f a' b'), DHom (cat_idr f) (f' $o' DId a') f';
}.

Definition dcat_postwhisker {A : Type} {D : A -> Type} `{IsD1Cat A D}
  {a b c : A} {f g : a $-> b} {h : b $-> c} {p : f $== g}
  {a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
  (h' : DHom h b' c') (p' : DHom p f' g')
  : DHom (h $@L p) (h' $o' f') (h' $o' g')
  := dfmap (cat_postcomp a h) (dcat_postcomp h') p'.

Notation "h $@L' p" := (dcat_postwhisker h p).

Definition dcat_prewhisker {A : Type} {D : A -> Type} `{IsD1Cat A D}
  {a b c : A} {f : a $-> b} {g h : b $-> c} {p : g $== h}
  {a' : D a} {b' : D b} {c' : D c} {g' : DHom g b' c'} {h' : DHom h b' c'}
  (p' : DHom p g' h') (f' : DHom f a' b')
  : DHom (p $@R f) (g' $o' f') (h' $o' f')
  := dfmap (cat_precomp c f) (dcat_precomp f') p'.

Notation "p $@R' f" := (dcat_prewhisker p f).

Definition dcat_comp2 {A : Type} {D : A -> Type} `{IsD1Cat A D} {a b c : A}
  {f g : a $-> b} {h k : b $-> c} {p : f $== g} {q : h $== k}
  {a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
  {h' : DHom h b' c'} {k' : DHom k b' c'}
  (p' : DHom p f' g') (q' : DHom q h' k')
  : DHom (p $@@ q) (h' $o' f') (k' $o' g')
  :=  (k' $@L' p') $o' (q' $@R' f').

Notation "q $@@' p" := (dcat_comp2 q p).

(** Monomorphisms and epimorphisms. *)

Definition DMonic {A} {D : A -> Type} `{IsD1Cat A D} {b c : A}
  {f : b $-> c} {mon : Monic f} {b' : D b} {c' : D c} (f' : DHom f b' c')
  := forall (a : A) (g h : a $-> b) (p : f $o g $== f $o h) (a' : D a)
      (g' : DHom g a' b') (h' : DHom h a' b'),
      DGpdHom p (f' $o' g') (f' $o' h') -> DGpdHom (mon a g h p) g' h'.

Definition DEpic {A} {D : A -> Type} `{IsD1Cat A D} {a b : A}
  {f : a $-> b} {epi : Epic f} {a' : D a} {b' : D b} (f' : DHom f a' b')
  := forall (c : A) (g h : b $-> c) (p : g $o f $== h $o f) (c' : D c)
      (g' : DHom g b' c') (h' : DHom h b' c'),
      DGpdHom p (g' $o' f') (h' $o' f') -> DGpdHom (epi c g h p) g' h'.

Instance isgraph_total {A : Type} (D : A -> Type) `{IsDGraph A D}
  : IsGraph (sig D).A: Type
D: A -> Type
H: IsGraph A
H0: IsDGraph D
IsGraph {x : _ & D x}
Proof.A: Type
D: A -> Type
H: IsGraph A
H0: IsDGraph D
IsGraph {x : _ & D x}
  srapply Build_IsGraph.A: Type
D: A -> Type
H: IsGraph A
H0: IsDGraph D
{x : _ & D x} -> {x : _ & D x} -> Type
  intros [a a'] [b b'].A: Type
D: A -> Type
H: IsGraph A
H0: IsDGraph D
a: A
a': D a
b: A
b': D b
Type
  exact {f : a $-> b & DHom f a' b'}.
Defined.

Instance is01cat_total {A : Type} (D : A -> Type) `{IsD01Cat A D}
  : Is01Cat (sig D).A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
Is01Cat {x : _ & D x}
Proof.A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
Is01Cat {x : _ & D x}
  srapply Build_Is01Cat.A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
forall a : {x : _ & D x}, a $-> a
A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
forall a b c : {x : _ & D x},
(b $-> c) -> (a $-> b) -> a $-> c
  -A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
forall a : {x : _ & D x}, a $-> a intros [a a'].A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
a: A
a': D a
(a; a') $-> (a; a')
    exact (Id a; DId a').
  -A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
forall a b c : {x : _ & D x},
(b $-> c) -> (a $-> b) -> a $-> c intros [a a'] [b b'] [c c'] [g g'] [f f'].A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph D
H1: IsD01Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
g: b $-> c
g': DHom g b' c'
f: a $-> b
f': DHom f a' b'
(a; a') $-> (c; c')
    exact (g $o f; g' $o' f').
Defined.

Instance is0gpd_total {A : Type} (D : A -> Type) `{IsD0Gpd A D}
  : Is0Gpd (sig D).A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
IsDGraph0: IsDGraph D
IsD01Cat0: IsD01Cat D
H2: IsD0Gpd D
Is0Gpd {x : _ & D x}
Proof.A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
IsDGraph0: IsDGraph D
IsD01Cat0: IsD01Cat D
H2: IsD0Gpd D
Is0Gpd {x : _ & D x}
  srapply Build_Is0Gpd.A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
IsDGraph0: IsDGraph D
IsD01Cat0: IsD01Cat D
H2: IsD0Gpd D
forall a b : {x : _ & D x}, (a $-> b) -> b $-> a
  intros [a a'] [b b'] [f f'].A: Type
D: A -> Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
IsDGraph0: IsDGraph D
IsD01Cat0: IsD01Cat D
H2: IsD0Gpd D
a: A
a': D a
b: A
b': D b
f: a $-> b
f': DHom f a' b'
(b; b') $-> (a; a')
  exact (f^$; dgpd_rev f').
Defined.

Instance is0functor_total_pr1 {A : Type} (D : A -> Type) `{IsDGraph A D}
  : Is0Functor (pr1 : sig D -> A).A: Type
D: A -> Type
H: IsGraph A
H0: IsDGraph D
Is0Functor (pr1 : {x : _ & D x} -> A)
Proof.A: Type
D: A -> Type
H: IsGraph A
H0: IsDGraph D
Is0Functor (pr1 : {x : _ & D x} -> A)
  srapply Build_Is0Functor.A: Type
D: A -> Type
H: IsGraph A
H0: IsDGraph D
forall a b : {x : _ & D x}, (a $-> b) -> a.1 $-> b.1
  intros [a a'] [b b'] [f f'].A: Type
D: A -> Type
H: IsGraph A
H0: IsDGraph D
a: A
a': D a
b: A
b': D b
f: a $-> b
f': DHom f a' b'
(a; a').1 $-> (b; b').1
  exact f.
Defined.

Instance is2graph_total {A : Type} (D : A -> Type) `{IsD2Graph A D}
  : Is2Graph (sig D).A: Type
D: A -> Type
H: IsGraph A
H0: Is2Graph A
IsDGraph0: IsDGraph D
H1: IsD2Graph D
Is2Graph {x : _ & D x}
Proof.A: Type
D: A -> Type
H: IsGraph A
H0: Is2Graph A
IsDGraph0: IsDGraph D
H1: IsD2Graph D
Is2Graph {x : _ & D x}
  intros [a a'] [b b'].A: Type
D: A -> Type
H: IsGraph A
H0: Is2Graph A
IsDGraph0: IsDGraph D
H1: IsD2Graph D
a: A
a': D a
b: A
b': D b
IsGraph ((a; a') $-> (b; b'))
  srapply Build_IsGraph.A: Type
D: A -> Type
H: IsGraph A
H0: Is2Graph A
IsDGraph0: IsDGraph D
H1: IsD2Graph D
a: A
a': D a
b: A
b': D b
((a; a') $-> (b; b')) -> ((a; a') $-> (b; b')) -> Type
  intros [f f'] [g g'].A: Type
D: A -> Type
H: IsGraph A
H0: Is2Graph A
IsDGraph0: IsDGraph D
H1: IsD2Graph D
a: A
a': D a
b: A
b': D b
f: a $-> b
f': DHom f a' b'
g: a $-> b
g': DHom g a' b'
Type
  exact ({p : f $-> g & DHom p f' g'}).
Defined.

Instance is0functor_total {A : Type} (DA : A -> Type) `{IsD01Cat A DA}
  {B : Type} (DB : B -> Type) `{IsD01Cat B DB} (F : A -> B) `{!Is0Functor F}
  (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F'}
  : Is0Functor (functor_sigma F F').A: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
B: Type
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
F: A -> B
Is0Functor0: Is0Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
Is0Functor (functor_sigma F F')
Proof.A: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
B: Type
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
F: A -> B
Is0Functor0: Is0Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
Is0Functor (functor_sigma F F')
  srapply Build_Is0Functor.A: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
B: Type
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
F: A -> B
Is0Functor0: Is0Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
forall a b : {x : _ & DA x},
(a $-> b) ->
functor_sigma F F' a $-> functor_sigma F F' b
  intros [a a'] [b b'].A: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
B: Type
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
F: A -> B
Is0Functor0: Is0Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
a: A
a': DA a
b: A
b': DA b
((a; a') $-> (b; b')) ->
functor_sigma F F' (a; a') $->
functor_sigma F F' (b; b')
  intros [f f'].A: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
B: Type
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
F: A -> B
Is0Functor0: Is0Functor F
F': forall a : A, DA a -> DB (F a)
IsD0Functor0: IsD0Functor F F'
a: A
a': DA a
b: A
b': DA b
f: a $-> b
f': DHom f a' b'
functor_sigma F F' (a; a') $->
functor_sigma F F' (b; b')
  exact (fmap F f; dfmap F F' f').
Defined.

Instance is1cat_total {A : Type} (D : A -> Type) `{IsD1Cat A D}
  : Is1Cat (sig D).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
Is1Cat {x : _ & D x}
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
Is1Cat {x : _ & D x}
  srapply Build_Is1Cat.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c : {x : _ & D x}) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c : {x : _ & D x}) 
(f : a $-> b), Is0Functor (cat_precomp c f)
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c d : {x : _ & D x}) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f)
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c d : {x : _ & D x}) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b : {x : _ & D x}) 
(f : a $-> b), Id b $o f $== f
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b : {x : _ & D x}) 
(f : a $-> b), f $o Id a $== f
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c : {x : _ & D x}) (g : b $-> c),
Is0Functor (cat_postcomp a g) intros [a a'] [b b'] [c c'] [f f'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
f: b $-> c
f': DHom f b' c'
Is0Functor (cat_postcomp (a; a') (f; f'))
    apply Build_Is0Functor.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
f: b $-> c
f': DHom f b' c'
forall a0 b0 : (a; a') $-> (b; b'),
(a0 $-> b0) ->
cat_postcomp (a; a') (f; f') a0 $->
cat_postcomp (a; a') (f; f') b0
    intros [g g'] [h h'] [p p'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
f: b $-> c
f': DHom f b' c'
g: a $-> b
g': DHom g a' b'
h: a $-> b
h': DHom h a' b'
p: g $-> h
p': DHom p g' h'
cat_postcomp (a; a') (f; f') (g; g') $->
cat_postcomp (a; a') (f; f') (h; h')
    exact (f $@L p; f' $@L' p').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c : {x : _ & D x}) (f : a $-> b),
Is0Functor (cat_precomp c f) intros [a a'] [b b'] [c c'] [f f'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
f: a $-> b
f': DHom f a' b'
Is0Functor (cat_precomp (c; c') (f; f'))
    apply Build_Is0Functor.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
f: a $-> b
f': DHom f a' b'
forall a0 b0 : (b; b') $-> (c; c'),
(a0 $-> b0) ->
cat_precomp (c; c') (f; f') a0 $->
cat_precomp (c; c') (f; f') b0
    intros [g g'] [h h'] [p p'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
f: a $-> b
f': DHom f a' b'
g: b $-> c
g': DHom g b' c'
h: b $-> c
h': DHom h b' c'
p: g $-> h
p': DHom p g' h'
cat_precomp (c; c') (f; f') (g; g') $->
cat_precomp (c; c') (f; f') (h; h')
    exact (p $@R f; p' $@R' f').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c d : {x : _ & D x}) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f) intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
d: A
d': D d
f: a $-> b
f': DHom f a' b'
g: b $-> c
g': DHom g b' c'
h: c $-> d
h': DHom h c' d'
(h; h') $o (g; g') $o (f; f') $==
(h; h') $o ((g; g') $o (f; f'))
    exact (cat_assoc f g h; dcat_assoc f' g' h').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c d : {x : _ & D x}) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o (g $o f) $== h $o g $o f intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
d: A
d': D d
f: a $-> b
f': DHom f a' b'
g: b $-> c
g': DHom g b' c'
h: c $-> d
h': DHom h c' d'
(h; h') $o ((g; g') $o (f; f')) $==
(h; h') $o (g; g') $o (f; f')
    exact (cat_assoc_opp f g h; dcat_assoc_opp f' g' h').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b : {x : _ & D x}) (f : a $-> b),
Id b $o f $== f intros [a a'] [b b'] [f f'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
f: a $-> b
f': DHom f a' b'
Id (b; b') $o (f; f') $== (f; f')
    exact (cat_idl f; dcat_idl f').
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b : {x : _ & D x}) (f : a $-> b),
f $o Id a $== f intros [a a'] [b b'] [f f'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
f: a $-> b
f': DHom f a' b'
(f; f') $o Id (a; a') $== (f; f')
    exact (cat_idr f; dcat_idr f').
Defined.

Instance is1functor_pr1 {A : Type} {D : A -> Type} `{IsD1Cat A D}
  : Is1Functor (pr1 : sig D -> A).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
Is1Functor (pr1 : {x : _ & D x} -> A)
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
Is1Functor (pr1 : {x : _ & D x} -> A)
  srapply Build_Is1Functor.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b : {x : _ & D x}) (f g : a $-> b),
f $== g ->
fmap (pr1 : {x : _ & D x} -> A) f $==
fmap (pr1 : {x : _ & D x} -> A) g
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall a : {x : _ & D x},
fmap (pr1 : {x : _ & D x} -> A) (Id a) $== Id a.1
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c : {x : _ & D x}) 
(f : a $-> b) (g : b $-> c),
fmap (pr1 : {x : _ & D x} -> A) (g $o f) $==
fmap (pr1 : {x : _ & D x} -> A) g $o
fmap (pr1 : {x : _ & D x} -> A) f
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b : {x : _ & D x}) (f g : a $-> b),
f $== g ->
fmap (pr1 : {x : _ & D x} -> A) f $==
fmap (pr1 : {x : _ & D x} -> A) g intros [a a'] [b b'] [f f'] [g g'] [p p'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
f: a $-> b
f': DHom f a' b'
g: a $-> b
g': DHom g a' b'
p: f $-> g
p': DHom p f' g'
fmap (pr1 : {x : _ & D x} -> A) (f; f') $==
fmap (pr1 : {x : _ & D x} -> A) (g; g')
    exact p.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall a : {x : _ & D x},
fmap (pr1 : {x : _ & D x} -> A) (Id a) $== Id a.1 intros [a a'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
fmap (pr1 : {x : _ & D x} -> A) (Id (a; a')) $==
Id (a; a').1
    apply Id.
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
forall (a b c : {x : _ & D x}) (f : a $-> b)
(g : b $-> c),
fmap (pr1 : {x : _ & D x} -> A) (g $o f) $==
fmap (pr1 : {x : _ & D x} -> A) g $o
fmap (pr1 : {x : _ & D x} -> A) f intros [a a'] [b b'] [c c'] [f f'] [g g'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat D
a: A
a': D a
b: A
b': D b
c: A
c': D c
f: a $-> b
f': DHom f a' b'
g: b $-> c
g': DHom g b' c'
fmap (pr1 : {x : _ & D x} -> A) ((g; g') $o (f; f')) $==
fmap (pr1 : {x : _ & D x} -> A) (g; g') $o
fmap (pr1 : {x : _ & D x} -> A) (f; f')
    apply Id.
Defined.

Class IsD1Cat_Strong {A : Type} `{Is1Cat_Strong A}
  (D : A -> Type)
  `{!IsDGraph D, !IsD2Graph D, !IsD01Cat D} :=
{
  isd01cat_hom_strong :: forall {a b : A} {a' : D a} {b' : D b},
                        IsD01Cat (fun f => DHom f a' b');
  isd0gpd_hom_strong :: forall {a b : A} {a' : D a} {b' : D b},
                       IsD0Gpd (fun f => DHom f a' b');
  isd0functor_postcomp_strong :: forall {a b c : A} {g : b $-> c} {a' : D a}
                                {b' : D b} {c' : D c} (g' : DHom g b' c'),
                                @IsD0Functor _ _ (fun f => DHom f a' b')
                                _ _ (fun gf => DHom gf a' c')
                                _ _ (cat_postcomp a g) _ (dcat_postcomp g');
  isd0functor_precomp_strong :: forall {a b c : A} {f : a $-> b} {a' : D a}
                                {b' : D b} {c' : D c} (f' : DHom f a' b'),
                                @IsD0Functor _ _ (fun g => DHom g b' c')
                                _ _ (fun gf => DHom gf a' c')
                                _ _ (cat_precomp c f) _ (dcat_precomp f');
  dcat_assoc_strong : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
                      {a' : D a} {b' : D b} {c' : D c} {d' : D d}
                      (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
                      (transport (fun k => DHom k a' d') (cat_assoc_strong f g h)
                      ((h' $o' g') $o' f')) = h' $o' (g' $o' f');
  dcat_assoc_opp_strong : forall {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
                      {a' : D a} {b' : D b} {c' : D c} {d' : D d}
                      (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
                      (transport (fun k => DHom k a' d') (cat_assoc_opp_strong f g h)
                      (h' $o' (g' $o' f'))) = (h' $o' g') $o' f';
  dcat_idl_strong : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
                    (f' : DHom f a' b'),
                    (transport (fun k => DHom k a' b') (cat_idl_strong f)
                    (DId b' $o' f')) = f';
  dcat_idr_strong : forall {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
                    (f' : DHom f a' b'),
                    (transport (fun k => DHom k a' b') (cat_idr_strong f)
                    (f' $o' DId a')) = f';
}.

(* If in the future we make a [Build_Is1Cat_Strong'] that lets the user omit the second proof of associativity, this shows how it can be recovered from the original proof:
Definition dcat_assoc_opp_strong {A : Type} {D : A -> Type} `{IsD1Cat_Strong A D}
  {a b c d : A}  {f : a $-> b} {g : b $-> c} {h : c $-> d}
  {a' : D a} {b' : D b} {c' : D c} {d' : D d}
  (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d')
  : (transport (fun k => DHom k a' d') (cat_assoc_opp_strong f g h)
    (h' $o' (g' $o' f'))) = (h' $o' g') $o' f'.
Proof.
  exact (moveR_transport_V (fun k => DHom k a' d') (cat_assoc_strong f g h) _ _).
  exact ((dcat_assoc_strong f' g' h')^).
Defined.
*)

Instance isd1cat_isd1catstrong {A : Type} (D : A -> Type)
  `{IsD1Cat_Strong A D} : IsD1Cat D.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
IsD1Cat D
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
IsD1Cat D
  srapply Build_IsD1Cat.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b c d : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d) (a' : D a) (b' : D b) (c' : D c)
(d' : D d) (f' : DHom f a' b') (g' : DHom g b' c')
(h' : DHom h c' d'),
DHom (cat_assoc f g h) (h' $o' g' $o' f')
  (h' $o' (g' $o' f'))
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b c d : A) (f : a $-> b) 
(g : b $-> c) (h : c $-> d) 
(a' : D a) (b' : D b) (c' : D c) 
(d' : D d) (f' : DHom f a' b') 
(g' : DHom g b' c') (h' : DHom h c' d'),
DHom (cat_assoc_opp f g h) 
  (h' $o' (g' $o' f')) 
  (h' $o' g' $o' f')
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b : A) (f : a $-> b) 
(a' : D a) (b' : D b) (f' : DHom f a' b'),
DHom (cat_idl f) (DId b' $o' f') f'
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b : A) (f : a $-> b) 
(a' : D a) (b' : D b) (f' : DHom f a' b'),
DHom (cat_idr f) (f' $o' DId a') f'
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b c d : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d) (a' : D a) (b' : D b) (c' : D c)
(d' : D d) (f' : DHom f a' b') (g' : DHom g b' c')
(h' : DHom h c' d'),
DHom (cat_assoc f g h) (h' $o' g' $o' f')
  (h' $o' (g' $o' f')) intros a b c d f g h a' b' c' d' f' g' h'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
a, b, c, d: A
f: a $-> b
g: b $-> c
h: c $-> d
a': D a
b': D b
c': D c
d': D d
f': DHom f a' b'
g': DHom g b' c'
h': DHom h c' d'
DHom (cat_assoc f g h) (h' $o' g' $o' f')
  (h' $o' (g' $o' f'))
    exact (DHom_path (cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b c d : A) (f : a $-> b) (g : b $-> c)
(h : c $-> d) (a' : D a) (b' : D b) (c' : D c)
(d' : D d) (f' : DHom f a' b') (g' : DHom g b' c')
(h' : DHom h c' d'),
DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f'))
  (h' $o' g' $o' f') intros a b c d f g h a' b' c' d' f' g' h'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
a, b, c, d: A
f: a $-> b
g: b $-> c
h: c $-> d
a': D a
b': D b
c': D c
d': D d
f': DHom f a' b'
g': DHom g b' c'
h': DHom h c' d'
DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f'))
  (h' $o' g' $o' f')
    exact (DHom_path (cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b : A) (f : a $-> b) (a' : D a) (b' : D b)
(f' : DHom f a' b'),
DHom (cat_idl f) (DId b' $o' f') f' intros a b f a' b' f'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
a, b: A
f: a $-> b
a': D a
b': D b
f': DHom f a' b'
DHom (cat_idl f) (DId b' $o' f') f'
    exact (DHom_path (cat_idl_strong f) (dcat_idl_strong f')).
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b : A) (f : a $-> b) (a' : D a) (b' : D b)
(f' : DHom f a' b'),
DHom (cat_idr f) (f' $o' DId a') f' intros a b f a' b' f'.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
a, b: A
f: a $-> b
a': D a
b': D b
f': DHom f a' b'
DHom (cat_idr f) (f' $o' DId a') f'
    exact (DHom_path (cat_idr_strong f) (dcat_idr_strong f')).
Defined.

Instance is1catstrong_total {A : Type}
  (D : A -> Type) `{IsD1Cat_Strong A D}
  : Is1Cat_Strong (sig D).A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
Is1Cat_Strong {x : _ & D x}
Proof.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
Is1Cat_Strong {x : _ & D x}
  srapply Build_Is1Cat_Strong.A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b c d : {x : _ & D x}) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f = h $o (g $o f)
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b c d : {x : _ & D x}) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) = h $o g $o f
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b : {x : _ & D x}) 
(f : a $-> b), Id b $o f = f
A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b : {x : _ & D x}) 
(f : a $-> b), f $o Id a = f
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b c d : {x : _ & D x}) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f = h $o (g $o f) intros aa' bb' cc' dd' [f f'] [g g'] [h h'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
aa', bb', cc', dd': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
g: bb'.1 $-> cc'.1
g': DHom g bb'.2 cc'.2
h: cc'.1 $-> dd'.1
h': DHom h cc'.2 dd'.2
(h; h') $o (g; g') $o (f; f') =
(h; h') $o ((g; g') $o (f; f'))
    exact (path_sigma' _
            (cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b c d : {x : _ & D x}) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o (g $o f) = h $o g $o f intros aa' bb' cc' dd' [f f'] [g g'] [h h'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
aa', bb', cc', dd': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
g: bb'.1 $-> cc'.1
g': DHom g bb'.2 cc'.2
h: cc'.1 $-> dd'.1
h': DHom h cc'.2 dd'.2
(h; h') $o ((g; g') $o (f; f')) =
(h; h') $o (g; g') $o (f; f')
    exact (path_sigma' _
            (cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b : {x : _ & D x}) (f : a $-> b),
Id b $o f = f intros aa' bb' [f f'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
Id bb' $o (f; f') = (f; f')
    exact (path_sigma' _ (cat_idl_strong f) (dcat_idl_strong f')).
  -A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
forall (a b : {x : _ & D x}) (f : a $-> b),
f $o Id a = f intros aa' bb' [f f'].A: Type
D: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
IsDGraph0: IsDGraph D
IsD2Graph0: IsD2Graph D
IsD01Cat0: IsD01Cat D
H0: IsD1Cat_Strong D
aa', bb': {x : _ & D x}
f: aa'.1 $-> bb'.1
f': DHom f aa'.2 bb'.2
(f; f') $o Id aa' = (f; f')
    exact (path_sigma' _ (cat_idr_strong f) (dcat_idr_strong f')).
Defined.

Class IsD1Functor
  {A B : Type} {DA : A -> Type} `{IsD1Cat A DA} {DB : B -> Type} `{IsD1Cat B DB}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
  (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F'} :=
{
  dfmap2 : forall {a b : A} {f g : a $-> b} {p : f $== g} {a' : DA a}
            {b' : DA b} (f' : DHom f a' b') (g' : DHom g a' b'),
            DHom p f' g' -> DHom (fmap2 F p) (dfmap F F' f') (dfmap F F' g');
  dfmap_id : forall {a : A} (a' : DA a),
              DHom (fmap_id F a) (dfmap F F' (DId a')) (DId (F' a a'));
  dfmap_comp : forall {a b c : A} {f : a $-> b} {g : b $-> c} {a' : DA a}
                {b' : DA b} {c' : DA c} (f' : DHom f a' b') (g' : DHom g b' c'),
                DHom (fmap_comp F f g) (dfmap F F' (g' $o' f'))
                (dfmap F F' g' $o' dfmap F F' f');
}.

Arguments dfmap2 {A B DA _ _ _ _ _ _ _ _ DB _ _ _ _ _ _ _ _}
  F {_ _} F' {_ _ a b f g p a' b' f' g'} p'.
Arguments dfmap_id {A B DA _ _ _ _ _ _ _ _ DB _ _ _ _ _ _ _ _}
  F {_ _} F' {_ _ a} a'.
Arguments dfmap_comp {A B DA _ _ _ _ _ _ _ _ DB _ _ _ _ _ _ _ _}
  F {_ _} F' {_ _ a b c f g a' b' c'} f' g'.

Instance is1functor_total {A B : Type} (DA : A -> Type) (DB : B -> Type)
  (F : A -> B) (F' : forall (a : A), DA a -> DB (F a)) `{IsD1Functor A B DA DB F F'}
  : Is1Functor (functor_sigma F F').A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
Is1Functor (functor_sigma F F')
Proof.A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
Is1Functor (functor_sigma F F')
  srapply Build_Is1Functor.A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
forall (a b : {x : _ & DA x}) (f g : a $-> b),
f $== g ->
fmap (functor_sigma F F') f $==
fmap (functor_sigma F F') g
A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
forall a : {x : _ & DA x},
fmap (functor_sigma F F') (Id a) $==
Id (functor_sigma F F' a)
A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
forall (a b c : {x : _ & DA x}) 
(f : a $-> b) (g : b $-> c),
fmap (functor_sigma F F') (g $o f) $==
fmap (functor_sigma F F') g $o
fmap (functor_sigma F F') f
  -A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
forall (a b : {x : _ & DA x}) (f g : a $-> b),
f $== g ->
fmap (functor_sigma F F') f $==
fmap (functor_sigma F F') g intros [a a'] [b b'] [f f'] [g g'] [p p'].A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
a: A
a': DA a
b: A
b': DA b
f: a $-> b
f': DHom f a' b'
g: a $-> b
g': DHom g a' b'
p: f $-> g
p': DHom p f' g'
fmap (functor_sigma F F') (f; f') $==
fmap (functor_sigma F F') (g; g')
    exists (fmap2 F p).A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
a: A
a': DA a
b: A
b': DA b
f: a $-> b
f': DHom f a' b'
g: a $-> b
g': DHom g a' b'
p: f $-> g
p': DHom p f' g'
DHom (fmap2 F p) (fmap (functor_sigma F F') (f; f')).2
  (fmap (functor_sigma F F') (g; g')).2
    exact (dfmap2 F F' p').
  -A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
forall a : {x : _ & DA x},
fmap (functor_sigma F F') (Id a) $==
Id (functor_sigma F F' a) intros [a a'].A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
a: A
a': DA a
fmap (functor_sigma F F') (Id (a; a')) $==
Id (functor_sigma F F' (a; a'))
    exact (fmap_id F a; dfmap_id F F' a').
  -A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
forall (a b c : {x : _ & DA x}) (f : a $-> b)
(g : b $-> c),
fmap (functor_sigma F F') (g $o f) $==
fmap (functor_sigma F F') g $o
fmap (functor_sigma F F') f intros [a a'] [b b'] [c c'] [f f'] [g g'].A, B: Type
DA: A -> Type
DB: B -> Type
F: A -> B
F': forall a : A, DA a -> DB (F a)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsD0Functor0: IsD0Functor F F'
H3: IsD1Functor F F'
a: A
a': DA a
b: A
b': DA b
c: A
c': DA c
f: a $-> b
f': DHom f a' b'
g: b $-> c
g': DHom g b' c'
fmap (functor_sigma F F') ((g; g') $o (f; f')) $==
fmap (functor_sigma F F') (g; g') $o
fmap (functor_sigma F F') (f; f')
    exact (fmap_comp F f g; dfmap_comp F F' f' g').
Defined.

Section IdentityFunctor.
  #[export] Instance isd0functor_idmap {A : Type} `{Is01Cat A}
    (DA : A -> Type) `{!IsDGraph DA, !IsD01Cat DA}
    : IsD0Functor (idmap) (fun a a' => a').A: Type
H: IsGraph A
H0: Is01Cat A
DA: A -> Type
IsDGraph0: IsDGraph DA
IsD01Cat0: IsD01Cat DA
IsD0Functor idmap (fun a : A => idmap)
  Proof.A: Type
H: IsGraph A
H0: Is01Cat A
DA: A -> Type
IsDGraph0: IsDGraph DA
IsD01Cat0: IsD01Cat DA
IsD0Functor idmap (fun a : A => idmap)
    intros a b f a' b' f'.A: Type
H: IsGraph A
H0: Is01Cat A
DA: A -> Type
IsDGraph0: IsDGraph DA
IsD01Cat0: IsD01Cat DA
a, b: A
f: a $-> b
a': DA a
b': DA b
f': DHom f a' b'
DHom (fmap idmap f) a' b'
    assumption.
  Defined.

  #[export] Instance isd1functor_idmap {A : Type} (DA : A -> Type)
    `{IsD1Cat A DA}
    : IsD1Functor (idmap) (fun a a' => a').A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsD1Functor idmap (fun a : A => idmap)
  Proof.A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsD1Functor idmap (fun a : A => idmap)
    apply Build_IsD1Functor.A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
forall (a b : A) (f g : a $-> b) (p : f $== g)
(a' : DA a) (b' : DA b) (f' : DHom f a' b')
(g' : DHom g a' b'),
DHom p f' g' ->
DHom (fmap2 idmap p)
  (dfmap idmap (fun a0 : A => idmap) f')
  (dfmap idmap (fun a0 : A => idmap) g')
A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
forall (a : A) (a' : DA a),
DHom (fmap_id idmap a)
  (dfmap idmap (fun a0 : A => idmap) (DId a'))
  (DId a')
A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
forall (a b c : A) (f : a $-> b) 
(g : b $-> c) (a' : DA a) 
(b' : DA b) (c' : DA c) 
(f' : DHom f a' b') (g' : DHom g b' c'),
DHom (fmap_comp idmap f g)
  (dfmap idmap (fun a0 : A => idmap) (g' $o' f'))
  (dfmap idmap (fun a0 : A => idmap) g' $o'
   dfmap idmap (fun a0 : A => idmap) f')
    -A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
forall (a b : A) (f g : a $-> b) (p : f $== g)
(a' : DA a) (b' : DA b) (f' : DHom f a' b')
(g' : DHom g a' b'),
DHom p f' g' ->
DHom (fmap2 idmap p)
  (dfmap idmap (fun a0 : A => idmap) f')
  (dfmap idmap (fun a0 : A => idmap) g') intros a b f g p a' b' f' g' p'.A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
a, b: A
f, g: a $-> b
p: f $== g
a': DA a
b': DA b
f': DHom f a' b'
g': DHom g a' b'
p': DHom p f' g'
DHom (fmap2 idmap p)
  (dfmap idmap (fun a : A => idmap) f')
  (dfmap idmap (fun a : A => idmap) g')
      assumption.
    -A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
forall (a : A) (a' : DA a),
DHom (fmap_id idmap a)
  (dfmap idmap (fun a0 : A => idmap) (DId a'))
  (DId a') intros a a'.A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
a: A
a': DA a
DHom (fmap_id idmap a)
  (dfmap idmap (fun a : A => idmap) (DId a')) (DId a')
      apply DId.
    -A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
forall (a b c : A) (f : a $-> b) (g : b $-> c)
(a' : DA a) (b' : DA b) (c' : DA c)
(f' : DHom f a' b') (g' : DHom g b' c'),
DHom (fmap_comp idmap f g)
  (dfmap idmap (fun a0 : A => idmap) (g' $o' f'))
  (dfmap idmap (fun a0 : A => idmap) g' $o'
   dfmap idmap (fun a0 : A => idmap) f') intros a b c f g a' b' c' f' g'.A: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
a, b, c: A
f: a $-> b
g: b $-> c
a': DA a
b': DA b
c': DA c
f': DHom f a' b'
g': DHom g b' c'
DHom (fmap_comp idmap f g)
  (dfmap idmap (fun a : A => idmap) (g' $o' f'))
  (dfmap idmap (fun a : A => idmap) g' $o'
   dfmap idmap (fun a : A => idmap) f')
      apply DId.
  Defined.
End IdentityFunctor.

Section ConstantFunctor.
  #[export] Instance isd0functor_const {A : Type} `{IsGraph A}
    {B : Type} `{Is01Cat B} (DA : A -> Type) `{!IsDGraph DA}
    (DB : B -> Type) `{!IsDGraph DB, !IsD01Cat DB} (x : B) (x' : DB x)
    : IsD0Functor (fun _ : A => x) (fun _ _ => x').A: Type
H: IsGraph A
B: Type
H0: IsGraph B
H1: Is01Cat B
DA: A -> Type
IsDGraph0: IsDGraph DA
DB: B -> Type
IsDGraph1: IsDGraph DB
IsD01Cat0: IsD01Cat DB
x: B
x': DB x
IsD0Functor (fun _ : A => x)
  (fun (a : A) (_ : DA a) => x')
  Proof.A: Type
H: IsGraph A
B: Type
H0: IsGraph B
H1: Is01Cat B
DA: A -> Type
IsDGraph0: IsDGraph DA
DB: B -> Type
IsDGraph1: IsDGraph DB
IsD01Cat0: IsD01Cat DB
x: B
x': DB x
IsD0Functor (fun _ : A => x)
  (fun (a : A) (_ : DA a) => x')
    intros a b f a' b' f'.A: Type
H: IsGraph A
B: Type
H0: IsGraph B
H1: Is01Cat B
DA: A -> Type
IsDGraph0: IsDGraph DA
DB: B -> Type
IsDGraph1: IsDGraph DB
IsD01Cat0: IsD01Cat DB
x: B
x': DB x
a, b: A
f: a $-> b
a': DA a
b': DA b
f': DHom f a' b'
DHom (fmap (fun _ : A => x) f) x' x'
    apply DId.
  Defined.

  #[export] Instance isd1functor_const {A : Type} {B : Type}
    (DA : A -> Type)
    `{IsD1Cat A DA}
    (DB : B -> Type)
    `{IsD1Cat B DB}
    (x : B) (x' : DB x)
    : IsD1Functor (fun _ => x) (fun _ _ => x').A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
IsD1Functor (fun _ : B => x)
  (fun (a : B) (_ : DB a) => x')
  Proof.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
IsD1Functor (fun _ : B => x)
  (fun (a : B) (_ : DB a) => x')
    snapply Build_IsD1Functor.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
forall (a b : B) (f g : a $-> b) (p : f $== g)
(a' : DB a) (b' : DB b) (f' : DHom f a' b')
(g' : DHom g a' b'),
DHom p f' g' ->
DHom (fmap2 (fun _ : B => x) p)
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') f')
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') g')
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
forall (a : B) (a' : DB a),
DHom (fmap_id (fun _ : B => x) a)
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') 
     (DId a'))
  (DId ((fun (a0 : B) (_ : DB a0) => x') a a'))
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
forall (a b c : B) (f : a $-> b) 
(g : b $-> c) (a' : DB a) 
(b' : DB b) (c' : DB c) 
(f' : DHom f a' b') (g' : DHom g b' c'),
DHom (fmap_comp (fun _ : B => x) f g)
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') 
     (g' $o' f'))
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') g' $o'
   dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') f')
    -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
forall (a b : B) (f g : a $-> b) (p : f $== g)
(a' : DB a) (b' : DB b) (f' : DHom f a' b')
(g' : DHom g a' b'),
DHom p f' g' ->
DHom (fmap2 (fun _ : B => x) p)
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') f')
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') g') intros a b f g p a' b' f' g' p'.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
a, b: B
f, g: a $-> b
p: f $== g
a': DB a
b': DB b
f': DHom f a' b'
g': DHom g a' b'
p': DHom p f' g'
DHom (fmap2 (fun _ : B => x) p)
  (dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') f')
  (dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') g')
      apply DId.
    -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
forall (a : B) (a' : DB a),
DHom (fmap_id (fun _ : B => x) a)
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') (DId a'))
  (DId ((fun (a0 : B) (_ : DB a0) => x') a a')) intros a a'.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
a: B
a': DB a
DHom (fmap_id (fun _ : B => x) a)
  (dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') (DId a'))
  (DId ((fun (a : B) (_ : DB a) => x') a a'))
      apply DId.
    -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
forall (a b c : B) (f : a $-> b) (g : b $-> c)
(a' : DB a) (b' : DB b) (c' : DB c)
(f' : DHom f a' b') (g' : DHom g b' c'),
DHom (fmap_comp (fun _ : B => x) f g)
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') (g' $o' f'))
  (dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') g' $o'
   dfmap (fun _ : B => x)
     (fun (a0 : B) (_ : DB a0) => x') f') intros a b c f g a' b' c' f' g'.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
a, b, c: B
f: a $-> b
g: b $-> c
a': DB a
b': DB b
c': DB c
f': DHom f a' b'
g': DHom g b' c'
DHom (fmap_comp (fun _ : B => x) f g)
  (dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') (g' $o' f'))
  (dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') g' $o'
   dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') f')
      apply dgpd_rev.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
x: B
x': DB x
a, b, c: B
f: a $-> b
g: b $-> c
a': DB a
b': DB b
c': DB c
f': DHom f a' b'
g': DHom g b' c'
DHom (cat_idl (Id x))
  (dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') g' $o'
   dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') f')
  (dfmap (fun _ : B => x)
     (fun (a : B) (_ : DB a) => x') (g' $o' f'))
      apply dcat_idl.
  Defined.
End ConstantFunctor.

Section CompositeFunctor.
  Context {A B C : Type} {DA : A -> Type} {DB : B -> Type} {DC : C -> Type}
    (F : A -> B) (G : B -> C)
    (F' : forall (a : A), DA a -> DB (F a))
    (G' : forall (b : B), DB b -> DC (G b)).

  #[export] Instance isd0functor_compose
    `{IsDGraph A DA} `{IsDGraph B DB} `{IsDGraph C DC}
    `{!Is0Functor F} `{!Is0Functor G}
    `{!IsD0Functor F F'} `{!IsD0Functor G G'}
    : IsD0Functor (G o F) (fun a a' => (G' (F a) o (F' a)) a').A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
H: IsGraph A
H0: IsDGraph DA
H1: IsGraph B
H2: IsDGraph DB
H3: IsGraph C
H4: IsDGraph DC
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
IsD0Functor0: IsD0Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD0Functor (G o F)
  (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
  Proof.A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
H: IsGraph A
H0: IsDGraph DA
H1: IsGraph B
H2: IsDGraph DB
H3: IsGraph C
H4: IsDGraph DC
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
IsD0Functor0: IsD0Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD0Functor (G o F)
  (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
    intros a b f a' b' f'.A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
H: IsGraph A
H0: IsDGraph DA
H1: IsGraph B
H2: IsDGraph DB
H3: IsGraph C
H4: IsDGraph DC
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
IsD0Functor0: IsD0Functor F F'
IsD0Functor1: IsD0Functor G G'
a, b: A
f: a $-> b
a': DA a
b': DA b
f': DHom f a' b'
DHom (fmap (G o F) f) (G' (F a) (F' a a'))
  (G' (F b) (F' b b'))
    exact (dfmap G G' (dfmap F F' f')).
  Defined.

  #[export] Instance isd1functor_compose
    `{IsD1Cat A DA} `{IsD1Cat B DB} `{IsD1Cat C DC}
    `{!Is0Functor F, !Is1Functor F} `{!Is0Functor G, !Is1Functor G}
    `{!IsD0Functor F F', !IsD1Functor F F'}
    `{!IsD0Functor G G', !IsD1Functor G G'}
    : IsD1Functor (G o F) (fun a a' => (G' (F a) o (F' a)) a').A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
IsD1Functor (G o F)
  (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
  Proof.A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
IsD1Functor (G o F)
  (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
    snapply Build_IsD1Functor.A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
forall (a b : A) (f g : a $-> b) (p : f $== g)
(a' : DA a) (b' : DA b) (f' : DHom f a' b')
(g' : DHom g a' b'),
DHom p f' g' ->
DHom (fmap2 (G o F) p)
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) f')
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) g')
A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
forall (a : A) (a' : DA a),
DHom (fmap_id (G o F) a)
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) 
     (DId a'))
  (DId
     ((fun (a0 : A) (a'0 : DA a0) =>
       (G' (F a0) o F' a0) a'0) a a'))
A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
forall (a b c : A) (f : a $-> b) 
(g : b $-> c) (a' : DA a) 
(b' : DA b) (c' : DA c) 
(f' : DHom f a' b') (g' : DHom g b' c'),
DHom (fmap_comp (G o F) f g)
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) 
     (g' $o' f'))
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) g' $o'
   dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) f')
    -A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
forall (a b : A) (f g : a $-> b) (p : f $== g)
(a' : DA a) (b' : DA b) (f' : DHom f a' b')
(g' : DHom g a' b'),
DHom p f' g' ->
DHom (fmap2 (G o F) p)
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) f')
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) g') intros a b f g p a' b' f' g' p'.A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
a, b: A
f, g: a $-> b
p: f $== g
a': DA a
b': DA b
f': DHom f a' b'
g': DHom g a' b'
p': DHom p f' g'
DHom (fmap2 (G o F) p)
  (dfmap (fun x : A => G (F x))
     (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
     f')
  (dfmap (fun x : A => G (F x))
     (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
     g')
      exact (dfmap2 _ _ (dfmap2 F F' p')).
    -A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
forall (a : A) (a' : DA a),
DHom (fmap_id (G o F) a)
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) (DId a'))
  (DId
     ((fun (a0 : A) (a'0 : DA a0) =>
       (G' (F a0) o F' a0) a'0) a a')) intros a a'.A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
a: A
a': DA a
DHom (fmap_id (G o F) a)
  (dfmap (fun x : A => G (F x))
     (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
     (DId a'))
  (DId
     ((fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
        a a'))
      exact (dfmap2 _ _ (dfmap_id F F' a') $@' dfmap_id G G' _).
    -A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
forall (a b c : A) (f : a $-> b) (g : b $-> c)
(a' : DA a) (b' : DA b) (c' : DA c)
(f' : DHom f a' b') (g' : DHom g b' c'),
DHom (fmap_comp (G o F) f g)
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) (g' $o' f'))
  (dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) g' $o'
   dfmap (fun x : A => G (F x))
     (fun (a0 : A) (a'0 : DA a0) =>
      (G' (F a0) o F' a0) a'0) f') intros a b c f g a' b' c' f' g'.A, B, C: Type
DA: A -> Type
DB: B -> Type
DC: C -> Type
F: A -> B
G: B -> C
F': forall a : A, DA a -> DB (F a)
G': forall b : B, DB b -> DC (G b)
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H3: Is1Cat C
IsDGraph2: IsDGraph DC
IsD2Graph2: IsD2Graph DC
IsD01Cat2: IsD01Cat DC
H4: IsD1Cat DC
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor1: Is1Functor G
IsD0Functor0: IsD0Functor F F'
IsD1Functor0: IsD1Functor F F'
IsD0Functor1: IsD0Functor G G'
IsD1Functor1: IsD1Functor G G'
a, b, c: A
f: a $-> b
g: b $-> c
a': DA a
b': DA b
c': DA c
f': DHom f a' b'
g': DHom g b' c'
DHom (fmap_comp (G o F) f g)
  (dfmap (fun x : A => G (F x))
     (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
     (g' $o' f'))
  (dfmap (fun x : A => G (F x))
     (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
     g' $o'
   dfmap (fun x : A => G (F x))
     (fun (a : A) (a' : DA a) => (G' (F a) o F' a) a')
     f')
      exact (dfmap2 _ _ (dfmap_comp F F' f' g') $@' dfmap_comp G G' _ _).
  Defined.
End CompositeFunctor.

Local Definition pointwise_prod {A B : Type} (DA : A -> Type) (DB : B -> Type)
  (x : A * B) := DA (fst x) * DB (snd x).

Instance isdgraph_prod {A B : Type} (DA : A -> Type) `{IsDGraph A DA}
  (DB : B -> Type) `{IsDGraph B DB}
  : IsDGraph (pointwise_prod DA DB).A, B: Type
DA: A -> Type
H: IsGraph A
H0: IsDGraph DA
DB: B -> Type
H1: IsGraph B
H2: IsDGraph DB
IsDGraph (pointwise_prod DA DB)
Proof.A, B: Type
DA: A -> Type
H: IsGraph A
H0: IsDGraph DA
DB: B -> Type
H1: IsGraph B
H2: IsDGraph DB
IsDGraph (pointwise_prod DA DB)
  intros [a1 b1] [a2 b2] [f g] [a1' b1'] [a2' b2'].A, B: Type
DA: A -> Type
H: IsGraph A
H0: IsDGraph DA
DB: B -> Type
H1: IsGraph B
H2: IsDGraph DB
a1: A
b1: B
a2: A
b2: B
f: fst (a1, b1) $-> fst (a2, b2)
g: snd (a1, b1) $-> snd (a2, b2)
a1': DA (fst (a1, b1))
b1': DB (snd (a1, b1))
a2': DA (fst (a2, b2))
b2': DB (snd (a2, b2))
Type
  exact (DHom f a1' a2' * DHom g b1' b2').
Defined.

Instance isd01cat_prod {A B : Type} (DA : A -> Type) `{IsD01Cat A DA}
  (DB : B -> Type) `{IsD01Cat B DB}
  : IsD01Cat (pointwise_prod DA DB).A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
IsD01Cat (pointwise_prod DA DB)
Proof.A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
IsD01Cat (pointwise_prod DA DB)
  srapply Build_IsD01Cat.A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
forall (a : A * B) (a' : pointwise_prod DA DB a),
DHom (Id a) a' a'
A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
forall (a b c : A * B) 
(g : b $-> c) (f : a $-> b)
(a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c),
DHom g b' c' -> DHom f a' b' -> DHom (g $o f) a' c'
  -A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
forall (a : A * B) (a' : pointwise_prod DA DB a),
DHom (Id a) a' a' intros [a b] [a' b'].A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
a: A
b: B
a': DA (fst (a, b))
b': DB (snd (a, b))
DHom (Id (a, b)) (a', b') (a', b')
    exact (DId a', DId b').
  -A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
forall (a b c : A * B) 
(g : b $-> c) (f : a $-> b)
(a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c),
DHom g b' c' -> DHom f a' b' -> DHom (g $o f) a' c' intros [a1 b1] [a2 b2] [a3 b3] [f2 g2] [f1 g1] [a1' b1'] [a2' b2'] [a3' b3'].A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
a1: A
b1: B
a2: A
b2: B
a3: A
b3: B
f2: fst (a2, b2) $-> fst (a3, b3)
g2: snd (a2, b2) $-> snd (a3, b3)
f1: fst (a1, b1) $-> fst (a2, b2)
g1: snd (a1, b1) $-> snd (a2, b2)
a1': DA (fst (a1, b1))
b1': DB (snd (a1, b1))
a2': DA (fst (a2, b2))
b2': DB (snd (a2, b2))
a3': DA (fst (a3, b3))
b3': DB (snd (a3, b3))
DHom (f2, g2) (a2', b2') (a3', b3') ->
DHom (f1, g1) (a1', b1') (a2', b2') ->
DHom ((f2, g2) $o (f1, g1)) (a1', b1') (a3', b3')
    intros [f2' g2'] [f1' g1'].A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
IsDGraph0: IsDGraph DA
H1: IsD01Cat DA
DB: B -> Type
H2: IsGraph B
H3: Is01Cat B
IsDGraph1: IsDGraph DB
H4: IsD01Cat DB
a1: A
b1: B
a2: A
b2: B
a3: A
b3: B
f2: fst (a2, b2) $-> fst (a3, b3)
g2: snd (a2, b2) $-> snd (a3, b3)
f1: fst (a1, b1) $-> fst (a2, b2)
g1: snd (a1, b1) $-> snd (a2, b2)
a1': DA (fst (a1, b1))
b1': DB (snd (a1, b1))
a2': DA (fst (a2, b2))
b2': DB (snd (a2, b2))
a3': DA (fst (a3, b3))
b3': DB (snd (a3, b3))
f2': DHom f2 a2' a3'
g2': DHom g2 b2' b3'
f1': DHom f1 a1' a2'
g1': DHom g1 b1' b2'
DHom ((f2, g2) $o (f1, g1)) (a1', b1') (a3', b3')
    exact (f2' $o' f1', g2' $o' g1').
Defined.

Instance isd0gpd_prod {A B : Type} (DA : A -> Type) `{IsD0Gpd A DA}
  (DB : B -> Type) `{IsD0Gpd B DB}
  : IsD0Gpd (pointwise_prod DA DB).A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
IsDGraph0: IsDGraph DA
IsD01Cat0: IsD01Cat DA
H2: IsD0Gpd DA
DB: B -> Type
H3: IsGraph B
H4: Is01Cat B
H5: Is0Gpd B
IsDGraph1: IsDGraph DB
IsD01Cat1: IsD01Cat DB
H6: IsD0Gpd DB
IsD0Gpd (pointwise_prod DA DB)
Proof.A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
IsDGraph0: IsDGraph DA
IsD01Cat0: IsD01Cat DA
H2: IsD0Gpd DA
DB: B -> Type
H3: IsGraph B
H4: Is01Cat B
H5: Is0Gpd B
IsDGraph1: IsDGraph DB
IsD01Cat1: IsD01Cat DB
H6: IsD0Gpd DB
IsD0Gpd (pointwise_prod DA DB)
  intros [a1 b1] [a2 b2] [f g] [a1' b1'] [a2' b2'] [f' g'].A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
IsDGraph0: IsDGraph DA
IsD01Cat0: IsD01Cat DA
H2: IsD0Gpd DA
DB: B -> Type
H3: IsGraph B
H4: Is01Cat B
H5: Is0Gpd B
IsDGraph1: IsDGraph DB
IsD01Cat1: IsD01Cat DB
H6: IsD0Gpd DB
a1: A
b1: B
a2: A
b2: B
f: fst (a1, b1) $-> fst (a2, b2)
g: snd (a1, b1) $-> snd (a2, b2)
a1': DA (fst (a1, b1))
b1': DB (snd (a1, b1))
a2': DA (fst (a2, b2))
b2': DB (snd (a2, b2))
f': DHom f a1' a2'
g': DHom g b1' b2'
DHom (f, g)^$ (a2', b2') (a1', b1')
  exact (f'^$', g'^$').
Defined.

Instance isd2graph_prod {A B : Type} (DA : A -> Type) `{IsD2Graph A DA}
  (DB : B -> Type) `{IsD2Graph B DB}
  : IsD2Graph (pointwise_prod DA DB).A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is2Graph A
IsDGraph0: IsDGraph DA
H1: IsD2Graph DA
DB: B -> Type
H2: IsGraph B
H3: Is2Graph B
IsDGraph1: IsDGraph DB
H4: IsD2Graph DB
IsD2Graph (pointwise_prod DA DB)
Proof.A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is2Graph A
IsDGraph0: IsDGraph DA
H1: IsD2Graph DA
DB: B -> Type
H2: IsGraph B
H3: Is2Graph B
IsDGraph1: IsDGraph DB
H4: IsD2Graph DB
IsD2Graph (pointwise_prod DA DB)
  intros [a1 b1] [a2 b2] [a1' b1'] [a2' b2'].A, B: Type
DA: A -> Type
H: IsGraph A
H0: Is2Graph A
IsDGraph0: IsDGraph DA
H1: IsD2Graph DA
DB: B -> Type
H2: IsGraph B
H3: Is2Graph B
IsDGraph1: IsDGraph DB
H4: IsD2Graph DB
a1: A
b1: B
a2: A
b2: B
a1': DA (fst (a1, b1))
b1': DB (snd (a1, b1))
a2': DA (fst (a2, b2))
b2': DB (snd (a2, b2))
IsDGraph
  (fun f : (a1, b1) $-> (a2, b2) =>
   DHom f (a1', b1') (a2', b2'))
  srapply isdgraph_prod.
Defined.

Instance isd1cat_prod {A B : Type} (DA : A -> Type) `{IsD1Cat A DA}
  (DB : B -> Type) `{IsD1Cat B DB}
  : IsD1Cat (pointwise_prod DA DB).A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsD1Cat (pointwise_prod DA DB)
Proof.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
IsD1Cat (pointwise_prod DA DB)
  snapply Build_IsD1Cat.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b : A * B) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b),
IsD01Cat (fun f : a $-> b => DHom f a' b')
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b : A * B) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b),
IsD0Gpd (fun f : a $-> b => DHom f a' b')
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b c : A * B) 
(g : b $-> c) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c) 
(g' : DHom g b' c'),
IsD0Functor (cat_postcomp a g) (dcat_postcomp g')
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b c : A * B) 
(f : a $-> b) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c) 
(f' : DHom f a' b'),
IsD0Functor (cat_precomp c f) (dcat_precomp f')
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b c d : A * B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c)
(d' : pointwise_prod DA DB d) 
(f' : DHom f a' b') (g' : DHom g b' c')
(h' : DHom h c' d'),
DHom (cat_assoc f g h) 
  (h' $o' g' $o' f') (h' $o' (g' $o' f'))
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b c d : A * B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c)
(d' : pointwise_prod DA DB d) 
(f' : DHom f a' b') (g' : DHom g b' c')
(h' : DHom h c' d'),
DHom (cat_assoc_opp f g h) 
  (h' $o' (g' $o' f')) 
  (h' $o' g' $o' f')
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b : A * B) (f : a $-> b)
(a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b) 
(f' : DHom f a' b'),
DHom (cat_idl f) (DId b' $o' f') f'
A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b : A * B) (f : a $-> b)
(a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b) 
(f' : DHom f a' b'),
DHom (cat_idr f) (f' $o' DId a') f'
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b : A * B) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b),
IsD01Cat (fun f : a $-> b => DHom f a' b') intros ab1 ab2 ab1' ab2'.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2: A * B
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
IsD01Cat (fun f : ab1 $-> ab2 => DHom f ab1' ab2')
    srapply isd01cat_prod.
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b : A * B) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b),
IsD0Gpd (fun f : a $-> b => DHom f a' b') intros ab1 ab2 ab1' ab2'.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2: A * B
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
IsD0Gpd (fun f : ab1 $-> ab2 => DHom f ab1' ab2')
    exact (isd0gpd_prod _ _).
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b c : A * B) 
(g : b $-> c) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c) 
(g' : DHom g b' c'),
IsD0Functor (cat_postcomp a g) (dcat_postcomp g') intros ab1 ab2 ab3 fg ab1' ab2' ab3' [f' g'].A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2, ab3: A * B
fg: ab2 $-> ab3
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
ab3': pointwise_prod DA DB ab3
f': DHom (fst fg) (fst ab2') (fst ab3')
g': DHom (snd fg) (snd ab2') (snd ab3')
IsD0Functor (cat_postcomp ab1 fg)
  (dcat_postcomp (f', g'))
    intros hk1 hk2 pq hk1' hk2' [p' q'].A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2, ab3: A * B
fg: ab2 $-> ab3
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
ab3': pointwise_prod DA DB ab3
f': DHom (fst fg) (fst ab2') (fst ab3')
g': DHom (snd fg) (snd ab2') (snd ab3')
hk1, hk2: ab1 $-> ab2
pq: hk1 $-> hk2
hk1': DHom hk1 ab1' ab2'
hk2': DHom hk2 ab1' ab2'
p': DHom (fst pq) (fst hk1') (fst hk2')
q': DHom (snd pq) (snd hk1') (snd hk2')
DHom (fmap (cat_postcomp ab1 fg) pq)
  (dcat_postcomp (f', g') hk1 hk1')
  (dcat_postcomp (f', g') hk2 hk2')
    exact (f' $@L' p', g' $@L' q').
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b c : A * B) 
(f : a $-> b) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c) 
(f' : DHom f a' b'),
IsD0Functor (cat_precomp c f) (dcat_precomp f') intros ab1 ab2 ab3 fg ab1' ab2' ab3' [f' g'].A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2, ab3: A * B
fg: ab1 $-> ab2
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
ab3': pointwise_prod DA DB ab3
f': DHom (fst fg) (fst ab1') (fst ab2')
g': DHom (snd fg) (snd ab1') (snd ab2')
IsD0Functor (cat_precomp ab3 fg)
  (dcat_precomp (f', g'))
    intros hk1 hk2 pq hk1' hk2' [p' q'].A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2, ab3: A * B
fg: ab1 $-> ab2
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
ab3': pointwise_prod DA DB ab3
f': DHom (fst fg) (fst ab1') (fst ab2')
g': DHom (snd fg) (snd ab1') (snd ab2')
hk1, hk2: ab2 $-> ab3
pq: hk1 $-> hk2
hk1': DHom hk1 ab2' ab3'
hk2': DHom hk2 ab2' ab3'
p': DHom (fst pq) (fst hk1') (fst hk2')
q': DHom (snd pq) (snd hk1') (snd hk2')
DHom (fmap (cat_precomp ab3 fg) pq)
  (dcat_precomp (f', g') hk1 hk1')
  (dcat_precomp (f', g') hk2 hk2')
    exact (p' $@R' f', q' $@R' g').
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b c d : A * B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c)
(d' : pointwise_prod DA DB d) 
(f' : DHom f a' b') (g' : DHom g b' c')
(h' : DHom h c' d'),
DHom (cat_assoc f g h) 
  (h' $o' g' $o' f') (h' $o' (g' $o' f')) intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2, ab3, ab4: A * B
fg1: ab1 $-> ab2
fg2: ab2 $-> ab3
fg3: ab3 $-> ab4
forall (a' : pointwise_prod DA DB ab1)
(b' : pointwise_prod DA DB ab2)
(c' : pointwise_prod DA DB ab3)
(d' : pointwise_prod DA DB ab4) 
(f' : DHom fg1 a' b') (g' : DHom fg2 b' c')
(h' : DHom fg3 c' d'),
DHom (cat_assoc fg1 fg2 fg3) 
  (h' $o' g' $o' f') (h' $o' (g' $o' f'))
    intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2, ab3, ab4: A * B
fg1: ab1 $-> ab2
fg2: ab2 $-> ab3
fg3: ab3 $-> ab4
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
ab3': pointwise_prod DA DB ab3
ab4': pointwise_prod DA DB ab4
f1': DHom (fst fg1) (fst ab1') (fst ab2')
g1': DHom (snd fg1) (snd ab1') (snd ab2')
f2': DHom (fst fg2) (fst ab2') (fst ab3')
g2': DHom (snd fg2) (snd ab2') (snd ab3')
f3': DHom (fst fg3) (fst ab3') (fst ab4')
g3': DHom (snd fg3) (snd ab3') (snd ab4')
DHom (cat_assoc fg1 fg2 fg3)
  ((f3', g3') $o' (f2', g2') $o' (f1', g1'))
  ((f3', g3') $o' ((f2', g2') $o' (f1', g1')))
    exact (dcat_assoc f1' f2' f3', dcat_assoc g1' g2' g3').
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b c d : A * B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d) (a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b)
(c' : pointwise_prod DA DB c)
(d' : pointwise_prod DA DB d) 
(f' : DHom f a' b') (g' : DHom g b' c')
(h' : DHom h c' d'),
DHom (cat_assoc_opp f g h) 
  (h' $o' (g' $o' f')) 
  (h' $o' g' $o' f') intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2, ab3, ab4: A * B
fg1: ab1 $-> ab2
fg2: ab2 $-> ab3
fg3: ab3 $-> ab4
forall (a' : pointwise_prod DA DB ab1)
(b' : pointwise_prod DA DB ab2)
(c' : pointwise_prod DA DB ab3)
(d' : pointwise_prod DA DB ab4) 
(f' : DHom fg1 a' b') (g' : DHom fg2 b' c')
(h' : DHom fg3 c' d'),
DHom (cat_assoc_opp fg1 fg2 fg3) 
  (h' $o' (g' $o' f')) 
  (h' $o' g' $o' f')
    intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2, ab3, ab4: A * B
fg1: ab1 $-> ab2
fg2: ab2 $-> ab3
fg3: ab3 $-> ab4
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
ab3': pointwise_prod DA DB ab3
ab4': pointwise_prod DA DB ab4
f1': DHom (fst fg1) (fst ab1') (fst ab2')
g1': DHom (snd fg1) (snd ab1') (snd ab2')
f2': DHom (fst fg2) (fst ab2') (fst ab3')
g2': DHom (snd fg2) (snd ab2') (snd ab3')
f3': DHom (fst fg3) (fst ab3') (fst ab4')
g3': DHom (snd fg3) (snd ab3') (snd ab4')
DHom (cat_assoc_opp fg1 fg2 fg3)
  ((f3', g3') $o' ((f2', g2') $o' (f1', g1')))
  ((f3', g3') $o' (f2', g2') $o' (f1', g1'))
    exact (dcat_assoc_opp f1' f2' f3', dcat_assoc_opp g1' g2' g3').
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b : A * B) (f : a $-> b)
(a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b) 
(f' : DHom f a' b'),
DHom (cat_idl f) (DId b' $o' f') f' intros ab1 ab2 fg ab1' ab2' [f' g'].A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2: A * B
fg: ab1 $-> ab2
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
f': DHom (fst fg) (fst ab1') (fst ab2')
g': DHom (snd fg) (snd ab1') (snd ab2')
DHom (cat_idl fg) (DId ab2' $o' (f', g')) (f', g')
    exact (dcat_idl f', dcat_idl g').
  -A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
forall (a b : A * B) (f : a $-> b)
(a' : pointwise_prod DA DB a)
(b' : pointwise_prod DA DB b) 
(f' : DHom f a' b'),
DHom (cat_idr f) (f' $o' DId a') f' intros ab1 ab2 fg ab1' ab2' [f' g'].A, B: Type
DA: A -> Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsDGraph0: IsDGraph DA
IsD2Graph0: IsD2Graph DA
IsD01Cat0: IsD01Cat DA
H0: IsD1Cat DA
DB: B -> Type
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsDGraph1: IsDGraph DB
IsD2Graph1: IsD2Graph DB
IsD01Cat1: IsD01Cat DB
H2: IsD1Cat DB
ab1, ab2: A * B
fg: ab1 $-> ab2
ab1': pointwise_prod DA DB ab1
ab2': pointwise_prod DA DB ab2
f': DHom (fst fg) (fst ab1') (fst ab2')
g': DHom (snd fg) (snd ab1') (snd ab2')
DHom (cat_idr fg) ((f', g') $o' DId ab1') (f', g')
    exact (dcat_idr f', dcat_idr g').
Defined.