Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(499 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(22 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(37 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(9 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(41 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(51 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(47 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(280 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(10 entries)

---

Global Index

A

Assoc [projection, in category]
assoc [lemma, in category]

B

Build_Equal_hom [constructor, in category]

C

carrier [definition, in monad_def]
Cat [record, in category]
Category [record, in category]
category [library]
Category_mor [definition, in category]
Category_obj [definition, in category]
Category_structure [definition, in category]
CatFunct [section, in CatFunct]
CatFunct [library]
CatFunct.C [variable, in CatFunct]
CatFunct.D [variable, in CatFunct]
CatFunct.morC [variable, in CatFunct]
CatFunct.morD [variable, in CatFunct]
CatFunct.obC [variable, in CatFunct]
CatFunct.obD [variable, in CatFunct]
cat_lemmata [section, in category]
cat_lemmata.a [variable, in category]
cat_lemmata.b [variable, in category]
cat_lemmata.c [variable, in category]
cat_lemmata.C [variable, in category]
cat_lemmata.d [variable, in category]
cat_lemmata.f [variable, in category]
cat_lemmata.f' [variable, in category]
cat_lemmata.f'' [variable, in category]
cat_lemmata.g [variable, in category]
cat_lemmata.h [variable, in category]
cat_lemmata.hom [variable, in category]
cat_lemmata.ob [variable, in category]
cat_SET [library]
comp [projection, in category]
CompF [instance, in functor]
CompFassoc [lemma, in functor]
CompF_assoc [lemma, in functor]
CompF_compat_with_eq_Functor [lemma, in functor]
CompF_Morphism [section, in functor]
CompF_Morphism.C [variable, in functor]
CompF_Morphism.D [variable, in functor]
CompF_Morphism.E [variable, in functor]
CompF_Morphism.morC [variable, in functor]
CompF_Morphism.morD [variable, in functor]
CompF_Morphism.morE [variable, in functor]
CompF_Morphism.obC [variable, in functor]
CompF_Morphism.obD [variable, in functor]
CompF_Morphism.obE [variable, in functor]
Comp_Fmor [definition, in functor]
Comp_Fobj [definition, in functor]
Comp_Functor [section, in functor]
Comp_Functor.C [variable, in functor]
Comp_Functor.D [variable, in functor]
Comp_Functor.E [variable, in functor]
Comp_Functor.F [variable, in functor]
Comp_Functor.G [variable, in functor]
Comp_Functor.morC [variable, in functor]
Comp_Functor.morD [variable, in functor]
Comp_Functor.morE [variable, in functor]
Comp_Functor.obC [variable, in functor]
Comp_Functor.obD [variable, in functor]
Comp_Functor.obE [variable, in functor]
Comp_functor_map_morphism [lemma, in functor]
comp_oid [projection, in category]
Comp_preserve_comp [lemma, in functor]
Comp_preserve_ident [lemma, in functor]
comp_tensor [instance, in smon_cats]

D

dist [projection, in monad_haskell]

E

e [projection, in smon_cats]
eleft [instance, in smon_cats]
eleft_unit [projection, in smon_cats]
endo_monad [section, in smon_cats]
endo_monad.C [variable, in smon_cats]
eqFunctor [section, in functor]
eqFunctor.C [variable, in functor]
eqFunctor.D [variable, in functor]
eqFunctor.morC [variable, in functor]
eqFunctor.morD [variable, in functor]
eqFunctor.obC [variable, in functor]
eqFunctor.obD [variable, in functor]
eqFunctor1 [section, in functor]
eqFunctor1.C [variable, in functor]
eqFunctor1.D [variable, in functor]
eqFunctor1.E [variable, in functor]
eqFunctor1.E' [variable, in functor]
eqFunctor1.F [variable, in functor]
eqFunctor1.G [variable, in functor]
eqFunctor1.H [variable, in functor]
eqFunctor1.morC [variable, in functor]
eqFunctor1.morD [variable, in functor]
eqFunctor1.morE [variable, in functor]
eqFunctor1.morE' [variable, in functor]
eqFunctor1.obC [variable, in functor]
eqFunctor1.obD [variable, in functor]
eqFunctor1.obE [variable, in functor]
eqFunctor1.obE' [variable, in functor]
Equal_hom [inductive, in category]
Equal_hom [section, in category]
Equal_hom.C [variable, in category]
Equal_hom.hom [variable, in category]
Equal_hom.ob [variable, in category]
Equal_hom_imp_setoideq [lemma, in category]
Equal_hom_imp_setoideq2 [lemma, in category]
Equal_hom_refl [lemma, in category]
Equal_hom_src [lemma, in category]
Equal_hom_sym [lemma, in category]
Equal_hom_tgt [lemma, in category]
Equal_hom_trans [lemma, in category]
Equal_NT [definition, in horcomp]
Equal_NTh [definition, in horcomp]
Equal_NTh_lemmata [section, in horcomp]
Equal_NTh_lemmata.C [variable, in horcomp]
Equal_NTh_lemmata.D [variable, in horcomp]
Equal_NTh_lemmata.morC [variable, in horcomp]
Equal_NTh_lemmata.morD [variable, in horcomp]
Equal_NTh_lemmata.obC [variable, in horcomp]
Equal_NTh_lemmata.obD [variable, in horcomp]
Equal_NT_equiv [lemma, in horcomp]
Equal_NT_refl [lemma, in horcomp]
Equal_NT_sym [lemma, in horcomp]
Equal_NT_trans [lemma, in horcomp]
eq_Functor [definition, in functor]
eq_Functor1 [definition, in functor]
eq_Functor_equiv [lemma, in functor]
eq_Functor_imp_eq_Fobj [lemma, in functor]
eq_Functor_imp_eq_Fobj [section, in functor]
eq_Functor_imp_eq_Fobj.C [variable, in functor]
eq_Functor_imp_eq_Fobj.D [variable, in functor]
eq_Functor_imp_eq_Fobj.F [variable, in functor]
eq_Functor_imp_eq_Fobj.G [variable, in functor]
eq_Functor_imp_eq_Fobj.H [variable, in functor]
eq_Functor_imp_eq_Fobj.morC [variable, in functor]
eq_Functor_imp_eq_Fobj.morD [variable, in functor]
eq_Functor_imp_eq_Fobj.obC [variable, in functor]
eq_Functor_imp_eq_Fobj.obD [variable, in functor]
Eq_Monad [definition, in monad_def]
Eq_Monad1 [definition, in monad_def]
Eq_Monad_oid [lemma, in monad_def]
eq_NT [definition, in NT]
eq_NTh [section, in horcomp]
eq_NTh [definition, in horcomp]
eq_NTh.alpha [variable, in horcomp]
eq_NTh.beta [variable, in horcomp]
eq_NTh.C [variable, in horcomp]
eq_NTh.D [variable, in horcomp]
eq_NTh.F [variable, in horcomp]
eq_NTh.F' [variable, in horcomp]
eq_NTh.G [variable, in horcomp]
eq_NTh.G' [variable, in horcomp]
eq_NTh.morC [variable, in horcomp]
eq_NTh.morD [variable, in horcomp]
eq_NTh.obC [variable, in horcomp]
eq_NTh.obD [variable, in horcomp]
eq_NTh_lemmata [section, in horcomp]
eq_NTh_lemmata.alpha [variable, in horcomp]
eq_NTh_lemmata.beta [variable, in horcomp]
eq_NTh_lemmata.C [variable, in horcomp]
eq_NTh_lemmata.D [variable, in horcomp]
eq_NTh_lemmata.F [variable, in horcomp]
eq_NTh_lemmata.F' [variable, in horcomp]
eq_NTh_lemmata.F'' [variable, in horcomp]
eq_NTh_lemmata.G [variable, in horcomp]
eq_NTh_lemmata.gamma [variable, in horcomp]
eq_NTh_lemmata.G' [variable, in horcomp]
eq_NTh_lemmata.G'' [variable, in horcomp]
eq_NTh_lemmata.morC [variable, in horcomp]
eq_NTh_lemmata.morD [variable, in horcomp]
eq_NTh_lemmata.obC [variable, in horcomp]
eq_NTh_lemmata.obD [variable, in horcomp]
eq_NTh_refl [lemma, in horcomp]
eq_NTh_sym [lemma, in horcomp]
eq_NTh_trans [lemma, in horcomp]
eq_NT1 [definition, in NT]
eq_NT_equiv [lemma, in NT]
eright [instance, in smon_cats]
erightleft [section, in smon_cats]
erightleft.C [variable, in smon_cats]
erightleft.e [variable, in smon_cats]
eright_unit [projection, in smon_cats]
eta [projection, in monad_haskell]
ETA [projection, in monad_def]
eta1 [projection, in monad_def]
eta2 [projection, in monad_def]
eta_kl [projection, in monad_haskell]
eta_mu_ax1 [definition, in monad_def]
eta_mu_ax2 [definition, in monad_def]

F

F [projection, in monad_haskell]
FComp [lemma, in functor]
FId [lemma, in functor]
FM [definition, in monad_haskell]
Fmor [projection, in functor]
Fobj [projection, in functor]
FunctCat [instance, in CatFunct]
FunctCat_lemmata [section, in CatFunct]
FunctCat_lemmata.alpha [variable, in CatFunct]
FunctCat_lemmata.beta [variable, in CatFunct]
FunctCat_lemmata.C [variable, in CatFunct]
FunctCat_lemmata.D [variable, in CatFunct]
FunctCat_lemmata.F [variable, in CatFunct]
FunctCat_lemmata.G [variable, in CatFunct]
FunctCat_lemmata.h [variable, in CatFunct]
FunctCat_lemmata.H [variable, in CatFunct]
FunctCat_lemmata.h' [variable, in CatFunct]
FunctCat_lemmata.K [variable, in CatFunct]
FunctCat_lemmata.morC [variable, in CatFunct]
FunctCat_lemmata.morD [variable, in CatFunct]
FunctCat_lemmata.obC [variable, in CatFunct]
FunctCat_lemmata.obD [variable, in CatFunct]
FunctCat_struct [instance, in CatFunct]
Functor [record, in functor]
functor [library]
Functors [section, in functor]
Functors.morC [variable, in functor]
Functors.morD [variable, in functor]
Functors.obC [variable, in functor]
Functors.obD [variable, in functor]
Functor_Composition_Morphism [section, in functor]
Functor_Composition_Morphism.C [variable, in functor]
Functor_Composition_Morphism.D [variable, in functor]
Functor_Composition_Morphism.E [variable, in functor]
Functor_Composition_Morphism.morC [variable, in functor]
Functor_Composition_Morphism.morD [variable, in functor]
Functor_Composition_Morphism.morE [variable, in functor]
Functor_Composition_Morphism.obC [variable, in functor]
Functor_Composition_Morphism.obD [variable, in functor]
Functor_Composition_Morphism.obE [variable, in functor]
Functor_Comp_Id [section, in functor]
Functor_Comp_Id.C [variable, in functor]
Functor_Comp_Id.D [variable, in functor]
Functor_Comp_Id.E [variable, in functor]
Functor_Comp_Id.E' [variable, in functor]
Functor_Comp_Id.F [variable, in functor]
Functor_Comp_Id.G [variable, in functor]
Functor_Comp_Id.H [variable, in functor]
Functor_Comp_Id.morC [variable, in functor]
Functor_Comp_Id.morD [variable, in functor]
Functor_Comp_Id.morE [variable, in functor]
Functor_Comp_Id.morE' [variable, in functor]
Functor_Comp_Id.obC [variable, in functor]
Functor_Comp_Id.obD [variable, in functor]
Functor_Comp_Id.obE [variable, in functor]
Functor_Comp_Id.obE' [variable, in functor]
Functor_equal [lemma, in functor]
Functor_equal [section, in functor]
Functor_equal.C [variable, in functor]
Functor_equal.D [variable, in functor]
Functor_equal.morC [variable, in functor]
Functor_equal.morD [variable, in functor]
Functor_equal.obC [variable, in functor]
Functor_equal.obD [variable, in functor]
Functor_Fobj [definition, in functor]
Functor_lemmata [section, in functor]
Functor_lemmata.a [variable, in functor]
Functor_lemmata.b [variable, in functor]
Functor_lemmata.c [variable, in functor]
Functor_lemmata.C [variable, in functor]
Functor_lemmata.D [variable, in functor]
Functor_lemmata.f [variable, in functor]
Functor_lemmata.F [variable, in functor]
Functor_lemmata.g [variable, in functor]
Functor_lemmata.morC [variable, in functor]
Functor_lemmata.morD [variable, in functor]
Functor_lemmata.obC [variable, in functor]
Functor_lemmata.obD [variable, in functor]
functor_map_morphism [projection, in functor]

G

gr [lemma, in CatFunct]

H

hcomp [section, in horcomp]
hcompNT [instance, in horcomp]
hcompNT1 [definition, in horcomp]
hcompNT_ax [lemma, in horcomp]
hcomp.A [variable, in horcomp]
hcomp.alpha [variable, in horcomp]
hcomp.B [variable, in horcomp]
hcomp.beta [variable, in horcomp]
hcomp.C [variable, in horcomp]
hcomp.F [variable, in horcomp]
hcomp.F' [variable, in horcomp]
hcomp.G [variable, in horcomp]
hcomp.G' [variable, in horcomp]
hcomp.morA [variable, in horcomp]
hcomp.morB [variable, in horcomp]
hcomp.morC [variable, in horcomp]
hcomp.obA [variable, in horcomp]
hcomp.obB [variable, in horcomp]
hcomp.obC [variable, in horcomp]
helper [lemma, in functor]
helper2 [lemma, in functor]
hidNT [section, in horcomp]
hidNT [instance, in horcomp]
hidNT.C [variable, in horcomp]
hidNT.morC [variable, in horcomp]
hidNT.obC [variable, in horcomp]
hidNT1 [definition, in horcomp]
hidNT_ax [lemma, in horcomp]
hidNT_unit [section, in horcomp]
hidNT_unit.alpha [variable, in horcomp]
hidNT_unit.C [variable, in horcomp]
hidNT_unit.D [variable, in horcomp]
hidNT_unit.F [variable, in horcomp]
hidNT_unit.G [variable, in horcomp]
hidNT_unit.morC [variable, in horcomp]
hidNT_unit.morD [variable, in horcomp]
hidNT_unit.obC [variable, in horcomp]
hidNT_unit.obD [variable, in horcomp]
hid_L [lemma, in horcomp]
hid_l [lemma, in horcomp]
hom_refl [lemma, in category]
hom_sym [lemma, in category]
hom_trans [lemma, in category]
hom_transport [definition, in category]
hom_transport_id [lemma, in category]
hom_transport_pi [lemma, in category]
horcomp [library]
hor_comp [section, in horcomp]
hor_comp.alpha [variable, in horcomp]
hor_comp.C [variable, in horcomp]
hor_comp.D [variable, in horcomp]
hor_comp.F [variable, in horcomp]
hor_comp.G [variable, in horcomp]
hor_comp.morC [variable, in horcomp]
hor_comp.morD [variable, in horcomp]
hor_comp.obC [variable, in horcomp]
hor_comp.obD [variable, in horcomp]

I

Id [instance, in functor]
id [projection, in category]
IdFl [lemma, in functor]
IdFr [lemma, in functor]
IdF_unit_l [lemma, in functor]
IdF_unit_r [lemma, in functor]
idl [lemma, in category]
idr [lemma, in category]
Id_Functor [section, in functor]
Id_Functor.C [variable, in functor]
Id_Functor.mor [variable, in functor]
Id_Functor.ob [variable, in functor]
id_l [projection, in category]
id_r [projection, in category]
iso [instance, in smon_cats]

K

kleisli [projection, in monad_haskell]
kleisli_oid [projection, in monad_haskell]
kl_eta [projection, in monad_haskell]

M

MEtatrafo [instance, in monad_haskell]
MFunc [instance, in monad_haskell]
Mmor [definition, in monad_haskell]
MMu [definition, in monad_haskell]
MMutrafo [instance, in monad_haskell]
Monad [record, in monad_def]
monads [section, in smon_cats]
monads [instance, in smon_cats]
monads.C [variable, in smon_cats]
monad_def [section, in monad_def]
monad_def [library]
monad_def.C [variable, in monad_def]
monad_def.morC [variable, in monad_def]
monad_def.obC [variable, in monad_def]
monad_def.obD [variable, in monad_def]
Monad_from_Monad_h_struct [instance, in monad_haskell]
Monad_gives_Monad_h [section, in monad_haskell]
Monad_gives_Monad_h.C [variable, in monad_haskell]
Monad_gives_Monad_h.M [variable, in monad_haskell]
Monad_gives_Monad_h.mor [variable, in monad_haskell]
Monad_gives_Monad_h.ob [variable, in monad_haskell]
Monad_h [record, in monad_haskell]
monad_haskell [library]
monad_haskell_def [section, in monad_haskell]
monad_haskell_def.C [variable, in monad_haskell]
monad_haskell_def.monad_haskell_class [section, in monad_haskell]
monad_haskell_def.monad_haskell_class.eta [variable, in monad_haskell]
monad_haskell_def.monad_haskell_class.F [variable, in monad_haskell]
monad_haskell_def.monad_haskell_class.kleisli [variable, in monad_haskell]
monad_haskell_def.mor [variable, in monad_haskell]
monad_haskell_def.ob [variable, in monad_haskell]
Monad_h_eta [definition, in monad_haskell]
Monad_h_F [definition, in monad_haskell]
Monad_h_from_Monad_struct [instance, in monad_haskell]
Monad_h_gives_Monad [section, in monad_haskell]
Monad_h_gives_Monad.C [variable, in monad_haskell]
Monad_h_gives_Monad.M [variable, in monad_haskell]
Monad_h_gives_Monad.mor [variable, in monad_haskell]
Monad_h_gives_Monad.ob [variable, in monad_haskell]
Monad_h_kl [definition, in monad_haskell]
monad_h_struct [projection, in monad_haskell]
Monad_h_struct [record, in monad_haskell]
monad_struct [projection, in monad_def]
Monad_struct [record, in monad_def]
mor [projection, in category]
mor_oid [projection, in category]
MU [projection, in monad_def]

N

no_choice [lemma, in horcomp]
NT [record, in NT]
NT [library]
NTcomm [lemma, in NT]
NTlarge [definition, in horcomp]
NTlarge [section, in horcomp]
NTlarge.C [variable, in horcomp]
NTlarge.D [variable, in horcomp]
NTlarge.morC [variable, in horcomp]
NTlarge.morD [variable, in horcomp]
NTlarge.obC [variable, in horcomp]
NTlarge.obD [variable, in horcomp]
NT_def [section, in NT]
NT_def.C [variable, in NT]
NT_def.D [variable, in NT]
NT_def.F [variable, in NT]
NT_def.G [variable, in NT]
NT_def.morC [variable, in NT]
NT_def.morD [variable, in NT]
NT_def.obC [variable, in NT]
NT_def.obD [variable, in NT]
NT_trafo [definition, in NT]
NT_type [definition, in horcomp]

O

obj [projection, in category]

P

PI [definition, in functor]
preserve_comp [projection, in functor]
preserve_ident [projection, in functor]
PROD [instance, in prods]
prods [library]
PROD_almost_assoc [section, in smon_cats]
PROD_almost_assoc.A [variable, in smon_cats]
PROD_almost_assoc.B [variable, in smon_cats]
PROD_almost_assoc.C [variable, in smon_cats]
prod_cat [section, in prods]
prod_cat.C [variable, in prods]
prod_cat.D [variable, in prods]
Prod_comp [definition, in prods]
Prod_equiv [definition, in prods]
Prod_equiv1 [definition, in prods]
Prod_equiv_equiv [lemma, in prods]
prod_Fmor [definition, in prods]
prod_Fobj [definition, in prods]
prod_func [section, in prods]
Prod_functor [instance, in prods]
prod_func.C [variable, in prods]
prod_func.C' [variable, in prods]
prod_func.D [variable, in prods]
prod_func.D' [variable, in prods]
prod_func.F [variable, in prods]
prod_func.G [variable, in prods]
Prod_id [definition, in prods]
Prod_mor [definition, in prods]
Prod_obj [definition, in prods]
PROD_struct [instance, in prods]

S

SET [instance, in cat_SET]
SET [section, in cat_SET]
SET.SET_data [section, in cat_SET]
SET.SET_data.A [variable, in cat_SET]
SET.SET_data.B [variable, in cat_SET]
SET_catstruct [instance, in cat_SET]
SET_hom [definition, in cat_SET]
SET_hom_equiv [definition, in cat_SET]
SET_hom_oid [definition, in cat_SET]
SET_hom_oid_prf [lemma, in cat_SET]
smon_cat [record, in smon_cats]
smon_cats [library]
struct [projection, in category]
subst [projection, in monad_def]
subst_ax [definition, in monad_def]

T

T [projection, in monad_def]
tensor [projection, in smon_cats]
tensor_assoc [projection, in smon_cats]
tra [definition, in horcomp]
trafo [projection, in NT]
trafo_ax [projection, in NT]
trafo_comm [definition, in NT]
transport [section, in category]
transport.C [variable, in category]
transport.Equal_hom_lemmata [section, in category]
transport.Equal_hom_lemmata.a [variable, in category]
transport.Equal_hom_lemmata.b [variable, in category]
transport.Equal_hom_lemmata.c [variable, in category]
transport.Equal_hom_lemmata.d [variable, in category]
transport.Equal_hom_lemmata.f [variable, in category]
transport.Equal_hom_lemmata.g [variable, in category]
transport.Equal_hom_lemmata.H [variable, in category]
transport.hom [variable, in category]
transport.ob [variable, in category]

V

vcompNT [section, in NT]
vcompNT [definition, in NT]
vcompNT.a [variable, in NT]
vcompNT.b [variable, in NT]
vcompNT.C [variable, in NT]
vcompNT.D [variable, in NT]
vcompNT.F [variable, in NT]
vcompNT.G [variable, in NT]
vcompNT.H [variable, in NT]
vcompNT.morC [variable, in NT]
vcompNT.morD [variable, in NT]
vcompNT.obC [variable, in NT]
vcompNT.obD [variable, in NT]
vcompNT1 [definition, in NT]
vcompNT1_ax [lemma, in NT]
VIDNT [section, in NT]
vidNT [instance, in NT]
VIDNT.C [variable, in NT]
VIDNT.D [variable, in NT]
VIDNT.F [variable, in NT]
VIDNT.morC [variable, in NT]
VIDNT.morD [variable, in NT]
VIDNT.obC [variable, in NT]
VIDNT.obD [variable, in NT]

---

Instance Index

C

CompF [in functor]
comp_tensor [in smon_cats]

E

eleft [in smon_cats]
eright [in smon_cats]

F

FunctCat [in CatFunct]
FunctCat_struct [in CatFunct]

H

hcompNT [in horcomp]
hidNT [in horcomp]

I

Id [in functor]
iso [in smon_cats]

M

MEtatrafo [in monad_haskell]
MFunc [in monad_haskell]
MMutrafo [in monad_haskell]
monads [in smon_cats]
Monad_from_Monad_h_struct [in monad_haskell]
Monad_h_from_Monad_struct [in monad_haskell]

P

PROD [in prods]
Prod_functor [in prods]
PROD_struct [in prods]

S

SET [in cat_SET]
SET_catstruct [in cat_SET]

V

vidNT [in NT]

---

Projection Index

A

Assoc [in category]

C

comp [in category]
comp_oid [in category]

D

dist [in monad_haskell]

E

e [in smon_cats]
eleft_unit [in smon_cats]
eright_unit [in smon_cats]
eta [in monad_haskell]
ETA [in monad_def]
eta1 [in monad_def]
eta2 [in monad_def]
eta_kl [in monad_haskell]

F

F [in monad_haskell]
Fmor [in functor]
Fobj [in functor]
functor_map_morphism [in functor]

I

id [in category]
id_l [in category]
id_r [in category]

K

kleisli [in monad_haskell]
kleisli_oid [in monad_haskell]
kl_eta [in monad_haskell]

M

monad_h_struct [in monad_haskell]
monad_struct [in monad_def]
mor [in category]
mor_oid [in category]
MU [in monad_def]

O

obj [in category]

P

preserve_comp [in functor]
preserve_ident [in functor]

S

struct [in category]
subst [in monad_def]

T

T [in monad_def]
tensor [in smon_cats]
tensor_assoc [in smon_cats]
trafo [in NT]
trafo_ax [in NT]

---

Record Index

C

Cat [in category]
Category [in category]

F

Functor [in functor]

M

Monad [in monad_def]
Monad_h [in monad_haskell]
Monad_h_struct [in monad_haskell]
Monad_struct [in monad_def]

N

NT [in NT]

S

smon_cat [in smon_cats]

---

Section Index

C

CatFunct [in CatFunct]
cat_lemmata [in category]
CompF_Morphism [in functor]
Comp_Functor [in functor]

E

endo_monad [in smon_cats]
eqFunctor [in functor]
eqFunctor1 [in functor]
Equal_hom [in category]
Equal_NTh_lemmata [in horcomp]
eq_Functor_imp_eq_Fobj [in functor]
eq_NTh [in horcomp]
eq_NTh_lemmata [in horcomp]
erightleft [in smon_cats]

F

FunctCat_lemmata [in CatFunct]
Functors [in functor]
Functor_Composition_Morphism [in functor]
Functor_Comp_Id [in functor]
Functor_equal [in functor]
Functor_lemmata [in functor]

H

hcomp [in horcomp]
hidNT [in horcomp]
hidNT_unit [in horcomp]
hor_comp [in horcomp]

I

Id_Functor [in functor]

M

monads [in smon_cats]
monad_def [in monad_def]
Monad_gives_Monad_h [in monad_haskell]
monad_haskell_def [in monad_haskell]
monad_haskell_def.monad_haskell_class [in monad_haskell]
Monad_h_gives_Monad [in monad_haskell]

N

NTlarge [in horcomp]
NT_def [in NT]

P

PROD_almost_assoc [in smon_cats]
prod_cat [in prods]
prod_func [in prods]

S

SET [in cat_SET]
SET.SET_data [in cat_SET]

T

transport [in category]
transport.Equal_hom_lemmata [in category]

V

vcompNT [in NT]
VIDNT [in NT]

---

Lemma Index

A

assoc [in category]

C

CompFassoc [in functor]
CompF_assoc [in functor]
CompF_compat_with_eq_Functor [in functor]
Comp_functor_map_morphism [in functor]
Comp_preserve_comp [in functor]
Comp_preserve_ident [in functor]

E

Equal_hom_imp_setoideq [in category]
Equal_hom_imp_setoideq2 [in category]
Equal_hom_refl [in category]
Equal_hom_src [in category]
Equal_hom_sym [in category]
Equal_hom_tgt [in category]
Equal_hom_trans [in category]
Equal_NT_equiv [in horcomp]
Equal_NT_refl [in horcomp]
Equal_NT_sym [in horcomp]
Equal_NT_trans [in horcomp]
eq_Functor_equiv [in functor]
eq_Functor_imp_eq_Fobj [in functor]
Eq_Monad_oid [in monad_def]
eq_NTh_refl [in horcomp]
eq_NTh_sym [in horcomp]
eq_NTh_trans [in horcomp]
eq_NT_equiv [in NT]

F

FComp [in functor]
FId [in functor]
Functor_equal [in functor]

G

gr [in CatFunct]

H

hcompNT_ax [in horcomp]
helper [in functor]
helper2 [in functor]
hidNT_ax [in horcomp]
hid_L [in horcomp]
hid_l [in horcomp]
hom_refl [in category]
hom_sym [in category]
hom_trans [in category]
hom_transport_id [in category]
hom_transport_pi [in category]

I

IdFl [in functor]
IdFr [in functor]
IdF_unit_l [in functor]
IdF_unit_r [in functor]
idl [in category]
idr [in category]

N

no_choice [in horcomp]
NTcomm [in NT]

P

Prod_equiv_equiv [in prods]

S

SET_hom_oid_prf [in cat_SET]

V

vcompNT1_ax [in NT]

---

Constructor Index

B

Build_Equal_hom [in category]

---

Inductive Index

E

Equal_hom [in category]

---

Definition Index

C

carrier [in monad_def]
Category_mor [in category]
Category_obj [in category]
Category_structure [in category]
Comp_Fmor [in functor]
Comp_Fobj [in functor]

E

Equal_NT [in horcomp]
Equal_NTh [in horcomp]
eq_Functor [in functor]
eq_Functor1 [in functor]
Eq_Monad [in monad_def]
Eq_Monad1 [in monad_def]
eq_NT [in NT]
eq_NTh [in horcomp]
eq_NT1 [in NT]
eta_mu_ax1 [in monad_def]
eta_mu_ax2 [in monad_def]

F

FM [in monad_haskell]
Functor_Fobj [in functor]

H

hcompNT1 [in horcomp]
hidNT1 [in horcomp]
hom_transport [in category]

M

Mmor [in monad_haskell]
MMu [in monad_haskell]
Monad_h_eta [in monad_haskell]
Monad_h_F [in monad_haskell]
Monad_h_kl [in monad_haskell]

N

NTlarge [in horcomp]
NT_trafo [in NT]
NT_type [in horcomp]

P

PI [in functor]
Prod_comp [in prods]
Prod_equiv [in prods]
Prod_equiv1 [in prods]
prod_Fmor [in prods]
prod_Fobj [in prods]
Prod_id [in prods]
Prod_mor [in prods]
Prod_obj [in prods]

S

SET_hom [in cat_SET]
SET_hom_equiv [in cat_SET]
SET_hom_oid [in cat_SET]
subst_ax [in monad_def]

T

tra [in horcomp]
trafo_comm [in NT]

V

vcompNT [in NT]
vcompNT1 [in NT]

---

Variable Index

C

CatFunct.C [in CatFunct]
CatFunct.D [in CatFunct]
CatFunct.morC [in CatFunct]
CatFunct.morD [in CatFunct]
CatFunct.obC [in CatFunct]
CatFunct.obD [in CatFunct]
cat_lemmata.a [in category]
cat_lemmata.b [in category]
cat_lemmata.c [in category]
cat_lemmata.C [in category]
cat_lemmata.d [in category]
cat_lemmata.f [in category]
cat_lemmata.f' [in category]
cat_lemmata.f'' [in category]
cat_lemmata.g [in category]
cat_lemmata.h [in category]
cat_lemmata.hom [in category]
cat_lemmata.ob [in category]
CompF_Morphism.C [in functor]
CompF_Morphism.D [in functor]
CompF_Morphism.E [in functor]
CompF_Morphism.morC [in functor]
CompF_Morphism.morD [in functor]
CompF_Morphism.morE [in functor]
CompF_Morphism.obC [in functor]
CompF_Morphism.obD [in functor]
CompF_Morphism.obE [in functor]
Comp_Functor.C [in functor]
Comp_Functor.D [in functor]
Comp_Functor.E [in functor]
Comp_Functor.F [in functor]
Comp_Functor.G [in functor]
Comp_Functor.morC [in functor]
Comp_Functor.morD [in functor]
Comp_Functor.morE [in functor]
Comp_Functor.obC [in functor]
Comp_Functor.obD [in functor]
Comp_Functor.obE [in functor]

E

endo_monad.C [in smon_cats]
eqFunctor.C [in functor]
eqFunctor.D [in functor]
eqFunctor.morC [in functor]
eqFunctor.morD [in functor]
eqFunctor.obC [in functor]
eqFunctor.obD [in functor]
eqFunctor1.C [in functor]
eqFunctor1.D [in functor]
eqFunctor1.E [in functor]
eqFunctor1.E' [in functor]
eqFunctor1.F [in functor]
eqFunctor1.G [in functor]
eqFunctor1.H [in functor]
eqFunctor1.morC [in functor]
eqFunctor1.morD [in functor]
eqFunctor1.morE [in functor]
eqFunctor1.morE' [in functor]
eqFunctor1.obC [in functor]
eqFunctor1.obD [in functor]
eqFunctor1.obE [in functor]
eqFunctor1.obE' [in functor]
Equal_hom.C [in category]
Equal_hom.hom [in category]
Equal_hom.ob [in category]
Equal_NTh_lemmata.C [in horcomp]
Equal_NTh_lemmata.D [in horcomp]
Equal_NTh_lemmata.morC [in horcomp]
Equal_NTh_lemmata.morD [in horcomp]
Equal_NTh_lemmata.obC [in horcomp]
Equal_NTh_lemmata.obD [in horcomp]
eq_Functor_imp_eq_Fobj.C [in functor]
eq_Functor_imp_eq_Fobj.D [in functor]
eq_Functor_imp_eq_Fobj.F [in functor]
eq_Functor_imp_eq_Fobj.G [in functor]
eq_Functor_imp_eq_Fobj.H [in functor]
eq_Functor_imp_eq_Fobj.morC [in functor]
eq_Functor_imp_eq_Fobj.morD [in functor]
eq_Functor_imp_eq_Fobj.obC [in functor]
eq_Functor_imp_eq_Fobj.obD [in functor]
eq_NTh.alpha [in horcomp]
eq_NTh.beta [in horcomp]
eq_NTh.C [in horcomp]
eq_NTh.D [in horcomp]
eq_NTh.F [in horcomp]
eq_NTh.F' [in horcomp]
eq_NTh.G [in horcomp]
eq_NTh.G' [in horcomp]
eq_NTh.morC [in horcomp]
eq_NTh.morD [in horcomp]
eq_NTh.obC [in horcomp]
eq_NTh.obD [in horcomp]
eq_NTh_lemmata.alpha [in horcomp]
eq_NTh_lemmata.beta [in horcomp]
eq_NTh_lemmata.C [in horcomp]
eq_NTh_lemmata.D [in horcomp]
eq_NTh_lemmata.F [in horcomp]
eq_NTh_lemmata.F' [in horcomp]
eq_NTh_lemmata.F'' [in horcomp]
eq_NTh_lemmata.G [in horcomp]
eq_NTh_lemmata.gamma [in horcomp]
eq_NTh_lemmata.G' [in horcomp]
eq_NTh_lemmata.G'' [in horcomp]
eq_NTh_lemmata.morC [in horcomp]
eq_NTh_lemmata.morD [in horcomp]
eq_NTh_lemmata.obC [in horcomp]
eq_NTh_lemmata.obD [in horcomp]
erightleft.C [in smon_cats]
erightleft.e [in smon_cats]

F

FunctCat_lemmata.alpha [in CatFunct]
FunctCat_lemmata.beta [in CatFunct]
FunctCat_lemmata.C [in CatFunct]
FunctCat_lemmata.D [in CatFunct]
FunctCat_lemmata.F [in CatFunct]
FunctCat_lemmata.G [in CatFunct]
FunctCat_lemmata.h [in CatFunct]
FunctCat_lemmata.H [in CatFunct]
FunctCat_lemmata.h' [in CatFunct]
FunctCat_lemmata.K [in CatFunct]
FunctCat_lemmata.morC [in CatFunct]
FunctCat_lemmata.morD [in CatFunct]
FunctCat_lemmata.obC [in CatFunct]
FunctCat_lemmata.obD [in CatFunct]
Functors.morC [in functor]
Functors.morD [in functor]
Functors.obC [in functor]
Functors.obD [in functor]
Functor_Composition_Morphism.C [in functor]
Functor_Composition_Morphism.D [in functor]
Functor_Composition_Morphism.E [in functor]
Functor_Composition_Morphism.morC [in functor]
Functor_Composition_Morphism.morD [in functor]
Functor_Composition_Morphism.morE [in functor]
Functor_Composition_Morphism.obC [in functor]
Functor_Composition_Morphism.obD [in functor]
Functor_Composition_Morphism.obE [in functor]
Functor_Comp_Id.C [in functor]
Functor_Comp_Id.D [in functor]
Functor_Comp_Id.E [in functor]
Functor_Comp_Id.E' [in functor]
Functor_Comp_Id.F [in functor]
Functor_Comp_Id.G [in functor]
Functor_Comp_Id.H [in functor]
Functor_Comp_Id.morC [in functor]
Functor_Comp_Id.morD [in functor]
Functor_Comp_Id.morE [in functor]
Functor_Comp_Id.morE' [in functor]
Functor_Comp_Id.obC [in functor]
Functor_Comp_Id.obD [in functor]
Functor_Comp_Id.obE [in functor]
Functor_Comp_Id.obE' [in functor]
Functor_equal.C [in functor]
Functor_equal.D [in functor]
Functor_equal.morC [in functor]
Functor_equal.morD [in functor]
Functor_equal.obC [in functor]
Functor_equal.obD [in functor]
Functor_lemmata.a [in functor]
Functor_lemmata.b [in functor]
Functor_lemmata.c [in functor]
Functor_lemmata.C [in functor]
Functor_lemmata.D [in functor]
Functor_lemmata.f [in functor]
Functor_lemmata.F [in functor]
Functor_lemmata.g [in functor]
Functor_lemmata.morC [in functor]
Functor_lemmata.morD [in functor]
Functor_lemmata.obC [in functor]
Functor_lemmata.obD [in functor]

H

hcomp.A [in horcomp]
hcomp.alpha [in horcomp]
hcomp.B [in horcomp]
hcomp.beta [in horcomp]
hcomp.C [in horcomp]
hcomp.F [in horcomp]
hcomp.F' [in horcomp]
hcomp.G [in horcomp]
hcomp.G' [in horcomp]
hcomp.morA [in horcomp]
hcomp.morB [in horcomp]
hcomp.morC [in horcomp]
hcomp.obA [in horcomp]
hcomp.obB [in horcomp]
hcomp.obC [in horcomp]
hidNT.C [in horcomp]
hidNT.morC [in horcomp]
hidNT.obC [in horcomp]
hidNT_unit.alpha [in horcomp]
hidNT_unit.C [in horcomp]
hidNT_unit.D [in horcomp]
hidNT_unit.F [in horcomp]
hidNT_unit.G [in horcomp]
hidNT_unit.morC [in horcomp]
hidNT_unit.morD [in horcomp]
hidNT_unit.obC [in horcomp]
hidNT_unit.obD [in horcomp]
hor_comp.alpha [in horcomp]
hor_comp.C [in horcomp]
hor_comp.D [in horcomp]
hor_comp.F [in horcomp]
hor_comp.G [in horcomp]
hor_comp.morC [in horcomp]
hor_comp.morD [in horcomp]
hor_comp.obC [in horcomp]
hor_comp.obD [in horcomp]

I

Id_Functor.C [in functor]
Id_Functor.mor [in functor]
Id_Functor.ob [in functor]

M

monads.C [in smon_cats]
monad_def.C [in monad_def]
monad_def.morC [in monad_def]
monad_def.obC [in monad_def]
monad_def.obD [in monad_def]
Monad_gives_Monad_h.C [in monad_haskell]
Monad_gives_Monad_h.M [in monad_haskell]
Monad_gives_Monad_h.mor [in monad_haskell]
Monad_gives_Monad_h.ob [in monad_haskell]
monad_haskell_def.C [in monad_haskell]
monad_haskell_def.monad_haskell_class.eta [in monad_haskell]
monad_haskell_def.monad_haskell_class.F [in monad_haskell]
monad_haskell_def.monad_haskell_class.kleisli [in monad_haskell]
monad_haskell_def.mor [in monad_haskell]
monad_haskell_def.ob [in monad_haskell]
Monad_h_gives_Monad.C [in monad_haskell]
Monad_h_gives_Monad.M [in monad_haskell]
Monad_h_gives_Monad.mor [in monad_haskell]
Monad_h_gives_Monad.ob [in monad_haskell]

N

NTlarge.C [in horcomp]
NTlarge.D [in horcomp]
NTlarge.morC [in horcomp]
NTlarge.morD [in horcomp]
NTlarge.obC [in horcomp]
NTlarge.obD [in horcomp]
NT_def.C [in NT]
NT_def.D [in NT]
NT_def.F [in NT]
NT_def.G [in NT]
NT_def.morC [in NT]
NT_def.morD [in NT]
NT_def.obC [in NT]
NT_def.obD [in NT]

P

PROD_almost_assoc.A [in smon_cats]
PROD_almost_assoc.B [in smon_cats]
PROD_almost_assoc.C [in smon_cats]
prod_cat.C [in prods]
prod_cat.D [in prods]
prod_func.C [in prods]
prod_func.C' [in prods]
prod_func.D [in prods]
prod_func.D' [in prods]
prod_func.F [in prods]
prod_func.G [in prods]

S

SET.SET_data.A [in cat_SET]
SET.SET_data.B [in cat_SET]

T

transport.C [in category]
transport.Equal_hom_lemmata.a [in category]
transport.Equal_hom_lemmata.b [in category]
transport.Equal_hom_lemmata.c [in category]
transport.Equal_hom_lemmata.d [in category]
transport.Equal_hom_lemmata.f [in category]
transport.Equal_hom_lemmata.g [in category]
transport.Equal_hom_lemmata.H [in category]
transport.hom [in category]
transport.ob [in category]

V

vcompNT.a [in NT]
vcompNT.b [in NT]
vcompNT.C [in NT]
vcompNT.D [in NT]
vcompNT.F [in NT]
vcompNT.G [in NT]
vcompNT.H [in NT]
vcompNT.morC [in NT]
vcompNT.morD [in NT]
vcompNT.obC [in NT]
vcompNT.obD [in NT]
VIDNT.C [in NT]
VIDNT.D [in NT]
VIDNT.F [in NT]
VIDNT.morC [in NT]
VIDNT.morD [in NT]
VIDNT.obC [in NT]
VIDNT.obD [in NT]

---

Library Index

C

category
CatFunct
cat_SET

F

functor

H

horcomp

M

monad_def
monad_haskell

N

NT

P

prods

S

smon_cats

---

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(499 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(22 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(37 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(9 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(41 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(51 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(47 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(280 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(10 entries)

---

This page has been generated by coqdoc