Skip to content

Instantly share code, notes, and snippets.

@stepchowfun

stepchowfun/gigantic-proof-goal

Last active December 12, 2017 02:54
Show Gist options
  • Save stepchowfun/3972552274b3520e8028d41d988f8ecd to your computer and use it in GitHub Desktop.
Save stepchowfun/3972552274b3520e8028d41d988f8ecd to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gigantic-proof-goal
1 subgoal
w, x, y, z : category
oMap : w -> x
fMap : forall x0 y : w, arrow w x0 y -> arrow x (oMap x0) (oMap y)
fIdent : forall x0 : w, fMap x0 x0 (id w) = id x
fComp : forall (x0 y z : w) (f : arrow w x0 y) (g : arrow w y z),
compose x (fMap y z g) (fMap x0 y f) = fMap x0 z (compose w g f)
oMap0 : x -> y
fMap0 : forall x0 y0 : x, arrow x x0 y0 -> arrow y (oMap0 x0) (oMap0 y0)
fIdent0 : forall x0 : x, fMap0 x0 x0 (id x) = id y
fComp0 : forall (x0 y0 z : x) (f : arrow x x0 y0) (g : arrow x y0 z),
compose y (fMap0 y0 z g) (fMap0 x0 y0 f) =
fMap0 x0 z (compose x g f)
oMap1 : y -> z
fMap1 : forall x y0 : y, arrow y x y0 -> arrow z (oMap1 x) (oMap1 y0)
fIdent1 : forall x : y, fMap1 x x (id y) = id z
fComp1 : forall (x y0 z0 : y) (f : arrow y x y0) (g : arrow y y0 z0),
compose z (fMap1 y0 z0 g) (fMap1 x y0 f) =
fMap1 x z0 (compose y g f)
______________________________________(1/1)
{|
oMap := fun x0 : w =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y0 : w) (f : arrow w x1 y0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y0 z0 : w) (f : arrow w x1 y0)
(g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |} x0);
fMap := fun (x0 y0 : w) (f : arrow w x0 y0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z0 : w) (f0 : arrow w x1 y1)
(g : arrow w y1 z0) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f0))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z0 f0 g))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |} f);
fIdent := fun x0 : w =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y0 : w) (f : arrow w x1 y0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
=> a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y0 z0 : w) (f : arrow w x1 y0)
(g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |} x0)
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y0 : w) (f : arrow w x1 y0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
=> a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y0 z0 : w) (f : arrow w x1 y0)
(g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |} x0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y0 : w) (f : arrow w x1 y0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
=>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
x1)) => a = id y)
eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y0 z0 : w) (f : arrow w x1 y0)
(g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0))
=>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g f)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
=>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g f))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |} x0))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y0 : w) (f : arrow w x1 y0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
=>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
x1)) => a = id y)
eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y0 z0 : w) (f : arrow w x1 y0)
(g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0))
=>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g f)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
=>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g f))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |} x0))
=> a = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y0 : w) (f : arrow w x1 y0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y0 z0 : w) (f : arrow w x1 y0)
(g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |} x0)))
(Functor.fIdent
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y0 : w) (f : arrow w x1 y0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y0 z0 : w) (f : arrow w x1 y0)
(g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |} x0);
fComp := fun (x0 y0 z0 : w) (f : arrow w x0 y0) (g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
=> a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g0 f0))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} x0))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
=> a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g0 f0))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a0 : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a0 = id y)
(eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a0 = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a0 =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
(eq_ind_r
(fun
a0 : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a0 =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} (compose w g f)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
=> a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g0 f0))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} x0)
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
=> a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |}
(compose w g0 f0))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} z0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a0 : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a0 = id y)
(eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a0 = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a0 =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
(eq_ind_r
(fun
a0 : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a0 =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |}
(compose w g f))) eq_refl
(Functor.fComp
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} x0 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} x0)
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} y0)
(Functor.oMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} z0)
(Functor.fMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} f)
(Functor.fMap
{|
oMap := fun x1 : w =>
Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fMap := fun (x1 y1 : w) (f0 : arrow w x1 y1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0);
fIdent := fun x1 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a = id y)
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)) =>
a = id y) eq_refl
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1);
fComp := fun (x1 y1 z1 : w) (f0 : arrow w x1 y1)
(g0 : arrow w y1 z1) =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1))
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1) =>
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} a =
Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y1)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z1)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g0)) |} g)) |} =
{|
oMap := fun x0 : w =>
Functor.oMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y0 : x) (f : arrow x x1 y0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)) => a = id z)
eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y0 z0 : x) (f : arrow x x1 y0) (g : arrow x y0 z0)
=>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g f)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g f))) eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y0)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g)) |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0);
fMap := fun (x0 y0 : w) (f : arrow w x0 y0) =>
Functor.fMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y1 : x) (f0 : arrow x x1 y1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)) => a = id z)
eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y1 z0 : x) (f0 : arrow x x1 y1)
(g : arrow x y1 z0) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g f0)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g f0))) eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y1 z0 f0 g))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g)) |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f);
fIdent := fun x0 : w =>
eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0) =>
Functor.fMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y0 : x) (f : arrow x x1 y0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a0 = id z)
(eq_ind_r
(fun
a0 : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)) =>
a0 = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y0 z0 : x) (f : arrow x x1 y0)
(g : arrow x y0 z0) =>
eq_ind_r
(fun
a0 : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)) =>
a0 =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g f)))
(eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a0 =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g f)))
eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y0)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g)) |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y0 : x) (f : arrow x x1 y0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
x1)) => a = id z)
eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y0 z0 : x) (f : arrow x x1 y0)
(g : arrow x y0 z0) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0))
=>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(compose x g f)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)
=>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(compose x g f))) eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y0)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g)) |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0))
(Functor.oMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y0 : x) (f : arrow x x1 y0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
x1)) => a = id z)
eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y0 z0 : x) (f : arrow x x1 y0)
(g : arrow x y0 z0) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0))
=>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(compose x g f)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)
=>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(compose x g f))) eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y0)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g)) |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0)) => a = id z) eq_refl
(Functor.fIdent
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y0 : x) (f : arrow x x1 y0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)) =>
a = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y0 z0 : x) (f : arrow x x1 y0)
(g : arrow x y0 z0) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)) =>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g f)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g f)))
eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y0 z0 f g))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y0)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g)) |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0)))
(Functor.fIdent
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0);
fComp := fun (x0 y0 z0 : w) (f : arrow w x0 y0) (g : arrow w y0 z0) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y1 : x) (f0 : arrow x x1 y1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
=> a = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y1 z1 : x) (f0 : arrow x x1 y1)
(g0 : arrow x y1 z1) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(compose x g0 f0))) eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g0)) |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0))
(Functor.oMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y1 : x) (f0 : arrow x x1 y1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
=> a = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y1 z1 : x) (f0 : arrow x x1 y1)
(g0 : arrow x y1 z1) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |}
(compose x g0 f0))) eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g0)) |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)) =>
a =
Functor.fMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y1 : x) (f0 : arrow x x1 y1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a0 = id z)
(eq_ind_r
(fun
a0 : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)) =>
a0 = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y1 z1 : x) (f0 : arrow x x1 y1)
(g0 : arrow x y1 z1) =>
eq_ind_r
(fun
a0 : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)) =>
a0 =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
(eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a0 =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g0)) |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f)))
(eq_ind_r
(fun
a : arrow x
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0) =>
Functor.fMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y1 : x) (f0 : arrow x x1 y1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a0 = id z)
(eq_ind_r
(fun
a0 : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)) =>
a0 = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y1 z1 : x) (f0 : arrow x x1 y1)
(g0 : arrow x y1 z1) =>
eq_ind_r
(fun
a0 : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)) =>
a0 =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
(eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a0 =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g0)) |} a =
Functor.fMap
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y1 : x) (f0 : arrow x x1 y1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a0 = id z)
(eq_ind_r
(fun
a0 : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)) =>
a0 = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y1 z1 : x) (f0 : arrow x x1 y1)
(g0 : arrow x y1 z1) =>
eq_ind_r
(fun
a0 : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)) =>
a0 =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
(eq_ind_r
(fun
a0 : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a0 =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g0)) |}
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} (compose w g f))) eq_refl
(Functor.fComp
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0 y0 z0 f g))
(Functor.fComp
{|
oMap := fun x1 : x =>
Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fMap := fun (x1 y1 : x) (f0 : arrow x x1 y1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0);
fIdent := fun x1 : x =>
eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a = id z)
(eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)) =>
a = id z) eq_refl
(Functor.fIdent
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)))
(Functor.fIdent
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1);
fComp := fun (x1 y1 z1 : x) (f0 : arrow x x1 y1)
(g0 : arrow x y1 z1) =>
eq_ind_r
(fun
a : arrow z
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1))
(Functor.oMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)) =>
a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
(eq_ind_r
(fun
a : arrow y
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1) =>
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |} a =
Functor.fMap
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} (compose x g0 f0)))
eq_refl
(Functor.fComp
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1 y1 z1 f0 g0))
(Functor.fComp
{|
oMap := oMap1;
fMap := fMap1;
fIdent := fIdent1;
fComp := fComp1 |}
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} x1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} y1)
(Functor.oMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} z1)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} f0)
(Functor.fMap
{|
oMap := oMap0;
fMap := fMap0;
fIdent := fIdent0;
fComp := fComp0 |} g0)) |}
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} x0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} y0)
(Functor.oMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} z0)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} f)
(Functor.fMap
{|
oMap := oMap;
fMap := fMap;
fIdent := fIdent;
fComp := fComp |} g)) |}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment