| 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 | _ | (1216 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 | _ | (31 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 | _ | (95 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 | _ | (29 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 | _ | (175 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 | _ | (99 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 | _ | (69 entries) |
| 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 | _ | (18 entries) |
| 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 | _ | (184 entries) |
| Moduleid 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) |
| 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 | _ | (486 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 | _ | (29 entries) |
Global Index
A
Alpha [projection, in mon_cats]alpha_set [definition, in mon_cats]
alpha_SET [definition, in mon_cats]
alpha_set_NISO [instance, in mon_cats]
arrow [constructor, in pcf]
arrow [constructor, in pcfpo]
assoc [lemma, in category]
Assoc [projection, in category]
assoc2 [lemma, in category]
B
betaS_App1 [lemma, in pcfpo]betaS_App2 [lemma, in pcfpo]
betaS_Lam [lemma, in pcfpo]
betaS_Rec [lemma, in pcfpo]
Bifunctor [definition, in bifunctor]
bifunctor [library]
bifunctor_def [section, in bifunctor]
bifunctor_def.B [variable, in bifunctor]
bifunctor_def.C [variable, in bifunctor]
bifunctor_def.D [variable, in bifunctor]
bifunctor_def.Left_Functor [section, in bifunctor]
bifunctor_def.Left_Functor.c [variable, in bifunctor]
bifunctor_def.morB [variable, in bifunctor]
bifunctor_def.morC [variable, in bifunctor]
bifunctor_def.morD [variable, in bifunctor]
bifunctor_def.obB [variable, in bifunctor]
bifunctor_def.obC [variable, in bifunctor]
bifunctor_def.obD [variable, in bifunctor]
bifunctor_def.Right_Functor [section, in bifunctor]
bifunctor_def.Right_Functor.b [variable, in bifunctor]
bifunctor_def.S [variable, in bifunctor]
bla [section, in pcfpo]
bla [section, in mon_cats]
Bool [constructor, in pcf]
Bool [constructor, in pcfpo]
Bottom [constructor, in pcfpo]
Bottom [constructor, in pcf]
break_Sig_Prop [lemma, in my_lib]
break_Sig_Prop2 [lemma, in my_lib]
Build_Equal_hom [constructor, in category]
build_prod_mor [definition, in prods]
build_prod_obj [definition, in prods]
C
Cat [record, in category]cat [projection, in smon_cats]
Category [record, in category]
category [library]
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]
cats_lemmata [library]
Cat_Coprod [record, in coproduct]
Cat_from_SmallCat [instance, in small_cat]
cat_INDEXED_TYPE [library]
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_of_R_LModules_over_D [section, in monad_morphism]
cat_of_R_LModules_over_D.C [variable, in monad_morphism]
cat_of_R_LModules_over_D.D [variable, in monad_morphism]
cat_of_R_LModules_over_D.morC [variable, in monad_morphism]
cat_of_R_LModules_over_D.morD [variable, in monad_morphism]
cat_of_R_LModules_over_D.obC [variable, in monad_morphism]
cat_of_R_LModules_over_D.obD [variable, in monad_morphism]
cat_of_R_LModules_over_D.R [variable, in monad_morphism]
Cat_Prod [record, in product]
cat_SET [library]
Cat_struct [projection, in category]
cat_TYPE [library]
cccomp [definition, in monad_morphism]
cccomp_trans [definition, in monad_morphism]
clos_rt_1n [section, in orders]
clos_rt_1n.A [variable, in orders]
clos_rt_1n.R [variable, in orders]
Clos_RT_1n_prf [instance, in orders]
comp [projection, in category]
CompF [definition, 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_order_preserve [lemma, in orders]
Comp_preserve_comp [lemma, in functor]
Comp_preserve_ident [lemma, in functor]
comp_tensor [definition, in smon_cats]
condB [constructor, in pcfpo]
condB [constructor, in pcf]
condN [constructor, in pcfpo]
condN [constructor, in pcf]
Const [constructor, in pcfpo]
Const [constructor, in pcf]
coprod [projection, in coproduct]
coprod [section, in coproduct]
coproduct [library]
coprod.morC [variable, in coproduct]
coprod.obC [variable, in coproduct]
coprod_bifunctor [section, in coproduct]
coprod_bifunctor.C [variable, in coproduct]
coprod_bifunctor.GENERIC_OPT [section, in coproduct]
coprod_bifunctor.GENERIC_OPT.obC [variable, in coproduct]
coprod_bifunctor.H [variable, in coproduct]
coprod_bifunctor.morC [variable, in coproduct]
coprod_bifunctor.obC [variable, in coproduct]
COPROD_BIF_mor [definition, in coproduct]
COPROD_BIF_obj [definition, in coproduct]
coprod_diag [projection, in coproduct]
coprod_mor [projection, in coproduct]
coprod_mor_unique [projection, in coproduct]
D
dist [projection, in monad_haskell]E
e [projection, in smon_cats]eleft [definition, in smon_cats]
eleft_unit [projection, in smon_cats]
Empty [inductive, in cat_SET]
endo_monad [section, in smon_cats]
endo_monad.C [variable, in smon_cats]
endo_monad.morC [variable, in smon_cats]
endo_monad.obC [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 [section, in category]
Equal_hom [inductive, 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 [section, in functor]
eq_Functor_imp_eq_Fobj [lemma, 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_INDEXED_TYPE_mor [definition, in cat_INDEXED_TYPE]
eq_ind_po [definition, in ind_potype]
eq_ind_setoid [lemma, in ind_potype]
eq_lam_rho [definition, in mon_cats]
eq_l_r [projection, in mon_cats]
eq_MOD_R [definition, in monad_morphism]
eq_MOD_R_mor [definition, in monad_morphism]
eq_MOD_R_setoid [lemma, in monad_morphism]
Eq_Monad [definition, in monad_def]
Eq_Monad1 [definition, in monad_def]
eq_MONAD_mor1 [definition, in monad_morphism]
Eq_Monad_oid [lemma, in monad_def]
eq_NT [definition, in NT]
eq_NTh [definition, in horcomp]
eq_NTh [section, 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]
eq_NT_refl [lemma, in NT]
eq_NT_sym [lemma, in NT]
eq_NT_trans [lemma, in NT]
eq_PreOrder [definition, in orders]
eq_PreOrder_equiv [lemma, in orders]
eright [definition, in smon_cats]
erightleft [section, in smon_cats]
erightleft.C [variable, in smon_cats]
erightleft.e [variable, in smon_cats]
erightleft.morC [variable, in smon_cats]
erightleft.obC [variable, in smon_cats]
eright_unit [projection, in smon_cats]
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]
eta_no_choice [lemma, in monad_def]
eta_tau [lemma, in monad_morphism]
Eta_Tau [projection, in monad_morphism]
eta_tau_def [definition, in monad_morphism]
F
F [projection, in monad_haskell]FComp [lemma, in functor]
ff [constructor, in pcf]
ff [constructor, in pcfpo]
FId [lemma, in functor]
FINJ [definition, in subcategories]
Fmor [projection, in functor]
Fobj [projection, in functor]
Func [record, in functor]
FunctCat [definition, 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.C [variable, in functor]
Functors.D [variable, 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_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]
Func_struct [projection, in functor]
G
gr [lemma, in CatFunct]H
hcomp [section, in horcomp]hcompNT [definition, 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 [definition, in horcomp]
hidNT [section, 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
I [projection, in mon_cats]id [projection, in category]
Id [definition, in functor]
IdFl [lemma, in functor]
IdFr [lemma, in functor]
IdF_unit_l [lemma, in functor]
IdF_unit_r [lemma, in functor]
idl [lemma, in category]
idl2 [lemma, in category]
idr [lemma, in category]
idr2 [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_order_preserve [lemma, in orders]
id_r [projection, in category]
INDEXED_TYPE [instance, in cat_INDEXED_TYPE]
indexed_types [section, in cat_INDEXED_TYPE]
indexed_types.T [variable, in cat_INDEXED_TYPE]
INDEXED_TYPE_comp [definition, in cat_INDEXED_TYPE]
INDEXED_TYPE_equiv [lemma, in cat_INDEXED_TYPE]
INDEXED_TYPE_id [definition, in cat_INDEXED_TYPE]
INDEXED_TYPE_mor [definition, in cat_INDEXED_TYPE]
INDEXED_TYPE_obj [definition, in cat_INDEXED_TYPE]
INDEXED_TYPE_oid [definition, in cat_INDEXED_TYPE]
ind_potype [library]
ind_po_cat [section, in ind_potype]
ind_po_cat.T [variable, in ind_potype]
ind_po_comp [definition, in ind_potype]
ind_po_id [definition, in ind_potype]
ind_po_mor [definition, in ind_potype]
ind_po_obj [definition, in ind_potype]
ind_po_obj_car [definition, in ind_potype]
ind_po_oid [definition, in ind_potype]
IND_PO_struct [instance, in ind_potype]
Init [projection, in initial_terminal]
Initial [record, in initial_terminal]
initial [definition, in initial_terminal]
Initial_Terminal [section, in initial_terminal]
initial_terminal [library]
Initial_Terminal.morC [variable, in initial_terminal]
Initial_Terminal.obC [variable, in initial_terminal]
InitMor [projection, in initial_terminal]
InitMorUnique [projection, in initial_terminal]
Injection_Functor [section, in subcategories]
Injection_Functor.C [variable, in subcategories]
Injection_Functor.mor [variable, in subcategories]
Injection_Functor.ob [variable, in subcategories]
Injection_Functor.SC [variable, in subcategories]
Injection_Functor.submorP [variable, in subcategories]
Injection_Functor.subobP [variable, in subcategories]
inl [projection, in coproduct]
inl_coprod [lemma, in coproduct]
inr [projection, in coproduct]
inr_coprod [lemma, in coproduct]
inv [projection, in nat_iso]
inv_left [projection, in nat_iso]
inv_right [projection, in nat_iso]
iso [definition, in smon_cats]
I_set [definition, in mon_cats]
K
kleisli [projection, in monad_haskell]kleisli_oid [projection, in monad_haskell]
kl_eta [projection, in monad_haskell]
L
Lambda [projection, in mon_cats]lambda_SET [definition, in mon_cats]
lambda_set [definition, in mon_cats]
lambda_set_NISO [instance, in mon_cats]
lam_rho [projection, in mon_cats]
lam_rho_dia [definition, in mon_cats]
Left_Functor [definition, in bifunctor]
Left_Functor_struct [instance, in bifunctor]
LModule [record, in monad_morphism]
LmoduleF [projection, in monad_morphism]
lmoduleNT [projection, in monad_morphism]
LModule_def [section, in monad_morphism]
LModule_def.C [variable, in monad_morphism]
LModule_def.D [variable, in monad_morphism]
LModule_def.LModule_lemmata [section, in monad_morphism]
LModule_def.LModule_lemmata.M [variable, in monad_morphism]
LModule_def.morC [variable, in monad_morphism]
LModule_def.morD [variable, in monad_morphism]
LModule_def.obC [variable, in monad_morphism]
LModule_def.obD [variable, in monad_morphism]
LModule_def.R [variable, in monad_morphism]
LModule_Morphism [section, in monad_morphism]
LModule_Morphism.C [variable, in monad_morphism]
LModule_Morphism.D [variable, in monad_morphism]
LModule_Morphism.LModule_Morphism_struct [section, in monad_morphism]
LModule_Morphism.LModule_Morphism_struct.F [variable, in monad_morphism]
LModule_Morphism.M [variable, in monad_morphism]
LModule_Morphism.morC [variable, in monad_morphism]
LModule_Morphism.morD [variable, in monad_morphism]
LModule_Morphism.N [variable, in monad_morphism]
LModule_Morphism.obC [variable, in monad_morphism]
LModule_Morphism.obD [variable, in monad_morphism]
LModule_Morphism.R [variable, in monad_morphism]
lmodule_morphism_struct [projection, in monad_morphism]
LModule_struct [record, in monad_morphism]
Lmodule_struct [projection, in monad_morphism]
LMOD_R_ob [definition, in monad_morphism]
M
MEta [definition, in monad_haskell]MEtatrafo [definition, in monad_haskell]
MFunc [definition, in monad_haskell]
Mmor [definition, in monad_haskell]
MMu [definition, in monad_haskell]
MMutrafo [definition, in monad_haskell]
module_diag [projection, in monad_morphism]
Module_Mor [projection, in monad_morphism]
Module_Morphism [record, in monad_morphism]
Module_Morphism_struct [record, in monad_morphism]
MOD_R [instance, in monad_morphism]
MOD_R_comp [definition, in monad_morphism]
MOD_R_id [definition, in monad_morphism]
MOD_R_mor [definition, in monad_morphism]
mod_subst [lemma, in monad_morphism]
Monad [record, in monad_def]
MONAD [instance, in monad_morphism]
MONAD [section, in monad_morphism]
monads [section, in smon_cats]
monads [instance, in smon_cats]
monads.C [variable, in smon_cats]
monads.morC [variable, in smon_cats]
monads.obC [variable, in smon_cats]
MONAD.C [variable, in monad_morphism]
MONAD.morC [variable, in monad_morphism]
MONAD.obC [variable, in monad_morphism]
MONAD_comp [definition, in monad_morphism]
monad_comp [section, in monad_def]
monad_comp.C [variable, in monad_def]
monad_comp.etaF [variable, in monad_def]
monad_comp.etaG [variable, in monad_def]
monad_comp.F [variable, in monad_def]
monad_comp.G [variable, in monad_def]
monad_comp.MonadF [variable, in monad_def]
monad_comp.MonadG [variable, in monad_def]
monad_comp.mor [variable, in monad_def]
monad_comp.muF [variable, in monad_def]
monad_comp.muG [variable, in monad_def]
monad_comp.ob [variable, in monad_def]
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.morC [variable, in monad_haskell]
Monad_gives_Monad_h.obC [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.F [variable, in monad_haskell]
monad_haskell_def.morC [variable, in monad_haskell]
monad_haskell_def.obC [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.morC [variable, in monad_haskell]
Monad_h_gives_Monad.obC [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_id [definition, in monad_morphism]
MONAD_mor [definition, in monad_morphism]
Monad_Morphism [record, in monad_morphism]
monad_morphism [library]
monad_morphism_def [section, in monad_morphism]
monad_morphism_def.C [variable, in monad_morphism]
monad_morphism_def.F [variable, in monad_morphism]
monad_morphism_def.G [variable, in monad_morphism]
monad_morphism_def.Monad_Morphism_lemmata [section, in monad_morphism]
monad_morphism_def.Monad_Morphism_lemmata.Tau [variable, in monad_morphism]
monad_morphism_def.morC [variable, in monad_morphism]
monad_morphism_def.obC [variable, in monad_morphism]
MONAD_mor_oid [definition, in monad_morphism]
MONAD_mor_setoid [lemma, in monad_morphism]
MONAD_obj [definition, in monad_morphism]
Monad_struct [record, in monad_def]
monad_struct [projection, in monad_def]
monoidal_cat_def [section, in mon_cats]
monoidal_cat_def.C [variable, in mon_cats]
monoidal_cat_def.Diagram_def [section, in mon_cats]
monoidal_cat_def.Diagram_def.Alpha [variable, in mon_cats]
monoidal_cat_def.Diagram_def.I [variable, in mon_cats]
monoidal_cat_def.Diagram_def.Lambda [variable, in mon_cats]
monoidal_cat_def.Diagram_def.Rho [variable, in mon_cats]
monoidal_cat_def.Diagram_def.tens [variable, in mon_cats]
monoidal_cat_def.morC [variable, in mon_cats]
monoidal_cat_def.obC [variable, in mon_cats]
mon_cat [record, in mon_cats]
mon_cats [library]
mor [projection, in category]
mor_oid [projection, in category]
mu [projection, in monad_def]
mu_tau [lemma, in monad_morphism]
Mu_Tau [projection, in monad_morphism]
mu_tau2 [lemma, in monad_morphism]
mu_tau_def [definition, in monad_morphism]
my_lib [library]
N
Nat [constructor, in pcf]Nat [constructor, in pcfpo]
Nats [constructor, in pcfpo]
Nats [constructor, in pcf]
NatTrans [record, in NT]
NatTrans_struct [projection, in NT]
nat_iso [library]
Nat_Iso_def [section, in nat_iso]
Nat_Iso_def.C [variable, in nat_iso]
Nat_Iso_def.D [variable, in nat_iso]
Nat_Iso_def.F [variable, in nat_iso]
Nat_Iso_def.G [variable, in nat_iso]
Nat_Iso_def.morC [variable, in nat_iso]
Nat_Iso_def.morD [variable, in nat_iso]
Nat_Iso_def.obC [variable, in nat_iso]
Nat_Iso_def.obD [variable, in nat_iso]
Nat_Iso_def.struct_def [section, in nat_iso]
Nat_Iso_def.struct_def.alpha [variable, in nat_iso]
Nat_Iso_gives_NT [section, in nat_iso]
Nat_Iso_gives_NT.alpha [variable, in nat_iso]
Nat_Iso_gives_NT.C [variable, in nat_iso]
Nat_Iso_gives_NT.D [variable, in nat_iso]
Nat_Iso_gives_NT.F [variable, in nat_iso]
Nat_Iso_gives_NT.G [variable, in nat_iso]
Nat_Iso_gives_NT.morC [variable, in nat_iso]
Nat_Iso_gives_NT.morD [variable, in nat_iso]
Nat_Iso_gives_NT.obC [variable, in nat_iso]
Nat_Iso_gives_NT.obD [variable, in nat_iso]
NISO [record, in nat_iso]
niso_struct [projection, in nat_iso]
NISO_struct [record, in nat_iso]
None_T [constructor, in cat_INDEXED_TYPE]
None_TP [constructor, in ind_potype]
no_choice [lemma, in horcomp]
NT [record, in NT]
NT [library]
NTcomm [lemma, in NT]
NTinv [definition, in nat_iso]
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_from_MM [definition, in monad_morphism]
NT_type [definition, in horcomp]
O
obj [projection, in category]optrelTP [inductive, in ind_potype]
optrelTP_none [constructor, in ind_potype]
optrelTP_some [constructor, in ind_potype]
opt_incl [definition, in cat_INDEXED_TYPE]
opt_T [section, in cat_INDEXED_TYPE]
opt_T [inductive, in cat_INDEXED_TYPE]
opt_TP [definition, in ind_potype]
opt_TPd [inductive, in ind_potype]
opt_TP_Func [instance, in ind_potype]
opt_TP_map [definition, in ind_potype]
opt_TP_mapd [definition, in ind_potype]
opt_TP_map_comp [lemma, in ind_potype]
opt_TP_map_extens [lemma, in ind_potype]
opt_TP_map_id [lemma, in ind_potype]
opt_TP_preorder [lemma, in ind_potype]
opt_T.T [variable, in cat_INDEXED_TYPE]
opt_T_Functor [definition, in cat_INDEXED_TYPE]
opt_T_map [definition, in cat_INDEXED_TYPE]
opt_T_map_comp [lemma, in cat_INDEXED_TYPE]
opt_T_map_extens [lemma, in cat_INDEXED_TYPE]
opt_T_map_id [lemma, in cat_INDEXED_TYPE]
orders [library]
P
PApp [constructor, in pcfpo]PApp [constructor, in pcf]
par_prodF [definition, in prods]
PCF [moduleid, in pcfpo_mod]
PCF [inductive, in pcfpo]
PCF [inductive, in pcf]
pcf [library]
PCFbeta [definition, in pcfpo]
PCFBETA [definition, in pcfpo]
PCFbetaS [definition, in pcfpo]
PCFbeta_beta [constructor, in pcfpo]
PCFbeta_var [constructor, in pcfpo]
pcfo_syntax [section, in pcfpo]
pcfpo [library]
pcfpo_mod [library]
PCFPO_monad_h [instance, in pcfpo_mod]
PCFrelorig [constructor, in pcfpo]
PCFrelPApp1 [constructor, in pcfpo]
PCFrelPApp2 [constructor, in pcfpo]
PCFrelPLam [constructor, in pcfpo]
PCFrelPRec [constructor, in pcfpo]
PCFrelpropag [inductive, in pcfpo]
PCFVar [constructor, in pcf]
PCFVAR [definition, in pcfpo]
PCFVar [constructor, in pcfpo]
PCF.App [constructor, in pcfpo_mod]
PCF.arrow [constructor, in pcfpo_mod]
PCF.beta [definition, in pcfpo_mod]
PCF.BETA [definition, in pcfpo_mod]
PCF.betaS [definition, in pcfpo_mod]
PCF.beta_ [inductive, in pcfpo_mod]
PCF.beta_beta [constructor, in pcfpo_mod]
PCF.Beta_Relation [section, in pcfpo_mod]
PCF.beta_var [constructor, in pcfpo_mod]
PCF.Bool [constructor, in pcfpo_mod]
PCF.Bottom [constructor, in pcfpo_mod]
PCF.clos [lemma, in pcfpo_mod]
PCF.Compat_with_Beta [section, in pcfpo_mod]
PCF.Compat_with_Beta.inj [section, in pcfpo_mod]
PCF.Compat_with_Beta.rename [section, in pcfpo_mod]
PCF.Compat_with_Beta.rename.rename_bs [section, in pcfpo_mod]
PCF.Compat_with_Beta.rename.rename_bs.rel [variable, in pcfpo_mod]
PCF.Compat_with_Beta.shift [section, in pcfpo_mod]
PCF.Compat_with_Beta.shift.shift_bs [section, in pcfpo_mod]
PCF.Compat_with_Beta.shift.shift_bs.rel [variable, in pcfpo_mod]
PCF.Compat_with_Beta.shift.u [variable, in pcfpo_mod]
PCF.Compat_with_Beta.subst [section, in pcfpo_mod]
PCF.Compat_with_Beta.subst.subst_bs [section, in pcfpo_mod]
PCF.Compat_with_Beta.subst.subst_bs.rel [variable, in pcfpo_mod]
PCF.condB [constructor, in pcfpo_mod]
PCF.condN [constructor, in pcfpo_mod]
PCF.Const [constructor, in pcfpo_mod]
PCF.Consts [inductive, in pcfpo_mod]
PCF.cp_App1 [lemma, in pcfpo_mod]
PCF.cp_App2 [lemma, in pcfpo_mod]
PCF.cp_Lam [lemma, in pcfpo_mod]
PCF.cp_Rec [lemma, in pcfpo_mod]
PCF.ff [constructor, in pcfpo_mod]
PCF.Fusion_Laws [section, in pcfpo_mod]
PCF.inj [definition, in pcfpo_mod]
PCF.inj_ [definition, in pcfpo_mod]
PCF.ipo [definition, in pcfpo_mod]
PCF.Lam [constructor, in pcfpo_mod]
PCF.Nat [constructor, in pcfpo_mod]
PCF.Nats [constructor, in pcfpo_mod]
PCF.PCF [inductive, in pcfpo_mod]
PCF.PCFrel [definition, in pcfpo_mod]
PCF.propag [inductive, in pcfpo_mod]
PCF.propag_clos_propag_clos [lemma, in pcfpo_mod]
PCF.Rec [constructor, in pcfpo_mod]
PCF.relApp1 [constructor, in pcfpo_mod]
PCF.relApp2 [constructor, in pcfpo_mod]
PCF.Relations_on_PCF [section, in pcfpo_mod]
PCF.Relations_on_PCF.rel [variable, in pcfpo_mod]
PCF.relLam [constructor, in pcfpo_mod]
PCF.relorig [constructor, in pcfpo_mod]
PCF.relRec [constructor, in pcfpo_mod]
PCF.rename [definition, in pcfpo_mod]
PCF.rename_ [definition, in pcfpo_mod]
PCF.rename_beta [lemma, in pcfpo_mod]
PCF.rename_comp [lemma, in pcfpo_mod]
PCF.rename_eq [lemma, in pcfpo_mod]
PCF.rename_id [lemma, in pcfpo_mod]
PCF.rename_propag [lemma, in pcfpo_mod]
PCF.rename_rt_clos [lemma, in pcfpo_mod]
PCF.rename_subst [lemma, in pcfpo_mod]
PCF.rename_substar [lemma, in pcfpo_mod]
PCF.rename_term_inj [lemma, in pcfpo_mod]
PCF.shift [definition, in pcfpo_mod]
PCF.shift_ [definition, in pcfpo_mod]
PCF.shift_eq [lemma, in pcfpo_mod]
PCF.shift_lift [lemma, in pcfpo_mod]
PCF.shift_propag [lemma, in pcfpo_mod]
PCF.shift_rt_clos [lemma, in pcfpo_mod]
PCF.shift_var [lemma, in pcfpo_mod]
PCF.subst [definition, in pcfpo_mod]
PCF.substar [definition, in pcfpo_mod]
PCF.subst_ [definition, in pcfpo_mod]
PCF.subst_eq [lemma, in pcfpo_mod]
PCF.subst_eq_rename [lemma, in pcfpo_mod]
PCF.subst_propag [lemma, in pcfpo_mod]
PCF.subst_rename [lemma, in pcfpo_mod]
PCF.subst_rt_clos [lemma, in pcfpo_mod]
PCF.subst_shift_shift [lemma, in pcfpo_mod]
PCF.subst_subst [lemma, in pcfpo_mod]
PCF.subst_substar [lemma, in pcfpo_mod]
PCF.subst_term_inj [lemma, in pcfpo_mod]
PCF.subst_var [lemma, in pcfpo_mod]
PCF.succ [constructor, in pcfpo_mod]
PCF.tt [constructor, in pcfpo_mod]
PCF.TY [inductive, in pcfpo_mod]
PCF.VAR [definition, in pcfpo_mod]
PCF.Var [constructor, in pcfpo_mod]
PCF.varmap [definition, in pcfpo_mod]
PCF.var_lift_shift_eq [lemma, in pcfpo_mod]
PCF.zero [constructor, in pcfpo_mod]
PCF_beta [inductive, in pcfpo]
PCF_clos [lemma, in pcfpo]
PCF_consts [inductive, in pcf]
PCF_consts [inductive, in pcfpo]
PCF_inj [definition, in pcf]
PCF_inj [definition, in pcfpo]
PCF_inj_ [definition, in pcfpo]
PCF_rename [definition, in pcfpo]
PCF_rename [definition, in pcf]
PCF_rename_ [definition, in pcfpo]
PCF_rename_beta [lemma, in pcfpo]
PCF_rename_comp [lemma, in pcfpo]
PCF_rename_comp [lemma, in pcf]
PCF_rename_eq [lemma, in pcf]
PCF_rename_eq [lemma, in pcfpo]
PCF_rename_id [lemma, in pcfpo]
PCF_rename_id [lemma, in pcf]
PCF_rename_propag [lemma, in pcfpo]
PCF_rename_rt_clos [lemma, in pcfpo]
PCF_rename_subst [lemma, in pcf]
PCF_rename_subst [lemma, in pcfpo]
PCF_rename_substar [lemma, in pcfpo]
PCF_rename_term_inj [lemma, in pcf]
PCF_rename_term_inj [lemma, in pcfpo]
PCF_shift [definition, in pcfpo]
PCF_shift [definition, in pcf]
PCF_shift2 [definition, in pcf]
PCF_shift_ [definition, in pcfpo]
PCF_shift_eq [lemma, in pcf]
PCF_shift_eq [lemma, in pcfpo]
PCF_shift_lift [lemma, in pcf]
PCF_shift_lift [lemma, in pcfpo]
PCF_shift_propag [lemma, in pcfpo]
PCF_shift_rt_clos [lemma, in pcfpo]
PCF_shift_var [lemma, in pcfpo]
PCF_shift_var [lemma, in pcf]
PCF_subst [definition, in pcfpo]
PCF_subst [definition, in pcf]
PCF_substar [definition, in pcf]
PCF_substar [definition, in pcfpo]
PCF_subst_ [definition, in pcfpo]
PCF_subst_eq [lemma, in pcfpo]
PCF_subst_eq [lemma, in pcf]
PCF_subst_eq_rename [lemma, in pcfpo]
PCF_subst_eq_rename [lemma, in pcf]
PCF_subst_propag [lemma, in pcfpo]
PCF_subst_rename [lemma, in pcfpo]
PCF_subst_rename [lemma, in pcf]
PCF_subst_rt_clos [lemma, in pcfpo]
PCF_subst_shift_shift [lemma, in pcfpo]
PCF_subst_shift_shift [lemma, in pcf]
PCF_subst_subst [lemma, in pcfpo]
PCF_subst_subst [lemma, in pcf]
PCF_subst_substar [lemma, in pcfpo]
PCF_subst_term_inj [lemma, in pcf]
PCF_subst_term_inj [lemma, in pcfpo]
PCF_subst_var [lemma, in pcfpo]
PCF_subst_var [lemma, in pcf]
pcf_syntax [section, in pcf]
PCF_varmap [definition, in pcf]
PCF_varmap [definition, in pcfpo]
PCF_var_lift_shift_eq [lemma, in pcf]
PCF_var_lift_shift_eq [lemma, in pcfpo]
penta_diag [definition, in mon_cats]
PI [definition, in functor]
PI [definition, in my_lib]
PLam [constructor, in pcf]
PLam [constructor, in pcfpo]
POCarrier [projection, in orders]
postcomp [lemma, in cats_lemmata]
POTYPE [instance, in orders]
PO_fun [projection, in orders]
PO_prop [projection, in orders]
praecomp [lemma, in cats_lemmata]
prae_post_comp [section, in cats_lemmata]
prae_post_comp.C [variable, in cats_lemmata]
prae_post_comp.mor [variable, in cats_lemmata]
prae_post_comp.ob [variable, in cats_lemmata]
PRec [constructor, in pcf]
PRec [constructor, in pcfpo]
PreOrderPrf [projection, in orders]
PreOrderRel [projection, in orders]
PreOrder_comp [definition, in orders]
PreOrder_comp [section, in orders]
PreOrder_comp.A [variable, in orders]
PreOrder_comp.B [variable, in orders]
PreOrder_comp.C [variable, in orders]
PreOrder_comp.f [variable, in orders]
PreOrder_comp.g [variable, in orders]
PreOrder_id [definition, in orders]
PreOrder_mor [record, in orders]
PreOrder_obj [record, in orders]
PreOrder_oid [definition, in orders]
preserve_comp [projection, in functor]
preserve_ident [projection, in functor]
prl [projection, in product]
PROD [definition, in prods]
prod [section, in product]
prods [library]
product [projection, in product]
product [library]
Product_LModule [section, in monad_morphism]
Product_LModule.C [variable, in monad_morphism]
Product_LModule.M [variable, in monad_morphism]
Product_LModule.morC [variable, in monad_morphism]
Product_LModule.N [variable, in monad_morphism]
Product_LModule.obC [variable, in monad_morphism]
Product_LModule.R [variable, in monad_morphism]
prod.morC [variable, in product]
prod.obC [variable, in product]
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_almost_assoc.morA [variable, in smon_cats]
PROD_almost_assoc.morB [variable, in smon_cats]
PROD_almost_assoc.morC [variable, in smon_cats]
PROD_almost_assoc.obA [variable, in smon_cats]
PROD_almost_assoc.obB [variable, in smon_cats]
PROD_almost_assoc.obC [variable, in smon_cats]
PROD_BIF [definition, in coproduct]
PROD_BIF [definition, in product]
prod_bifunctor [section, in product]
prod_bifunctor.C [variable, in product]
prod_bifunctor.H [variable, in product]
prod_bifunctor.morC [variable, in product]
prod_bifunctor.obC [variable, in product]
PROD_BIF_mor [definition, in product]
PROD_BIF_obj [definition, in product]
prod_cat [section, in prods]
prod_cat.B [variable, in prods]
prod_cat.C [variable, in prods]
prod_cat.D [variable, in prods]
prod_cat.morB [variable, in prods]
prod_cat.morC [variable, in prods]
prod_cat.morD [variable, in prods]
prod_cat.obB [variable, in prods]
prod_cat.obC [variable, in prods]
prod_cat.obD [variable, in prods]
prod_cat.S [variable, in prods]
Prod_comp [definition, in prods]
prod_diag [projection, in product]
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 [definition, 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_func.morC [variable, in prods]
prod_func.morC' [variable, in prods]
prod_func.morD [variable, in prods]
prod_func.morD' [variable, in prods]
prod_func.obC [variable, in prods]
prod_func.obC' [variable, in prods]
prod_func.obD [variable, in prods]
prod_func.obD' [variable, in prods]
Prod_id [definition, in prods]
PROD_MODULE [instance, in monad_morphism]
Prod_mor [definition, in prods]
prod_mor [projection, in product]
prod_mor_equal [lemma, in prods]
prod_mor_equal_l [lemma, in prods]
prod_mor_equal_r [lemma, in prods]
prod_mor_unique [projection, in product]
Prod_NT [definition, in monad_morphism]
Prod_obj [definition, in prods]
prod_prl [lemma, in product]
prod_prr [lemma, in product]
prod_set [record, in mon_cats]
PROD_struct [instance, in prods]
propag_clos_propag_clos [lemma, in pcfpo]
prr [projection, in product]
pts [library]
Pullback_Module [definition, in monad_morphism]
Pullback_Module_struct [instance, in monad_morphism]
Pull_back_Module [section, in monad_morphism]
Pull_back_Module.A [variable, in monad_morphism]
Pull_back_Module.B [variable, in monad_morphism]
Pull_back_Module.C [variable, in monad_morphism]
Pull_back_Module.D [variable, in monad_morphism]
Pull_back_Module.f [variable, in monad_morphism]
Pull_back_Module.M [variable, in monad_morphism]
Pull_back_Module.morC [variable, in monad_morphism]
Pull_back_Module.morD [variable, in monad_morphism]
Pull_back_Module.obC [variable, in monad_morphism]
Pull_back_Module.obD [variable, in monad_morphism]
R
reduce_to_sigma [lemma, in my_lib]Rho [projection, in mon_cats]
rho_SET [definition, in mon_cats]
rho_set [definition, in mon_cats]
rho_set_NISO [instance, in mon_cats]
Right_Functor [definition, in bifunctor]
Right_Functor_struct [instance, in bifunctor]
S
SC_inj_mor [definition, in subcategories]SC_inj_ob [definition, in subcategories]
SC_mor [definition, in subcategories]
SC_ob [definition, in subcategories]
SET [section, in cat_SET]
SET [definition, 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]
SET_INIT [instance, in cat_SET]
SET_INIT_TERM [section, in cat_SET]
SET_MONOIDAL [instance, in mon_cats]
SET_mon_cat [section, in mon_cats]
set_prod_functor [definition, in mon_cats]
set_prod_mor [definition, in mon_cats]
set_prod_obj [definition, in mon_cats]
SET_TERM [instance, in cat_SET]
sfst [projection, in mon_cats]
sigma [projection, in monad_morphism]
simpl_eq_sig [lemma, in my_lib]
SMALLCAT [instance, in small_cat]
SmallCat [record, in small_cat]
SMALLCAT_struct [instance, in small_cat]
small_cat [library]
SMON [record, in smon_cats]
smon_cat [section, in smon_cats]
smon_cat [record, in smon_cats]
smon_cats [library]
smon_cat.morC [variable, in smon_cats]
smon_cat.obC [variable, in smon_cats]
smon_cat.smon_cat_ [section, in smon_cats]
smon_cat.smon_cat_.C [variable, in smon_cats]
smon_struct [projection, in smon_cats]
smor [projection, in small_cat]
sobj [projection, in small_cat]
some_other_product_on_functors [section, in prods]
some_other_product_on_functors.C [variable, in prods]
some_other_product_on_functors.D [variable, in prods]
some_other_product_on_functors.F [variable, in prods]
some_other_product_on_functors.G [variable, in prods]
some_other_product_on_functors.morC [variable, in prods]
some_other_product_on_functors.morD [variable, in prods]
some_other_product_on_functors.obC [variable, in prods]
some_other_product_on_functors.obD [variable, in prods]
Some_T [constructor, in cat_INDEXED_TYPE]
Some_TP [constructor, in ind_potype]
Some_TP_PO [definition, in ind_potype]
ssnd [projection, in mon_cats]
sstruct [projection, in small_cat]
subcategories [library]
SubCat_compat [record, in subcategories]
SubCat_def [section, in subcategories]
SubCat_def.C [variable, in subcategories]
SubCat_def.mor [variable, in subcategories]
SubCat_def.ob [variable, in subcategories]
SubCat_def.SubCat_struct [section, in subcategories]
SubCat_def.SubCat_struct.SC [variable, in subcategories]
SubCat_def.SubCat_struct.submorP [variable, in subcategories]
SubCat_def.SubCat_struct.subobP [variable, in subcategories]
SubCat_struct [instance, in subcategories]
subcomp [definition, in subcategories]
subid [definition, in subcategories]
subidP [lemma, in subcategories]
submor [definition, in subcategories]
submor_equiv [lemma, in subcategories]
submor_relation [definition, in subcategories]
submor_rel_imp_rel [lemma, in subcategories]
submor_setoid [definition, in subcategories]
subob [definition, in subcategories]
subst [projection, in monad_def]
subst_ax [definition, in monad_def]
sub_comp [projection, in subcategories]
sub_id [projection, in subcategories]
succ [constructor, in pcfpo]
succ [constructor, in pcf]
syntax_monad_h [instance, in pcf]
syntax_monad_h [instance, in pcfpo]
T
T [projection, in monad_def]tau [projection, in monad_morphism]
tau_tau [lemma, in monad_morphism]
Tau_Tau [projection, in monad_morphism]
tau_tau_def [definition, in monad_morphism]
tens [projection, in mon_cats]
tensor [projection, in smon_cats]
tensor_assoc [projection, in smon_cats]
tens_penta [projection, in mon_cats]
Term [projection, in initial_terminal]
Terminal [record, in initial_terminal]
terminal [definition, in initial_terminal]
TermMor [projection, in initial_terminal]
TermMorUnique [projection, in initial_terminal]
termone [definition, in initial_terminal]
test [section, in category]
test.a [variable, in category]
test.b [variable, in category]
test.C [variable, in category]
test.c [variable, in category]
test.d [variable, in category]
test.f [variable, in category]
test.g [variable, in category]
test.h [variable, in category]
tra [projection, in nat_iso]
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]
tt [constructor, in pcf]
tt [constructor, in pcfpo]
TY [inductive, in pcf]
TY [inductive, in pcfpo]
TYPE [section, in cat_TYPE]
TYPE [definition, in cat_TYPE]
TYPE.TYPE_data [section, in cat_TYPE]
TYPE.TYPE_data.A [variable, in cat_TYPE]
TYPE.TYPE_data.B [variable, in cat_TYPE]
TYPE_catstruct [instance, in cat_TYPE]
TYPE_hom [definition, in cat_TYPE]
TYPE_hom_equiv [definition, in cat_TYPE]
TYPE_hom_oid [definition, in cat_TYPE]
TYPE_hom_oid_prf [lemma, in cat_TYPE]
V
vcompNT [definition, in NT]vcompNT [section, 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]
vcompNT_assoc [lemma, in NT]
vcompNT_lemmata [section, in NT]
vcompNT_lemmata.alpha [variable, in NT]
vcompNT_lemmata.beta [variable, in NT]
vcompNT_lemmata.C [variable, in NT]
vcompNT_lemmata.D [variable, in NT]
vcompNT_lemmata.F [variable, in NT]
vcompNT_lemmata.G [variable, in NT]
vcompNT_lemmata.gamma [variable, in NT]
vcompNT_lemmata.H [variable, in NT]
vcompNT_lemmata.J [variable, in NT]
vcompNT_lemmata.morC [variable, in NT]
vcompNT_lemmata.morD [variable, in NT]
vcompNT_lemmata.obC [variable, in NT]
vcompNT_lemmata.obD [variable, in NT]
VIDNT [section, in NT]
vidNT [definition, in NT]
vidNTl [lemma, in NT]
vidNTr [lemma, 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]
W
weta [projection, in monad_haskell]Z
zero [constructor, in pcf]zero [constructor, in pcfpo]
zerone [definition, in initial_terminal]
Instance Index
A
alpha_set_NISO [in mon_cats]C
Cat_from_SmallCat [in small_cat]Clos_RT_1n_prf [in orders]
F
FunctCat_struct [in CatFunct]I
INDEXED_TYPE [in cat_INDEXED_TYPE]IND_PO_struct [in ind_potype]
L
lambda_set_NISO [in mon_cats]Left_Functor_struct [in bifunctor]
M
MOD_R [in monad_morphism]MONAD [in monad_morphism]
monads [in smon_cats]
Monad_from_Monad_h_struct [in monad_haskell]
Monad_h_from_Monad_struct [in monad_haskell]
O
opt_TP_Func [in ind_potype]P
PCFPO_monad_h [in pcfpo_mod]POTYPE [in orders]
PROD_MODULE [in monad_morphism]
PROD_struct [in prods]
Pullback_Module_struct [in monad_morphism]
R
rho_set_NISO [in mon_cats]Right_Functor_struct [in bifunctor]
S
SET_catstruct [in cat_SET]SET_INIT [in cat_SET]
SET_MONOIDAL [in mon_cats]
SET_TERM [in cat_SET]
SMALLCAT [in small_cat]
SMALLCAT_struct [in small_cat]
SubCat_struct [in subcategories]
syntax_monad_h [in pcf]
syntax_monad_h [in pcfpo]
T
TYPE_catstruct [in cat_TYPE]Projection Index
A
Alpha [in mon_cats]Assoc [in category]
C
cat [in smon_cats]Cat_struct [in category]
comp [in category]
comp_oid [in category]
coprod [in coproduct]
coprod_diag [in coproduct]
coprod_mor [in coproduct]
coprod_mor_unique [in coproduct]
D
dist [in monad_haskell]E
e [in smon_cats]eleft_unit [in smon_cats]
eq_l_r [in mon_cats]
eright_unit [in smon_cats]
eta [in monad_def]
eta1 [in monad_def]
eta2 [in monad_def]
eta_kl [in monad_haskell]
Eta_Tau [in monad_morphism]
F
F [in monad_haskell]Fmor [in functor]
Fobj [in functor]
functor_map_morphism [in functor]
Func_struct [in functor]
I
I [in mon_cats]id [in category]
id_l [in category]
id_r [in category]
Init [in initial_terminal]
InitMor [in initial_terminal]
InitMorUnique [in initial_terminal]
inl [in coproduct]
inr [in coproduct]
inv [in nat_iso]
inv_left [in nat_iso]
inv_right [in nat_iso]
K
kleisli [in monad_haskell]kleisli_oid [in monad_haskell]
kl_eta [in monad_haskell]
L
Lambda [in mon_cats]lam_rho [in mon_cats]
LmoduleF [in monad_morphism]
lmoduleNT [in monad_morphism]
lmodule_morphism_struct [in monad_morphism]
Lmodule_struct [in monad_morphism]
M
module_diag [in monad_morphism]Module_Mor [in monad_morphism]
monad_h_struct [in monad_haskell]
monad_struct [in monad_def]
mor [in category]
mor_oid [in category]
mu [in monad_def]
Mu_Tau [in monad_morphism]
N
NatTrans_struct [in NT]niso_struct [in nat_iso]
O
obj [in category]P
POCarrier [in orders]PO_fun [in orders]
PO_prop [in orders]
PreOrderPrf [in orders]
PreOrderRel [in orders]
preserve_comp [in functor]
preserve_ident [in functor]
prl [in product]
product [in product]
prod_diag [in product]
prod_mor [in product]
prod_mor_unique [in product]
prr [in product]
R
Rho [in mon_cats]S
sfst [in mon_cats]sigma [in monad_morphism]
smon_struct [in smon_cats]
smor [in small_cat]
sobj [in small_cat]
ssnd [in mon_cats]
sstruct [in small_cat]
subst [in monad_def]
sub_comp [in subcategories]
sub_id [in subcategories]
T
T [in monad_def]tau [in monad_morphism]
Tau_Tau [in monad_morphism]
tens [in mon_cats]
tensor [in smon_cats]
tensor_assoc [in smon_cats]
tens_penta [in mon_cats]
Term [in initial_terminal]
TermMor [in initial_terminal]
TermMorUnique [in initial_terminal]
tra [in nat_iso]
trafo [in NT]
trafo_ax [in NT]
W
weta [in monad_haskell]Record Index
C
Cat [in category]Category [in category]
Cat_Coprod [in coproduct]
Cat_Prod [in product]
F
Func [in functor]Functor [in functor]
I
Initial [in initial_terminal]L
LModule [in monad_morphism]LModule_struct [in monad_morphism]
M
Module_Morphism [in monad_morphism]Module_Morphism_struct [in monad_morphism]
Monad [in monad_def]
Monad_h [in monad_haskell]
Monad_h_struct [in monad_haskell]
Monad_Morphism [in monad_morphism]
Monad_struct [in monad_def]
mon_cat [in mon_cats]
N
NatTrans [in NT]NISO [in nat_iso]
NISO_struct [in nat_iso]
NT [in NT]
P
PreOrder_mor [in orders]PreOrder_obj [in orders]
prod_set [in mon_cats]
S
SmallCat [in small_cat]SMON [in smon_cats]
smon_cat [in smon_cats]
SubCat_compat [in subcategories]
T
Terminal [in initial_terminal]Lemma Index
A
assoc [in category]assoc2 [in category]
B
betaS_App1 [in pcfpo]betaS_App2 [in pcfpo]
betaS_Lam [in pcfpo]
betaS_Rec [in pcfpo]
break_Sig_Prop [in my_lib]
break_Sig_Prop2 [in my_lib]
C
CompFassoc [in functor]CompF_assoc [in functor]
CompF_compat_with_eq_Functor [in functor]
Comp_functor_map_morphism [in functor]
comp_order_preserve [in orders]
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_ind_setoid [in ind_potype]
eq_MOD_R_setoid [in monad_morphism]
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]
eq_NT_refl [in NT]
eq_NT_sym [in NT]
eq_NT_trans [in NT]
eq_PreOrder_equiv [in orders]
eta_no_choice [in monad_def]
eta_tau [in monad_morphism]
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]
idl2 [in category]
idr [in category]
idr2 [in category]
id_order_preserve [in orders]
INDEXED_TYPE_equiv [in cat_INDEXED_TYPE]
inl_coprod [in coproduct]
inr_coprod [in coproduct]
M
mod_subst [in monad_morphism]MONAD_mor_setoid [in monad_morphism]
mu_tau [in monad_morphism]
mu_tau2 [in monad_morphism]
N
no_choice [in horcomp]NTcomm [in NT]
O
opt_TP_map_comp [in ind_potype]opt_TP_map_extens [in ind_potype]
opt_TP_map_id [in ind_potype]
opt_TP_preorder [in ind_potype]
opt_T_map_comp [in cat_INDEXED_TYPE]
opt_T_map_extens [in cat_INDEXED_TYPE]
opt_T_map_id [in cat_INDEXED_TYPE]
P
PCF.clos [in pcfpo_mod]PCF.cp_App1 [in pcfpo_mod]
PCF.cp_App2 [in pcfpo_mod]
PCF.cp_Lam [in pcfpo_mod]
PCF.cp_Rec [in pcfpo_mod]
PCF.propag_clos_propag_clos [in pcfpo_mod]
PCF.rename_beta [in pcfpo_mod]
PCF.rename_comp [in pcfpo_mod]
PCF.rename_eq [in pcfpo_mod]
PCF.rename_id [in pcfpo_mod]
PCF.rename_propag [in pcfpo_mod]
PCF.rename_rt_clos [in pcfpo_mod]
PCF.rename_subst [in pcfpo_mod]
PCF.rename_substar [in pcfpo_mod]
PCF.rename_term_inj [in pcfpo_mod]
PCF.shift_eq [in pcfpo_mod]
PCF.shift_lift [in pcfpo_mod]
PCF.shift_propag [in pcfpo_mod]
PCF.shift_rt_clos [in pcfpo_mod]
PCF.shift_var [in pcfpo_mod]
PCF.subst_eq [in pcfpo_mod]
PCF.subst_eq_rename [in pcfpo_mod]
PCF.subst_propag [in pcfpo_mod]
PCF.subst_rename [in pcfpo_mod]
PCF.subst_rt_clos [in pcfpo_mod]
PCF.subst_shift_shift [in pcfpo_mod]
PCF.subst_subst [in pcfpo_mod]
PCF.subst_substar [in pcfpo_mod]
PCF.subst_term_inj [in pcfpo_mod]
PCF.subst_var [in pcfpo_mod]
PCF.var_lift_shift_eq [in pcfpo_mod]
PCF_clos [in pcfpo]
PCF_rename_beta [in pcfpo]
PCF_rename_comp [in pcfpo]
PCF_rename_comp [in pcf]
PCF_rename_eq [in pcf]
PCF_rename_eq [in pcfpo]
PCF_rename_id [in pcfpo]
PCF_rename_id [in pcf]
PCF_rename_propag [in pcfpo]
PCF_rename_rt_clos [in pcfpo]
PCF_rename_subst [in pcf]
PCF_rename_subst [in pcfpo]
PCF_rename_substar [in pcfpo]
PCF_rename_term_inj [in pcf]
PCF_rename_term_inj [in pcfpo]
PCF_shift_eq [in pcf]
PCF_shift_eq [in pcfpo]
PCF_shift_lift [in pcf]
PCF_shift_lift [in pcfpo]
PCF_shift_propag [in pcfpo]
PCF_shift_rt_clos [in pcfpo]
PCF_shift_var [in pcfpo]
PCF_shift_var [in pcf]
PCF_subst_eq [in pcfpo]
PCF_subst_eq [in pcf]
PCF_subst_eq_rename [in pcfpo]
PCF_subst_eq_rename [in pcf]
PCF_subst_propag [in pcfpo]
PCF_subst_rename [in pcfpo]
PCF_subst_rename [in pcf]
PCF_subst_rt_clos [in pcfpo]
PCF_subst_shift_shift [in pcfpo]
PCF_subst_shift_shift [in pcf]
PCF_subst_subst [in pcfpo]
PCF_subst_subst [in pcf]
PCF_subst_substar [in pcfpo]
PCF_subst_term_inj [in pcf]
PCF_subst_term_inj [in pcfpo]
PCF_subst_var [in pcfpo]
PCF_subst_var [in pcf]
PCF_var_lift_shift_eq [in pcf]
PCF_var_lift_shift_eq [in pcfpo]
postcomp [in cats_lemmata]
praecomp [in cats_lemmata]
Prod_equiv_equiv [in prods]
prod_mor_equal [in prods]
prod_mor_equal_l [in prods]
prod_mor_equal_r [in prods]
prod_prl [in product]
prod_prr [in product]
propag_clos_propag_clos [in pcfpo]
R
reduce_to_sigma [in my_lib]S
SET_hom_oid_prf [in cat_SET]simpl_eq_sig [in my_lib]
subidP [in subcategories]
submor_equiv [in subcategories]
submor_rel_imp_rel [in subcategories]
T
tau_tau [in monad_morphism]TYPE_hom_oid_prf [in cat_TYPE]
V
vcompNT1_ax [in NT]vcompNT_assoc [in NT]
vidNTl [in NT]
vidNTr [in NT]
Section Index
B
bifunctor_def [in bifunctor]bifunctor_def.Left_Functor [in bifunctor]
bifunctor_def.Right_Functor [in bifunctor]
bla [in pcfpo]
bla [in mon_cats]
C
CatFunct [in CatFunct]cat_lemmata [in category]
cat_of_R_LModules_over_D [in monad_morphism]
clos_rt_1n [in orders]
CompF_Morphism [in functor]
Comp_Functor [in functor]
coprod [in coproduct]
coprod_bifunctor [in coproduct]
coprod_bifunctor.GENERIC_OPT [in coproduct]
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]indexed_types [in cat_INDEXED_TYPE]
ind_po_cat [in ind_potype]
Initial_Terminal [in initial_terminal]
Injection_Functor [in subcategories]
L
LModule_def [in monad_morphism]LModule_def.LModule_lemmata [in monad_morphism]
LModule_Morphism [in monad_morphism]
LModule_Morphism.LModule_Morphism_struct [in monad_morphism]
M
MONAD [in monad_morphism]monads [in smon_cats]
monad_comp [in monad_def]
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]
monad_morphism_def [in monad_morphism]
monad_morphism_def.Monad_Morphism_lemmata [in monad_morphism]
monoidal_cat_def [in mon_cats]
monoidal_cat_def.Diagram_def [in mon_cats]
N
Nat_Iso_def [in nat_iso]Nat_Iso_def.struct_def [in nat_iso]
Nat_Iso_gives_NT [in nat_iso]
NTlarge [in horcomp]
NT_def [in NT]
O
opt_T [in cat_INDEXED_TYPE]P
pcfo_syntax [in pcfpo]PCF.Beta_Relation [in pcfpo_mod]
PCF.Compat_with_Beta [in pcfpo_mod]
PCF.Compat_with_Beta.inj [in pcfpo_mod]
PCF.Compat_with_Beta.rename [in pcfpo_mod]
PCF.Compat_with_Beta.rename.rename_bs [in pcfpo_mod]
PCF.Compat_with_Beta.shift [in pcfpo_mod]
PCF.Compat_with_Beta.shift.shift_bs [in pcfpo_mod]
PCF.Compat_with_Beta.subst [in pcfpo_mod]
PCF.Compat_with_Beta.subst.subst_bs [in pcfpo_mod]
PCF.Fusion_Laws [in pcfpo_mod]
PCF.Relations_on_PCF [in pcfpo_mod]
pcf_syntax [in pcf]
prae_post_comp [in cats_lemmata]
PreOrder_comp [in orders]
prod [in product]
Product_LModule [in monad_morphism]
PROD_almost_assoc [in smon_cats]
prod_bifunctor [in product]
prod_cat [in prods]
prod_func [in prods]
Pull_back_Module [in monad_morphism]
S
SET [in cat_SET]SET.SET_data [in cat_SET]
SET_INIT_TERM [in cat_SET]
SET_mon_cat [in mon_cats]
smon_cat [in smon_cats]
smon_cat.smon_cat_ [in smon_cats]
some_other_product_on_functors [in prods]
SubCat_def [in subcategories]
SubCat_def.SubCat_struct [in subcategories]
T
test [in category]transport [in category]
transport.Equal_hom_lemmata [in category]
TYPE [in cat_TYPE]
TYPE.TYPE_data [in cat_TYPE]
V
vcompNT [in NT]vcompNT_lemmata [in NT]
VIDNT [in NT]
Constructor Index
A
arrow [in pcf]arrow [in pcfpo]
B
Bool [in pcf]Bool [in pcfpo]
Bottom [in pcfpo]
Bottom [in pcf]
Build_Equal_hom [in category]
C
condB [in pcfpo]condB [in pcf]
condN [in pcfpo]
condN [in pcf]
Const [in pcfpo]
Const [in pcf]
F
ff [in pcf]ff [in pcfpo]
N
Nat [in pcf]Nat [in pcfpo]
Nats [in pcfpo]
Nats [in pcf]
None_T [in cat_INDEXED_TYPE]
None_TP [in ind_potype]
O
optrelTP_none [in ind_potype]optrelTP_some [in ind_potype]
P
PApp [in pcfpo]PApp [in pcf]
PCFbeta_beta [in pcfpo]
PCFbeta_var [in pcfpo]
PCFrelorig [in pcfpo]
PCFrelPApp1 [in pcfpo]
PCFrelPApp2 [in pcfpo]
PCFrelPLam [in pcfpo]
PCFrelPRec [in pcfpo]
PCFVar [in pcf]
PCFVar [in pcfpo]
PCF.App [in pcfpo_mod]
PCF.arrow [in pcfpo_mod]
PCF.beta_beta [in pcfpo_mod]
PCF.beta_var [in pcfpo_mod]
PCF.Bool [in pcfpo_mod]
PCF.Bottom [in pcfpo_mod]
PCF.condB [in pcfpo_mod]
PCF.condN [in pcfpo_mod]
PCF.Const [in pcfpo_mod]
PCF.ff [in pcfpo_mod]
PCF.Lam [in pcfpo_mod]
PCF.Nat [in pcfpo_mod]
PCF.Nats [in pcfpo_mod]
PCF.Rec [in pcfpo_mod]
PCF.relApp1 [in pcfpo_mod]
PCF.relApp2 [in pcfpo_mod]
PCF.relLam [in pcfpo_mod]
PCF.relorig [in pcfpo_mod]
PCF.relRec [in pcfpo_mod]
PCF.succ [in pcfpo_mod]
PCF.tt [in pcfpo_mod]
PCF.Var [in pcfpo_mod]
PCF.zero [in pcfpo_mod]
PLam [in pcf]
PLam [in pcfpo]
PRec [in pcf]
PRec [in pcfpo]
S
Some_T [in cat_INDEXED_TYPE]Some_TP [in ind_potype]
succ [in pcfpo]
succ [in pcf]
T
tt [in pcf]tt [in pcfpo]
Z
zero [in pcf]zero [in pcfpo]
Inductive Index
E
Empty [in cat_SET]Equal_hom [in category]
O
optrelTP [in ind_potype]opt_T [in cat_INDEXED_TYPE]
opt_TPd [in ind_potype]
P
PCF [in pcfpo]PCF [in pcf]
PCFrelpropag [in pcfpo]
PCF.beta_ [in pcfpo_mod]
PCF.Consts [in pcfpo_mod]
PCF.PCF [in pcfpo_mod]
PCF.propag [in pcfpo_mod]
PCF.TY [in pcfpo_mod]
PCF_beta [in pcfpo]
PCF_consts [in pcf]
PCF_consts [in pcfpo]
T
TY [in pcf]TY [in pcfpo]
Definition Index
A
alpha_set [in mon_cats]alpha_SET [in mon_cats]
B
Bifunctor [in bifunctor]build_prod_mor [in prods]
build_prod_obj [in prods]
C
cccomp [in monad_morphism]cccomp_trans [in monad_morphism]
CompF [in functor]
Comp_Fmor [in functor]
Comp_Fobj [in functor]
comp_tensor [in smon_cats]
COPROD_BIF_mor [in coproduct]
COPROD_BIF_obj [in coproduct]
E
eleft [in smon_cats]Equal_NT [in horcomp]
Equal_NTh [in horcomp]
eq_Functor [in functor]
eq_Functor1 [in functor]
eq_INDEXED_TYPE_mor [in cat_INDEXED_TYPE]
eq_ind_po [in ind_potype]
eq_lam_rho [in mon_cats]
eq_MOD_R [in monad_morphism]
eq_MOD_R_mor [in monad_morphism]
Eq_Monad [in monad_def]
Eq_Monad1 [in monad_def]
eq_MONAD_mor1 [in monad_morphism]
eq_NT [in NT]
eq_NTh [in horcomp]
eq_NT1 [in NT]
eq_PreOrder [in orders]
eright [in smon_cats]
eta_mu_ax1 [in monad_def]
eta_mu_ax2 [in monad_def]
eta_tau_def [in monad_morphism]
F
FINJ [in subcategories]FunctCat [in CatFunct]
H
hcompNT [in horcomp]hcompNT1 [in horcomp]
hidNT [in horcomp]
hidNT1 [in horcomp]
hom_transport [in category]
I
Id [in functor]INDEXED_TYPE_comp [in cat_INDEXED_TYPE]
INDEXED_TYPE_id [in cat_INDEXED_TYPE]
INDEXED_TYPE_mor [in cat_INDEXED_TYPE]
INDEXED_TYPE_obj [in cat_INDEXED_TYPE]
INDEXED_TYPE_oid [in cat_INDEXED_TYPE]
ind_po_comp [in ind_potype]
ind_po_id [in ind_potype]
ind_po_mor [in ind_potype]
ind_po_obj [in ind_potype]
ind_po_obj_car [in ind_potype]
ind_po_oid [in ind_potype]
initial [in initial_terminal]
iso [in smon_cats]
I_set [in mon_cats]
L
lambda_SET [in mon_cats]lambda_set [in mon_cats]
lam_rho_dia [in mon_cats]
Left_Functor [in bifunctor]
LMOD_R_ob [in monad_morphism]
M
MEta [in monad_haskell]MEtatrafo [in monad_haskell]
MFunc [in monad_haskell]
Mmor [in monad_haskell]
MMu [in monad_haskell]
MMutrafo [in monad_haskell]
MOD_R_comp [in monad_morphism]
MOD_R_id [in monad_morphism]
MOD_R_mor [in monad_morphism]
MONAD_comp [in monad_morphism]
Monad_h_eta [in monad_haskell]
Monad_h_F [in monad_haskell]
Monad_h_kl [in monad_haskell]
MONAD_id [in monad_morphism]
MONAD_mor [in monad_morphism]
MONAD_mor_oid [in monad_morphism]
MONAD_obj [in monad_morphism]
mu_tau_def [in monad_morphism]
N
NTinv [in nat_iso]NTlarge [in horcomp]
NT_from_MM [in monad_morphism]
NT_type [in horcomp]
O
opt_incl [in cat_INDEXED_TYPE]opt_TP [in ind_potype]
opt_TP_map [in ind_potype]
opt_TP_mapd [in ind_potype]
opt_T_Functor [in cat_INDEXED_TYPE]
opt_T_map [in cat_INDEXED_TYPE]
P
par_prodF [in prods]PCFbeta [in pcfpo]
PCFBETA [in pcfpo]
PCFbetaS [in pcfpo]
PCFVAR [in pcfpo]
PCF.beta [in pcfpo_mod]
PCF.BETA [in pcfpo_mod]
PCF.betaS [in pcfpo_mod]
PCF.inj [in pcfpo_mod]
PCF.inj_ [in pcfpo_mod]
PCF.ipo [in pcfpo_mod]
PCF.PCFrel [in pcfpo_mod]
PCF.rename [in pcfpo_mod]
PCF.rename_ [in pcfpo_mod]
PCF.shift [in pcfpo_mod]
PCF.shift_ [in pcfpo_mod]
PCF.subst [in pcfpo_mod]
PCF.substar [in pcfpo_mod]
PCF.subst_ [in pcfpo_mod]
PCF.VAR [in pcfpo_mod]
PCF.varmap [in pcfpo_mod]
PCF_inj [in pcf]
PCF_inj [in pcfpo]
PCF_inj_ [in pcfpo]
PCF_rename [in pcfpo]
PCF_rename [in pcf]
PCF_rename_ [in pcfpo]
PCF_shift [in pcfpo]
PCF_shift [in pcf]
PCF_shift2 [in pcf]
PCF_shift_ [in pcfpo]
PCF_subst [in pcfpo]
PCF_subst [in pcf]
PCF_substar [in pcf]
PCF_substar [in pcfpo]
PCF_subst_ [in pcfpo]
PCF_varmap [in pcf]
PCF_varmap [in pcfpo]
penta_diag [in mon_cats]
PI [in functor]
PI [in my_lib]
PreOrder_comp [in orders]
PreOrder_id [in orders]
PreOrder_oid [in orders]
PROD [in prods]
PROD_BIF [in coproduct]
PROD_BIF [in product]
PROD_BIF_mor [in product]
PROD_BIF_obj [in product]
Prod_comp [in prods]
Prod_equiv [in prods]
Prod_equiv1 [in prods]
prod_Fmor [in prods]
prod_Fobj [in prods]
Prod_functor [in prods]
Prod_id [in prods]
Prod_mor [in prods]
Prod_NT [in monad_morphism]
Prod_obj [in prods]
Pullback_Module [in monad_morphism]
R
rho_SET [in mon_cats]rho_set [in mon_cats]
Right_Functor [in bifunctor]
S
SC_inj_mor [in subcategories]SC_inj_ob [in subcategories]
SC_mor [in subcategories]
SC_ob [in subcategories]
SET [in cat_SET]
SET_hom [in cat_SET]
SET_hom_equiv [in cat_SET]
SET_hom_oid [in cat_SET]
set_prod_functor [in mon_cats]
set_prod_mor [in mon_cats]
set_prod_obj [in mon_cats]
Some_TP_PO [in ind_potype]
subcomp [in subcategories]
subid [in subcategories]
submor [in subcategories]
submor_relation [in subcategories]
submor_setoid [in subcategories]
subob [in subcategories]
subst_ax [in monad_def]
T
tau_tau_def [in monad_morphism]terminal [in initial_terminal]
termone [in initial_terminal]
tra [in horcomp]
trafo_comm [in NT]
TYPE [in cat_TYPE]
TYPE_hom [in cat_TYPE]
TYPE_hom_equiv [in cat_TYPE]
TYPE_hom_oid [in cat_TYPE]
V
vcompNT [in NT]vcompNT1 [in NT]
vidNT [in NT]
Z
zerone [in initial_terminal]Moduleid Index
P
PCF [in pcfpo_mod]Variable Index
B
bifunctor_def.B [in bifunctor]bifunctor_def.C [in bifunctor]
bifunctor_def.D [in bifunctor]
bifunctor_def.Left_Functor.c [in bifunctor]
bifunctor_def.morB [in bifunctor]
bifunctor_def.morC [in bifunctor]
bifunctor_def.morD [in bifunctor]
bifunctor_def.obB [in bifunctor]
bifunctor_def.obC [in bifunctor]
bifunctor_def.obD [in bifunctor]
bifunctor_def.Right_Functor.b [in bifunctor]
bifunctor_def.S [in bifunctor]
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]
cat_of_R_LModules_over_D.C [in monad_morphism]
cat_of_R_LModules_over_D.D [in monad_morphism]
cat_of_R_LModules_over_D.morC [in monad_morphism]
cat_of_R_LModules_over_D.morD [in monad_morphism]
cat_of_R_LModules_over_D.obC [in monad_morphism]
cat_of_R_LModules_over_D.obD [in monad_morphism]
cat_of_R_LModules_over_D.R [in monad_morphism]
clos_rt_1n.A [in orders]
clos_rt_1n.R [in orders]
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]
coprod.morC [in coproduct]
coprod.obC [in coproduct]
coprod_bifunctor.C [in coproduct]
coprod_bifunctor.GENERIC_OPT.obC [in coproduct]
coprod_bifunctor.H [in coproduct]
coprod_bifunctor.morC [in coproduct]
coprod_bifunctor.obC [in coproduct]
E
endo_monad.C [in smon_cats]endo_monad.morC [in smon_cats]
endo_monad.obC [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]
erightleft.morC [in smon_cats]
erightleft.obC [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.C [in functor]
Functors.D [in functor]
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]
indexed_types.T [in cat_INDEXED_TYPE]
ind_po_cat.T [in ind_potype]
Initial_Terminal.morC [in initial_terminal]
Initial_Terminal.obC [in initial_terminal]
Injection_Functor.C [in subcategories]
Injection_Functor.mor [in subcategories]
Injection_Functor.ob [in subcategories]
Injection_Functor.SC [in subcategories]
Injection_Functor.submorP [in subcategories]
Injection_Functor.subobP [in subcategories]
L
LModule_def.C [in monad_morphism]LModule_def.D [in monad_morphism]
LModule_def.LModule_lemmata.M [in monad_morphism]
LModule_def.morC [in monad_morphism]
LModule_def.morD [in monad_morphism]
LModule_def.obC [in monad_morphism]
LModule_def.obD [in monad_morphism]
LModule_def.R [in monad_morphism]
LModule_Morphism.C [in monad_morphism]
LModule_Morphism.D [in monad_morphism]
LModule_Morphism.LModule_Morphism_struct.F [in monad_morphism]
LModule_Morphism.M [in monad_morphism]
LModule_Morphism.morC [in monad_morphism]
LModule_Morphism.morD [in monad_morphism]
LModule_Morphism.N [in monad_morphism]
LModule_Morphism.obC [in monad_morphism]
LModule_Morphism.obD [in monad_morphism]
LModule_Morphism.R [in monad_morphism]
M
monads.C [in smon_cats]monads.morC [in smon_cats]
monads.obC [in smon_cats]
MONAD.C [in monad_morphism]
MONAD.morC [in monad_morphism]
MONAD.obC [in monad_morphism]
monad_comp.C [in monad_def]
monad_comp.etaF [in monad_def]
monad_comp.etaG [in monad_def]
monad_comp.F [in monad_def]
monad_comp.G [in monad_def]
monad_comp.MonadF [in monad_def]
monad_comp.MonadG [in monad_def]
monad_comp.mor [in monad_def]
monad_comp.muF [in monad_def]
monad_comp.muG [in monad_def]
monad_comp.ob [in monad_def]
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.morC [in monad_haskell]
Monad_gives_Monad_h.obC [in monad_haskell]
monad_haskell_def.C [in monad_haskell]
monad_haskell_def.monad_haskell_class.F [in monad_haskell]
monad_haskell_def.morC [in monad_haskell]
monad_haskell_def.obC [in monad_haskell]
Monad_h_gives_Monad.C [in monad_haskell]
Monad_h_gives_Monad.M [in monad_haskell]
Monad_h_gives_Monad.morC [in monad_haskell]
Monad_h_gives_Monad.obC [in monad_haskell]
monad_morphism_def.C [in monad_morphism]
monad_morphism_def.F [in monad_morphism]
monad_morphism_def.G [in monad_morphism]
monad_morphism_def.Monad_Morphism_lemmata.Tau [in monad_morphism]
monad_morphism_def.morC [in monad_morphism]
monad_morphism_def.obC [in monad_morphism]
monoidal_cat_def.C [in mon_cats]
monoidal_cat_def.Diagram_def.Alpha [in mon_cats]
monoidal_cat_def.Diagram_def.I [in mon_cats]
monoidal_cat_def.Diagram_def.Lambda [in mon_cats]
monoidal_cat_def.Diagram_def.Rho [in mon_cats]
monoidal_cat_def.Diagram_def.tens [in mon_cats]
monoidal_cat_def.morC [in mon_cats]
monoidal_cat_def.obC [in mon_cats]
N
Nat_Iso_def.C [in nat_iso]Nat_Iso_def.D [in nat_iso]
Nat_Iso_def.F [in nat_iso]
Nat_Iso_def.G [in nat_iso]
Nat_Iso_def.morC [in nat_iso]
Nat_Iso_def.morD [in nat_iso]
Nat_Iso_def.obC [in nat_iso]
Nat_Iso_def.obD [in nat_iso]
Nat_Iso_def.struct_def.alpha [in nat_iso]
Nat_Iso_gives_NT.alpha [in nat_iso]
Nat_Iso_gives_NT.C [in nat_iso]
Nat_Iso_gives_NT.D [in nat_iso]
Nat_Iso_gives_NT.F [in nat_iso]
Nat_Iso_gives_NT.G [in nat_iso]
Nat_Iso_gives_NT.morC [in nat_iso]
Nat_Iso_gives_NT.morD [in nat_iso]
Nat_Iso_gives_NT.obC [in nat_iso]
Nat_Iso_gives_NT.obD [in nat_iso]
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]
O
opt_T.T [in cat_INDEXED_TYPE]P
PCF.Compat_with_Beta.rename.rename_bs.rel [in pcfpo_mod]PCF.Compat_with_Beta.shift.shift_bs.rel [in pcfpo_mod]
PCF.Compat_with_Beta.shift.u [in pcfpo_mod]
PCF.Compat_with_Beta.subst.subst_bs.rel [in pcfpo_mod]
PCF.Relations_on_PCF.rel [in pcfpo_mod]
prae_post_comp.C [in cats_lemmata]
prae_post_comp.mor [in cats_lemmata]
prae_post_comp.ob [in cats_lemmata]
PreOrder_comp.A [in orders]
PreOrder_comp.B [in orders]
PreOrder_comp.C [in orders]
PreOrder_comp.f [in orders]
PreOrder_comp.g [in orders]
Product_LModule.C [in monad_morphism]
Product_LModule.M [in monad_morphism]
Product_LModule.morC [in monad_morphism]
Product_LModule.N [in monad_morphism]
Product_LModule.obC [in monad_morphism]
Product_LModule.R [in monad_morphism]
prod.morC [in product]
prod.obC [in product]
PROD_almost_assoc.A [in smon_cats]
PROD_almost_assoc.B [in smon_cats]
PROD_almost_assoc.C [in smon_cats]
PROD_almost_assoc.morA [in smon_cats]
PROD_almost_assoc.morB [in smon_cats]
PROD_almost_assoc.morC [in smon_cats]
PROD_almost_assoc.obA [in smon_cats]
PROD_almost_assoc.obB [in smon_cats]
PROD_almost_assoc.obC [in smon_cats]
prod_bifunctor.C [in product]
prod_bifunctor.H [in product]
prod_bifunctor.morC [in product]
prod_bifunctor.obC [in product]
prod_cat.B [in prods]
prod_cat.C [in prods]
prod_cat.D [in prods]
prod_cat.morB [in prods]
prod_cat.morC [in prods]
prod_cat.morD [in prods]
prod_cat.obB [in prods]
prod_cat.obC [in prods]
prod_cat.obD [in prods]
prod_cat.S [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]
prod_func.morC [in prods]
prod_func.morC' [in prods]
prod_func.morD [in prods]
prod_func.morD' [in prods]
prod_func.obC [in prods]
prod_func.obC' [in prods]
prod_func.obD [in prods]
prod_func.obD' [in prods]
Pull_back_Module.A [in monad_morphism]
Pull_back_Module.B [in monad_morphism]
Pull_back_Module.C [in monad_morphism]
Pull_back_Module.D [in monad_morphism]
Pull_back_Module.f [in monad_morphism]
Pull_back_Module.M [in monad_morphism]
Pull_back_Module.morC [in monad_morphism]
Pull_back_Module.morD [in monad_morphism]
Pull_back_Module.obC [in monad_morphism]
Pull_back_Module.obD [in monad_morphism]
S
SET.SET_data.A [in cat_SET]SET.SET_data.B [in cat_SET]
smon_cat.morC [in smon_cats]
smon_cat.obC [in smon_cats]
smon_cat.smon_cat_.C [in smon_cats]
some_other_product_on_functors.C [in prods]
some_other_product_on_functors.D [in prods]
some_other_product_on_functors.F [in prods]
some_other_product_on_functors.G [in prods]
some_other_product_on_functors.morC [in prods]
some_other_product_on_functors.morD [in prods]
some_other_product_on_functors.obC [in prods]
some_other_product_on_functors.obD [in prods]
SubCat_def.C [in subcategories]
SubCat_def.mor [in subcategories]
SubCat_def.ob [in subcategories]
SubCat_def.SubCat_struct.SC [in subcategories]
SubCat_def.SubCat_struct.submorP [in subcategories]
SubCat_def.SubCat_struct.subobP [in subcategories]
T
test.a [in category]test.b [in category]
test.C [in category]
test.c [in category]
test.d [in category]
test.f [in category]
test.g [in category]
test.h [in category]
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]
TYPE.TYPE_data.A [in cat_TYPE]
TYPE.TYPE_data.B [in cat_TYPE]
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]
vcompNT_lemmata.alpha [in NT]
vcompNT_lemmata.beta [in NT]
vcompNT_lemmata.C [in NT]
vcompNT_lemmata.D [in NT]
vcompNT_lemmata.F [in NT]
vcompNT_lemmata.G [in NT]
vcompNT_lemmata.gamma [in NT]
vcompNT_lemmata.H [in NT]
vcompNT_lemmata.J [in NT]
vcompNT_lemmata.morC [in NT]
vcompNT_lemmata.morD [in NT]
vcompNT_lemmata.obC [in NT]
vcompNT_lemmata.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
B
bifunctorC
categoryCatFunct
cats_lemmata
cat_INDEXED_TYPE
cat_SET
cat_TYPE
coproduct
F
functorH
horcompI
ind_potypeinitial_terminal
M
monad_defmonad_haskell
monad_morphism
mon_cats
my_lib
N
nat_isoNT
O
ordersP
pcfpcfpo
pcfpo_mod
prods
product
pts
S
small_catsmon_cats
subcategories
| 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 | _ | (1216 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 | _ | (31 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 | _ | (95 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 | _ | (29 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 | _ | (175 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 | _ | (99 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 | _ | (69 entries) |
| 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 | _ | (18 entries) |
| 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 | _ | (184 entries) |
| Moduleid 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) |
| 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 | _ | (486 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 | _ | (29 entries) |
This page has been generated by coqdoc