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 _ other (3088 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 _ other (2 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 _ other (316 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 _ other (84 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 _ other (768 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 _ other (105 entries)
Notation 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 _ other (97 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 _ other (196 entries)
Abbreviation 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 _ other (101 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 _ other (28 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 _ other (878 entries)
Module 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 _ other (43 entries)
Axiom 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 _ other (16 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 _ other (417 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 _ other (37 entries)

Global Index

A

acong_fix [constructor, in acong_fix]
acong_app [constructor, in acong_app]
acong_app [constructor, in acong_app]
acong_if [constructor, in acong_if]
acong_if [constructor, in acong_if]
acong_lam [constructor, in acong_lam]
acong_lam [constructor, in acong_lam]
acong_bool [constructor, in acong_bool]
acong_bool [constructor, in acong_bool]
acong_var [constructor, in acong_var]
acong_var [constructor, in acong_var]
adequacy [lemma, in adequacy]
adequacy [lemma, in adequacy]
adequacy [lemma, in adequacy]
adequacy [lemma, in adequacy]
adjoin_char [definition, in adjoin_char]
adjunction [abbreviation, in adjunction]
Adjunction [abbreviation, in Adjunction]
Adjunction [module, in Adjunction]
Adjunction.adjoint_axiom1 [projection, in adjoint_axiom1]
Adjunction.adjoint_axiom2 [projection, in adjoint_axiom2]
Adjunction.adjunction [record, in adjunction]
Adjunction.adjunction [section, in adjunction]
Adjunction.Adjunction [constructor, in Adjunction]
Adjunction.adjunction.C [variable, in C]
Adjunction.adjunction.D [variable, in D]
Adjunction.adjunction.L [variable, in L]
Adjunction.adjunction.R [variable, in R]
Adjunction.counit [projection, in counit]
Adjunction.unit [projection, in unit]
adj_inv_eq_converse [lemma, in adj_inv_eq_converse]
adj_counit_inv_hom [definition, in adj_counit_inv_hom]
adj_unit [definition, in adj_unit]
adj_counit_inv_ntish [lemma, in adj_counit_inv_ntish]
adj_counit_rel_elem [lemma, in adj_counit_rel_elem]
adj_unit_rel_elem [lemma, in adj_unit_rel_elem]
adj_counit_inv_largest [lemma, in adj_counit_inv_largest]
adj_unit_hom [definition, in adj_unit_hom]
adj_counit_inv_eq [lemma, in adj_counit_inv_eq]
adj_counit_inv_le [lemma, in adj_counit_inv_le]
adj_unit_rel [definition, in adj_unit_rel]
adj_inv_eq [lemma, in adj_inv_eq]
adj_counit_hom [definition, in adj_counit_hom]
adj_counit [definition, in adj_counit]
adj_counit_rel [definition, in adj_counit_rel]
admissible [definition, in admissible]
AG_cocone' [definition, in AG_cocone']
AG_cocone [definition, in AG_cocone]
Alg [abbreviation, in Alg]
Alg [module, in Alg]
alg [abbreviation, in alg]
ALG [abbreviation, in ALG]
Alg.Alg [constructor, in Alg]
Alg.alg [record, in alg]
Alg.alg [section, in alg]
Alg.ALG [definition, in ALG]
Alg.Alg_hom [constructor, in Alg_hom]
Alg.alg_hom [record, in alg_hom]
Alg.alg.C [variable, in C]
Alg.alg.F [variable, in F]
Alg.carrier [projection, in carrier]
Alg.cata [projection, in cata]
Alg.cata_axiom' [lemma, in cata_axiom']
Alg.cata_axiom [projection, in cata_axiom]
Alg.compose [definition, in compose]
Alg.forget [definition, in forget]
Alg.forget [section, in forget]
Alg.forget.C [variable, in C]
Alg.forget.F [variable, in F]
Alg.free [definition, in free]
Alg.hom_axiom [projection, in hom_axiom]
Alg.hom_map [projection, in hom_map]
Alg.ident [definition, in ident]
Alg.init [projection, in init]
Alg.initial_inj_epic [lemma, in initial_inj_epic]
Alg.Initial_alg [constructor, in Initial_alg]
Alg.initial_alg [record, in initial_alg]
Alg.in_out [lemma, in in_out]
Alg.iota [projection, in iota]
Alg.lift_alg [definition, in lift_alg]
Alg.out [definition, in out]
Alg.out_in [lemma, in out_in]
allowable_chars [definition, in allowable_chars]
all_jrels_complete [lemma, in all_jrels_complete]
all_finset_semidec [definition, in all_finset_semidec]
all_finset_setdec [definition, in all_finset_setdec]
all_finset_setdec_elem [lemma, in all_finset_setdec_elem]
all_jrels_inh' [lemma, in all_jrels_inh']
all_jrels_inh [lemma, in all_jrels_inh]
all_jrels [definition, in all_jrels]
alpha_cong_denote' [lemma, in alpha_cong_denote']
alpha_cong_denote' [lemma, in alpha_cong_denote']
alpha_eq_trans [lemma, in alpha_eq_trans]
alpha_eq_trans [lemma, in alpha_eq_trans]
alpha_eq_sym [lemma, in alpha_eq_sym]
alpha_eq_sym [lemma, in alpha_eq_sym]
alpha_cong_eq [lemma, in alpha_cong_eq]
alpha_cong_eq [lemma, in alpha_cong_eq]
alpha_cong_wk [lemma, in alpha_cong_wk]
alpha_cong_wk [lemma, in alpha_cong_wk]
alpha_eq_refl [lemma, in alpha_eq_refl]
alpha_eq_refl [lemma, in alpha_eq_refl]
alpha_cong [inductive, in alpha_cong]
alpha_cong [inductive, in alpha_cong]
alpha_cong_denote [lemma, in alpha_cong_denote]
alpha_cong_denote [lemma, in alpha_cong_denote]
alpha_cong_value [lemma, in alpha_cong_value]
alpha_cong_value [lemma, in alpha_cong_value]
antistrict [definition, in antistrict]
antistrict_pair_commute1 [lemma, in antistrict_pair_commute1]
antistrict_pair_commute2 [lemma, in antistrict_pair_commute2]
antistrict_nonbottom [lemma, in antistrict_nonbottom]
apply [abbreviation, in apply]
apply [abbreviation, in apply]
apply_acceptable [definition, in apply_acceptable]
apply_acceptable_ok [lemma, in apply_acceptable_ok]
apply_rel_elem [lemma, in apply_rel_elem]
apply_acceptable_dec [lemma, in apply_acceptable_dec]
apply_rel_dir [lemma, in apply_rel_dir]
apply_rel [definition, in apply_rel]
apply_rel_ordering [lemma, in apply_rel_ordering]
approx_rels [library]
app_not_value [lemma, in app_not_value]
app_not_value [lemma, in app_not_value]
app_elem [lemma, in app_elem]
atom [definition, in atom]
atoms [library]
atom_dec [definition, in atom_dec]
atom_strong_eq [lemma, in atom_strong_eq]
atom_supp [definition, in atom_supp]


B

basics [library]
bicategories [library]
Bicategory [abbreviation, in Bicategory]
Bicategory [module, in Bicategory]
bicategory [abbreviation, in bicategory]
Bicategory.assoc [projection, in assoc]
Bicategory.associator_pentagon [projection, in associator_pentagon]
Bicategory.assoc_natural [projection, in assoc_natural]
Bicategory.Bicategory [constructor, in Bicategory]
Bicategory.bicategory [record, in bicategory]
Bicategory.bicategory [section, in bicategory]
Bicategory.bicategory.cat_axioms [variable, in cat_axioms]
Bicategory.bicategory.comp [variable, in comp]
Bicategory.bicategory.CompHom [variable, in CompHom]
Bicategory.bicategory.CompHoriz [variable, in CompHoriz]
Bicategory.bicategory.eq [variable, in eq]
Bicategory.bicategory.hom [variable, in hom]
Bicategory.bicategory.hom2 [variable, in hom2]
Bicategory.bicategory.Ident [variable, in Ident]
Bicategory.bicategory.ob [variable, in ob]
_ • _ [notation, in ::x_'•'_x]
_ ⋆ _ [notation, in ::x_'⋆'_x]
Id [notation, in ::'Id']
Id ( _ ) [notation, in ::'Id'_'('_x_')']
Bicategory.cat_axioms [projection, in cat_axioms]
Bicategory.comp [projection, in comp]
Bicategory.CompHom [projection, in CompHom]
Bicategory.CompHoriz [projection, in CompHoriz]
Bicategory.eq [projection, in eq]
Bicategory.hom [projection, in hom]
Bicategory.HOM [definition, in HOM]
Bicategory.hom2 [projection, in hom2]
Bicategory.Ident [projection, in Ident]
Bicategory.Mixin [constructor, in Mixin]
Bicategory.mixin [projection, in mixin]
Bicategory.mixin_of [record, in mixin_of]
Bicategory.ob [projection, in ob]
Bicategory.unitor_triangle [projection, in unitor_triangle]
Bicategory.unit1 [projection, in unit1]
Bicategory.unit1_natural [projection, in unit1_natural]
Bicategory.unit2 [projection, in unit2]
Bicategory.unit2_natural [projection, in unit2_natural]
BICAT_EQ [definition, in BICAT_EQ]
bicat_assoc [definition, in bicat_assoc]
bicat_unit1 [definition, in bicat_unit1]
bicat_unit2 [definition, in bicat_unit2]
BICAT_COMP [definition, in BICAT_COMP]
bilimit [definition, in bilimit]
bilimit [section, in bilimit]
bilimit [library]
bilimit_construction [definition, in bilimit_construction]
bilimit_cocone [definition, in bilimit_cocone]
bilimit_cpo_colimit [lemma, in bilimit_cpo_colimit]
bilimit_cpo_colimit1 [lemma, in bilimit_cpo_colimit1]
bilimit_cpo_colimit2 [lemma, in bilimit_cpo_colimit2]
bilimit.bilimit_univ.YC [variable, in YC]
bilimit.bilimit_univ [section, in bilimit_univ]
bilimit.DS [variable, in DS]
bilimit.hf [variable, in hf]
bilimit.I [variable, in I]
bind [constructor, in bind]
bind [abbreviation, in bind]
bind [abbreviation, in bind]
binding [definition, in binding]
bindingF [definition, in bindingF]
binding_equiv [definition, in binding_equiv]
binding_support [definition, in binding_support]
binding_fmap_defn [definition, in binding_fmap_defn]
binding_fmap [definition, in binding_fmap]
binding_eq [definition, in binding_eq]
binding_fmap_ident [lemma, in binding_fmap_ident]
binding_fmap_compose [lemma, in binding_fmap_compose]
binding_ty [inductive, in binding_ty]
binding_equiv_forall [lemma, in binding_equiv_forall]
binding_fmap_respects [lemma, in binding_fmap_respects]
binding_nominal_mixin [definition, in binding_nominal_mixin]
binding_eq_mixin [definition, in binding_eq_mixin]
binding_papp [definition, in binding_papp]
boolset [definition, in boolset]
bottom [section, in bottom]
bottom [projection, in bottom]
bottom_least [projection, in bottom_least]
bottom.X [variable, in X]
bottom.Y [variable, in Y]


C

canonical_bool [lemma, in canonical_bool]
Cartesian [abbreviation, in Cartesian]
Cartesian [module, in Cartesian]
cartesian [abbreviation, in cartesian]
CartesianClosed [abbreviation, in CartesianClosed]
CartesianClosed [module, in CartesianClosed]
CartesianClosed.apply [projection, in apply]
CartesianClosed.apply_op [definition, in apply_op]
CartesianClosed.Axioms [constructor, in Axioms]
CartesianClosed.axioms [record, in axioms]
CartesianClosed.cartesian [definition, in cartesian]
CartesianClosed.CartesianClosed [constructor, in CartesianClosed]
CartesianClosed.cartesian_closed.comp [variable, in comp]
CartesianClosed.cartesian_mixin [projection, in cartesian_mixin]
CartesianClosed.cartesian_closed.axioms.curry [variable, in curry]
CartesianClosed.cartesian_closed.cat_axioms [variable, in cat_axioms]
CartesianClosed.cartesian_closed.axioms.exp [variable, in exp]
CartesianClosed.cartesian_closed.cartesian [variable, in cartesian]
CartesianClosed.cartesian_closed.axioms [section, in axioms]
CartesianClosed.cartesian_closed.eq [variable, in eq]
CartesianClosed.cartesian_closed.hom [variable, in hom]
CartesianClosed.cartesian_closed.terminated [variable, in terminated]
CartesianClosed.cartesian_closed.ob [variable, in ob]
CartesianClosed.cartesian_closed.axioms.apply [variable, in apply]
CartesianClosed.cartesian_closed [record, in cartesian_closed]
CartesianClosed.cartesian_closed [section, in cartesian_closed]
CartesianClosed.cartesian' [definition, in cartesian']
CartesianClosed.category [definition, in category]
CartesianClosed.cat_axioms [projection, in cat_axioms]
CartesianClosed.ccc_axioms [projection, in ccc_axioms]
CartesianClosed.comp [definition, in comp]
CartesianClosed.comp_mixin [projection, in comp_mixin]
CartesianClosed.comp' [definition, in comp']
CartesianClosed.curry [projection, in curry]
CartesianClosed.curry_op [definition, in curry_op]
CartesianClosed.curry_univ [projection, in curry_univ]
CartesianClosed.curry_commute [projection, in curry_commute]
CartesianClosed.eq [definition, in eq]
CartesianClosed.eq_mixin [projection, in eq_mixin]
CartesianClosed.eq' [definition, in eq']
CartesianClosed.exp [projection, in exp]
CartesianClosed.exp_op [definition, in exp_op]
CartesianClosed.hom [projection, in hom]
CartesianClosed.Mixin [constructor, in Mixin]
CartesianClosed.mixin [projection, in mixin]
CartesianClosed.mixin_of [record, in mixin_of]
CartesianClosed.ob [projection, in ob]
CartesianClosed.terminated [definition, in terminated]
CartesianClosed.terminated_mixin [projection, in terminated_mixin]
cartesian_closed [abbreviation, in cartesian_closed]
Cartesian.Axioms [constructor, in Axioms]
Cartesian.axioms [record, in axioms]
Cartesian.Cartesian [constructor, in Cartesian]
Cartesian.cartesian [record, in cartesian]
Cartesian.cartesian [section, in cartesian]
Cartesian.cartesian_axioms [projection, in cartesian_axioms]
Cartesian.cartesian.axioms [section, in axioms]
Cartesian.cartesian.axioms.pairing [variable, in pairing]
Cartesian.cartesian.axioms.product [variable, in product]
Cartesian.cartesian.axioms.proj1 [variable, in proj1]
Cartesian.cartesian.axioms.proj2 [variable, in proj2]
Cartesian.cartesian.comp [variable, in comp]
Cartesian.cartesian.eq [variable, in eq]
Cartesian.cartesian.hom [variable, in hom]
Cartesian.cartesian.ob [variable, in ob]
Cartesian.category [definition, in category]
Cartesian.cat_axioms [projection, in cat_axioms]
Cartesian.comp [definition, in comp]
Cartesian.comp_mixin [projection, in comp_mixin]
Cartesian.comp' [definition, in comp']
Cartesian.eq [definition, in eq]
Cartesian.eq_mixin [projection, in eq_mixin]
Cartesian.eq' [definition, in eq']
Cartesian.hom [projection, in hom]
Cartesian.Mixin [constructor, in Mixin]
Cartesian.mixin [projection, in mixin]
Cartesian.mixin_of [record, in mixin_of]
Cartesian.ob [projection, in ob]
Cartesian.pairing [projection, in pairing]
Cartesian.pairing_univ [projection, in pairing_univ]
Cartesian.pairing_op [definition, in pairing_op]
Cartesian.product [projection, in product]
Cartesian.product_op [definition, in product_op]
Cartesian.proj1 [projection, in proj1]
Cartesian.proj1_commute [projection, in proj1_commute]
Cartesian.proj1_op [definition, in proj1_op]
Cartesian.proj2 [projection, in proj2]
Cartesian.proj2_op [definition, in proj2_op]
Cartesian.proj2_commute [projection, in proj2_commute]
Cartesian.terminated [definition, in terminated]
Cartesian.term_mixin [projection, in term_mixin]
cast [definition, in cast]
cast [section, in cast]
castty [abbreviation, in castty]
castty [abbreviation, in castty]
cast_iso1 [lemma, in cast_iso1]
cast_iso2 [lemma, in cast_iso2]
cast_dec_id [lemma, in cast_dec_id]
cast_refl [lemma, in cast_refl]
cast_compose [lemma, in cast_compose]
cast_rel_elem [lemma, in cast_rel_elem]
cast_rel [definition, in cast_rel]
cast.A [variable, in A]
cast.Adec [variable, in Adec]
cast.F [variable, in F]
cast.hf [variable, in hf]
CAT [definition, in CAT]
CAT [section, in CAT]
cata_hom_iter_hom [lemma, in cata_hom_iter_hom]
cata_alg_hom [definition, in cata_alg_hom]
cata_hom' [definition, in cata_hom']
cata_hom [definition, in cata_hom]
categories [library]
category [abbreviation, in category]
Category [abbreviation, in Category]
Category [module, in Category]
category_axioms.C [variable, in C]
category_axioms [section, in category_axioms]
Category.assoc [projection, in assoc]
Category.Axioms [constructor, in Axioms]
Category.axioms [record, in axioms]
Category.category [record, in category]
Category.category [section, in category]
Category.Category [constructor, in Category]
Category.category.COMP [variable, in COMP]
Category.category.EQ [variable, in EQ]
Category.category.hom [variable, in hom]
Category.category.ob [variable, in ob]
Category.cat_EQ [definition, in cat_EQ]
Category.cat_axioms [projection, in cat_axioms]
Category.cat_COMP [definition, in cat_COMP]
Category.comp [projection, in comp]
Category.eq [projection, in eq]
Category.hom [projection, in hom]
Category.ident1 [projection, in ident1]
Category.ident2 [projection, in ident2]
Category.ob [projection, in ob]
Category.respects [projection, in respects]
cat_bicategory_mixin [definition, in cat_bicategory_mixin]
CAT_EQ [definition, in CAT_EQ]
CAT_COMP [definition, in CAT_COMP]
cat_assoc [definition, in cat_assoc]
cat_respects [definition, in cat_respects]
cat_ident1 [definition, in cat_ident1]
cat_ident2 [definition, in cat_ident2]
CAT_axioms [definition, in CAT_axioms]
cbnLamF [definition, in cbnLamF]
cbnLamF_continuous [lemma, in cbnLamF_continuous]
cbvLamF [definition, in cbvLamF]
cbvLamF_continuous [lemma, in cbvLamF_continuous]
chain_sup [definition, in chain_sup]
chain_induction [lemma, in chain_induction]
char_ord [definition, in char_ord]
check_inh [lemma, in check_inh]
choose [definition, in choose]
choose_elem [lemma, in choose_elem]
choose_ub_set [projection, in choose_ub_set]
choose_ub [lemma, in choose_ub]
choose_finset_sub [lemma, in choose_finset_sub]
choose_finset [definition, in choose_finset]
choose_finset_in [lemma, in choose_finset_in]
choose' [definition, in choose']
cl_eset_theory [definition, in cl_eset_theory]
cl_finset [abbreviation, in cl_finset]
cl_finset_theory [definition, in cl_finset_theory]
cl_eset [abbreviation, in cl_eset]
cocartesian [abbreviation, in cocartesian]
Cocartesian [abbreviation, in Cocartesian]
Cocartesian [module, in Cocartesian]
Cocartesian.Axioms [constructor, in Axioms]
Cocartesian.axioms [record, in axioms]
Cocartesian.category [definition, in category]
Cocartesian.cat_axioms [projection, in cat_axioms]
Cocartesian.cocartesian [record, in cocartesian]
Cocartesian.cocartesian [section, in cocartesian]
Cocartesian.Cocartesian [constructor, in Cocartesian]
Cocartesian.cocartesian_axioms [projection, in cocartesian_axioms]
Cocartesian.cocartesian.axioms [section, in axioms]
Cocartesian.cocartesian.axioms.either [variable, in either]
Cocartesian.cocartesian.axioms.inl [variable, in inl]
Cocartesian.cocartesian.axioms.inr [variable, in inr]
Cocartesian.cocartesian.axioms.sum [variable, in sum]
Cocartesian.cocartesian.comp [variable, in comp]
Cocartesian.cocartesian.eq [variable, in eq]
Cocartesian.cocartesian.hom [variable, in hom]
Cocartesian.cocartesian.ob [variable, in ob]
Cocartesian.comp [definition, in comp]
Cocartesian.comp_mixin [projection, in comp_mixin]
Cocartesian.comp' [definition, in comp']
Cocartesian.either [projection, in either]
Cocartesian.either_op [definition, in either_op]
Cocartesian.either_univ [projection, in either_univ]
Cocartesian.eq [definition, in eq]
Cocartesian.eq_mixin [projection, in eq_mixin]
Cocartesian.eq' [definition, in eq']
Cocartesian.hom [projection, in hom]
Cocartesian.initalized [definition, in initalized]
Cocartesian.init_mixin [projection, in init_mixin]
Cocartesian.inl [projection, in inl]
Cocartesian.inl_op [definition, in inl_op]
Cocartesian.inl_commute [projection, in inl_commute]
Cocartesian.inr [projection, in inr]
Cocartesian.inr_op [definition, in inr_op]
Cocartesian.inr_commute [projection, in inr_commute]
Cocartesian.Mixin [constructor, in Mixin]
Cocartesian.mixin [projection, in mixin]
Cocartesian.mixin_of [record, in mixin_of]
Cocartesian.ob [projection, in ob]
Cocartesian.sum [projection, in sum]
Cocartesian.sum_op [definition, in sum_op]
Cocone [constructor, in Cocone]
cocone [record, in cocone]
cocone_fstF [definition, in cocone_fstF]
cocone_minus1 [definition, in cocone_minus1]
cocone_spoke [projection, in cocone_spoke]
cocone_commute [projection, in cocone_commute]
cocone_plus1 [definition, in cocone_plus1]
cocone_plus1 [definition, in cocone_plus1]
cocone_app [definition, in cocone_app]
cocone_point [projection, in cocone_point]
cocone_sndF [definition, in cocone_sndF]
colift [definition, in colift]
colimit_decompose2.I [variable, in I]
colimit_decompose.I [variable, in I]
colimit_decompose2.CC [variable, in CC]
colimit_decompose.CC [variable, in CC]
colimit_decompose2.DS [variable, in DS]
colimit_decompose.DS [variable, in DS]
colimit_decompose2 [section, in colimit_decompose2]
colimit_decompose [lemma, in colimit_decompose]
colimit_decompose [section, in colimit_decompose]
colimit_decompose2.hf [variable, in hf]
colimit_decompose.hf [variable, in hf]
colimit_decompose2.decompose [variable, in decompose]
colimit_decompose.Hcolimit [variable, in Hcolimit]
colim_commute [projection, in colim_commute]
colim_uniq [projection, in colim_uniq]
colim_univ [projection, in colim_univ]
Color [constructor, in Color]
color [record, in color]
colored_sets.colored_sets.cunion.A [variable, in A]
colored_sets.colored_sets.C [variable, in C]
colored_sets.colored_sets.T [variable, in T]
colored_sets.forget_color [definition, in forget_color]
colored_sets.mixin [definition, in mixin]
colored_sets.cset [definition, in cset]
colored_sets.colored_sets.cunion.XS [variable, in XS]
colored_sets.colored_sets [section, in colored_sets]
colored_sets [module, in colored_sets]
colored_sets.cmember [definition, in cmember]
colored_sets.csingle [definition, in csingle]
colored_sets.cunion [definition, in cunion]
colored_sets.colored_sets.cunion [section, in cunion]
colored_sets.cimage [definition, in cimage]
color_prop [projection, in color_prop]
color_eq [projection, in color_eq]
color_and [definition, in color_and]
color_union [projection, in color_union]
color_image [projection, in color_image]
color_single [projection, in color_single]
Comp [module, in Comp]
composeF_continuous [lemma, in composeF_continuous]
compose_directed [lemma, in compose_directed]
compose_ident_rel1 [lemma, in compose_ident_rel1]
compose_ident_rel2 [lemma, in compose_ident_rel2]
compose_elem [lemma, in compose_elem]
compose_rel [definition, in compose_rel]
compose_ordering [lemma, in compose_ordering]
compose_term_subst [lemma, in compose_term_subst]
compose_term_subst [lemma, in compose_term_subst]
compose_assoc [lemma, in compose_assoc]
comp_horiz [definition, in comp_horiz]
comp_op [definition, in comp_op]
Comp.comp [projection, in comp]
Comp.hom [projection, in hom]
Comp.identity [projection, in identity]
Comp.Mixin [constructor, in Mixin]
Comp.mixin [projection, in mixin]
Comp.mixin_of [record, in mixin_of]
Comp.ob [projection, in ob]
Comp.Pack [constructor, in Pack]
Comp.type [record, in type]
concat [definition, in concat]
concat [definition, in concat]
Concrete [constructor, in Concrete]
concrete [record, in concrete]
CONCRETE_EQ [definition, in CONCRETE_EQ]
Cone [module, in Cone]
Cone.axiom [projection, in axiom]
Cone.Cone [constructor, in Cone]
Cone.cone [record, in cone]
Cone.cone [section, in cone]
Cone.CONE [definition, in CONE]
Cone.cone_ident [definition, in cone_ident]
Cone.Cone_hom [constructor, in Cone_hom]
Cone.cone_hom [record, in cone_hom]
Cone.cone_compose [definition, in cone_compose]
Cone.cone.C [variable, in C]
Cone.cone.F [variable, in F]
Cone.cone.J [variable, in J]
Cone.diagram [definition, in diagram]
Cone.hom_axiom [projection, in hom_axiom]
Cone.hom_map [projection, in hom_map]
Cone.point [projection, in point]
Cone.spoke [projection, in spoke]
const [definition, in const]
cons_elem [lemma, in cons_elem]
cons_subset [lemma, in cons_subset]
cons_morphism [lemma, in cons_morphism]
context [inductive, in context]
context [inductive, in context]
context [inductive, in context]
context [inductive, in context]
continuous [definition, in continuous]
continuous_equiv [lemma, in continuous_equiv]
continuous_pair [lemma, in continuous_pair]
continuous_sequence [lemma, in continuous_sequence]
continuous_pi1 [lemma, in continuous_pi1]
continuous_pi2 [lemma, in continuous_pi2]
continuous_functor [definition, in continuous_functor]
cont_adj [library]
cont_functors [library]
Convex [constructor, in Convex]
countable_ID.A [variable, in A]
countable_ID [section, in countable_ID]
countable_indefinite_description [lemma, in countable_indefinite_description]
cpo [abbreviation, in cpo]
CPO [abbreviation, in CPO]
CPO [module, in CPO]
cpo [library]
CPO.app [definition, in app]
CPO.app_to [definition, in app_to]
CPO.axiom [lemma, in axiom]
CPO.build_hom [definition, in build_hom]
CPO.carrier [projection, in carrier]
CPO.cat_axioms [lemma, in cat_axioms]
CPO.comp [definition, in comp]
CPO.compose [definition, in compose]
CPO.comp_mixin [definition, in comp_mixin]
CPO.cont [projection, in cont]
CPO.continuous_sup [lemma, in continuous_sup]
CPO.continuous_sup' [lemma, in continuous_sup']
CPO.CPO [definition, in CPO]
CPO.cpo_mixin [projection, in cpo_mixin]
CPO.cpo_eq_mixin [definition, in cpo_eq_mixin]
CPO.cpo_eq [definition, in cpo_eq]
CPO.hom [record, in hom]
CPO.Hom [constructor, in Hom]
CPO.hom_ord [definition, in hom_ord]
CPO.hom_ord_mixin [definition, in hom_ord_mixin]
CPO.hom_order [definition, in hom_order]
CPO.hom_sup [definition, in hom_sup]
CPO.hom_cpo [definition, in hom_cpo]
CPO.hom_mixin [definition, in hom_mixin]
CPO.ident [definition, in ident]
CPO.map [projection, in map]
CPO.Mixin [constructor, in Mixin]
CPO.mixin_of [record, in mixin_of]
CPO.mono [projection, in mono]
CPO.ord_mixin [projection, in ord_mixin]
CPO.ord_hom [definition, in ord_hom]
CPO.Pack [constructor, in Pack]
CPO.pair [definition, in pair]
CPO.pi1 [definition, in pi1]
CPO.pi2 [definition, in pi2]
CPO.prod [section, in prod]
CPO.prod_mixin [definition, in prod_mixin]
CPO.prod_sup [definition, in prod_sup]
CPO.prod_cpo [definition, in prod_cpo]
CPO.prod.A [variable, in A]
CPO.prod.B [variable, in B]
CPO.prod.CL [variable, in CL]
CPO.sup [projection, in sup]
CPO.sup_op [definition, in sup_op]
CPO.sup_is_ub [projection, in sup_is_ub]
CPO.sup_is_lub [lemma, in sup_is_lub]
CPO.sup_is_least [projection, in sup_is_least]
CPO.type [record, in type]
∐ _ (cpo_scope) [notation, in :cpo_scope:'∐'_x]
cppo [abbreviation, in cppo]
cppo_bot_least [lemma, in cppo_bot_least]
cppo_pointed [instance, in cppo_pointed]
cppo_bot [definition, in cppo_bot]
cset_theory [definition, in cset_theory]
curry [section, in curry]
curry_rel_ordering [lemma, in curry_rel_ordering]
curry_acceptable_semidec [lemma, in curry_acceptable_semidec]
curry_rel [definition, in curry_rel]
curry_commute2 [lemma, in curry_commute2]
curry_commute3 [lemma, in curry_commute3]
curry_apply [lemma, in curry_apply]
curry_universal [lemma, in curry_universal]
curry_univ [lemma, in curry_univ]
curry_commute [lemma, in curry_commute]
curry_rel_elem [lemma, in curry_rel_elem]
curry_acceptable [definition, in curry_acceptable]
curry_rel_dir [lemma, in curry_rel_dir]
curry.A [variable, in A]
curry.B [variable, in B]
curry.C [variable, in C]
curry.HAeff [variable, in HAeff]
curry.HAplt [variable, in HAplt]
curry.HBeff [variable, in HBeff]
curry.HBplt [variable, in HBplt]
curry.HCeff [variable, in HCeff]
curry.hf [variable, in hf]
curry.HR [variable, in HR]
curry.HRdir [variable, in HRdir]
curry.R [variable, in R]
curry.Reff [variable, in Reff]
curry.R' [variable, in R']
cxt [abbreviation, in cxt]
cxt [abbreviation, in cxt]
cxt_fix [constructor, in cxt_fix]
cxt_eq [definition, in cxt_eq]
cxt_eq [definition, in cxt_eq]
cxt_eq [definition, in cxt_eq]
cxt_eq [definition, in cxt_eq]
cxt_if [constructor, in cxt_if]
cxt_if [constructor, in cxt_if]
cxt_appl [constructor, in cxt_appl]
cxt_appl [constructor, in cxt_appl]
cxt_appl [constructor, in cxt_appl]
cxt_appl [constructor, in cxt_appl]
cxt_appr [constructor, in cxt_appr]
cxt_appr [constructor, in cxt_appr]
cxt_appr [constructor, in cxt_appr]
cxt_appr [constructor, in cxt_appr]
cxt_lam [constructor, in cxt_lam]
cxt_lam [constructor, in cxt_lam]
cxt_top [constructor, in cxt_top]
cxt_top [constructor, in cxt_top]
cxt_top [constructor, in cxt_top]
cxt_top [constructor, in cxt_top]


D

dcpo [abbreviation, in dcpo]
decompose_is_colimit [definition, in decompose_is_colimit]
decompose_univ [definition, in decompose_univ]
decompose_univ_func [definition, in decompose_univ_func]
decset [projection, in decset]
decset_correct [projection, in decset_correct]
dec_lemmas.A [variable, in A]
dec_lemmas.Hplt [variable, in Hplt]
dec_semidec [definition, in dec_semidec]
dec_lemmas.hf [variable, in hf]
dec_conj [lemma, in dec_conj]
dec_lemmas.Heff [variable, in Heff]
dec_lemmas [section, in dec_lemmas]
deflate [definition, in deflate]
deflate_inflate0' [lemma, in deflate_inflate0']
deflate_inflate1' [lemma, in deflate_inflate1']
deflate_inflate' [lemma, in deflate_inflate']
deflate_inflate0 [lemma, in deflate_inflate0]
deflate_inflate1 [lemma, in deflate_inflate1]
deflate_inflate [lemma, in deflate_inflate]
deflate' [definition, in deflate']
deflate00 [lemma, in deflate00]
deflate00' [lemma, in deflate00']
deflate01 [lemma, in deflate01]
deflate01' [lemma, in deflate01']
deflate10 [lemma, in deflate10]
deflate10' [lemma, in deflate10']
deflate11 [lemma, in deflate11]
deflate11' [lemma, in deflate11']
denote [definition, in denote]
denote [definition, in denote]
denote [definition, in denote]
denote [definition, in denote]
denote_bottom_nonvalue [lemma, in denote_bottom_nonvalue]
denote_bottom_nonvalue [lemma, in denote_bottom_nonvalue]
directed [definition, in directed]
directed [library]
DirectedColimit [constructor, in DirectedColimit]
directed_joinables.HBplt [variable, in HBplt]
directed_joinables.A [variable, in A]
directed_joinables.B [variable, in B]
directed_joinables.swell.swell_relation.G [variable, in G]
directed_joinables.M [variable, in M]
directed_joinables.R [variable, in R]
directed_joinables.swell.swell_relation.z [variable, in z]
directed_preord [record, in directed_preord]
directed_joinables.swell.swell_relation.ODAB [variable, in ODAB]
directed_joinables.swell.RSinh [variable, in RSinh]
directed_colimit [record, in directed_colimit]
directed_joinables.swell.swell_relation.noub [variable, in noub]
directed_joinables.swell [section, in swell]
directed_cl [definition, in directed_cl]
directed_joinables [lemma, in directed_joinables]
directed_joinables [section, in directed_joinables]
directed_joinables.Minh [variable, in Minh]
directed_joinables.swell.swell_relation.G0inh [variable, in G0inh]
directed_joinables.swell.swell_relation.G0 [variable, in G0]
directed_joinables.swell.swell_relation.HG [variable, in HG]
directed_joinables.HM [variable, in HM]
directed_joinables.HR [variable, in HR]
directed_joinables.swell.swell_relation.Hz [variable, in Hz]
directed_joinables.OD [variable, in OD]
directed_joinables.HAeff [variable, in HAeff]
directed_hf_cl [definition, in directed_hf_cl]
directed_joinables.RS [variable, in RS]
directed_joinables.swell.RS [variable, in RS]
directed_joinables.swell.swell_relation.XS [variable, in XS]
directed_joinables.HRdir [variable, in HRdir]
directed_system [record, in directed_system]
directed_joinables.hf [variable, in hf]
directed_rel [definition, in directed_rel]
directed_joinables.HBeff [variable, in HBeff]
directed_joinables.swell.swell_relation [section, in swell_relation]
directed_joinables.swell.swell_relation.HG' [variable, in HG']
directed_joinables.swell.swell_relation.HG0 [variable, in HG0]
directed_joinables.swell.HRS [variable, in HRS]
directed_joinables.HAplt [variable, in HAplt]
directed_joinables.swell.swell_relation.HXS [variable, in HXS]
directed_joinables.swell.RS' [variable, in RS']
DirPreord [constructor, in DirPreord]
dirset [abbreviation, in dirset]
DirSys [constructor, in DirSys]
dir_preord [projection, in dir_preord]
dir_effective [projection, in dir_effective]
dir_sys_app [definition, in dir_sys_app]
disc [definition, in disc]
discrete [library]
disc_cases [definition, in disc_cases]
disc_cases [section, in disc_cases]
disc_cases.A [variable, in A]
disc_cases.B [variable, in B]
disc_cases.X [variable, in X]
disc_cases.f [variable, in f]
disc_elem_inj [lemma, in disc_elem_inj]
disc_cases_elem [lemma, in disc_cases_elem]
disc_elem [definition, in disc_elem]
disc_cases_univ [lemma, in disc_cases_univ]
disc_cases_commute [lemma, in disc_cases_commute]
disc_cases_elem' [lemma, in disc_cases_elem']
Distributive [abbreviation, in Distributive]
Distributive [module, in Distributive]
distributive [abbreviation, in distributive]
Distributive.cartesian [definition, in cartesian]
Distributive.cartesian_mixin [projection, in cartesian_mixin]
Distributive.cartesian' [definition, in cartesian']
Distributive.category [definition, in category]
Distributive.cat_axioms [projection, in cat_axioms]
Distributive.cocartesian [definition, in cocartesian]
Distributive.cocartesian_mixin [projection, in cocartesian_mixin]
Distributive.cocartesian' [definition, in cocartesian']
Distributive.comp [definition, in comp]
Distributive.comp_mixin [projection, in comp_mixin]
Distributive.comp' [definition, in comp']
Distributive.Distributive [constructor, in Distributive]
Distributive.distributive [record, in distributive]
Distributive.distributive [section, in distributive]
Distributive.distributive.cartesian [variable, in cartesian]
Distributive.distributive.cat_axioms [variable, in cat_axioms]
Distributive.distributive.cocartesian [variable, in cocartesian]
Distributive.distributive.comp [variable, in comp]
Distributive.distributive.eq [variable, in eq]
Distributive.distributive.hom [variable, in hom]
Distributive.distributive.initialized [variable, in initialized]
Distributive.distributive.ob [variable, in ob]
Distributive.distributive.terminated [variable, in terminated]
Distributive.distrib_law_op [definition, in distrib_law_op]
Distributive.distrib_law [projection, in distrib_law]
Distributive.eq [definition, in eq]
Distributive.eq_mixin [projection, in eq_mixin]
Distributive.eq' [definition, in eq']
Distributive.hom [projection, in hom]
Distributive.initialized [definition, in initialized]
Distributive.initialized_mixin [projection, in initialized_mixin]
Distributive.mixin [projection, in mixin]
Distributive.mixin_of [record, in mixin_of]
Distributive.ob [projection, in ob]
Distributive.terminated [definition, in terminated]
Distributive.terminated_mixin [projection, in terminated_mixin]
distrib_law [abbreviation, in distrib_law]
dom [definition, in dom]
dom [definition, in dom]
ds_compose [projection, in ds_compose]
ds_hom [projection, in ds_hom]
ds_F [projection, in ds_F]
ds_ident [projection, in ds_ident]


E

eapp [constructor, in eapp]
eapp [constructor, in eapp]
eapp1 [constructor, in eapp1]
eapp1 [constructor, in eapp1]
eapp2 [constructor, in eapp2]
eapp2 [constructor, in eapp2]
ebool [constructor, in ebool]
ebool [constructor, in ebool]
ebool [constructor, in ebool]
ebool [constructor, in ebool]
effective [library]
EffectiveOrder [constructor, in EffectiveOrder]
effective_Nord [definition, in effective_Nord]
effective_empty [definition, in effective_empty]
effective_sum [definition, in effective_sum]
effective_order [record, in effective_order]
effective_unit [definition, in effective_unit]
effective_prod [definition, in effective_prod]
effective_lift [definition, in effective_lift]
eff_ord_dec [projection, in eff_ord_dec]
eff_enum [projection, in eff_enum]
eff_in_dec [lemma, in eff_in_dec]
eff_complete [projection, in eff_complete]
eff_to_ord_dec [definition, in eff_to_ord_dec]
efix [constructor, in efix]
eI [constructor, in eI]
eI [constructor, in eI]
eIF [constructor, in eIF]
eIF [constructor, in eIF]
eif [constructor, in eif]
eif [constructor, in eif]
eimage' [definition, in eimage']
einh [constructor, in einh]
einhabited [inductive, in einhabited]
either [abbreviation, in either]
either_univ [lemma, in either_univ]
eK [constructor, in eK]
eK [constructor, in eK]
elam [constructor, in elam]
elam [constructor, in elam]
elem [definition, in elem]
elem [projection, in elem]
elem_inh [lemma, in elem_inh]
elist [definition, in elist]
elist_elem [lemma, in elist_elem]
EMBED [definition, in EMBED]
embed [projection, in embed]
embed [library]
embedding [record, in embedding]
Embedding [constructor, in Embedding]
embedForget [definition, in embedForget]
embed_comp [definition, in embed_comp]
embed_ord [definition, in embed_ord]
embed_func_is_ep_pair [lemma, in embed_func_is_ep_pair]
embed_compose [definition, in embed_compose]
embed_eq_mixin [definition, in embed_eq_mixin]
embed_func_reflects [lemma, in embed_func_reflects]
embed_rel_elem [lemma, in embed_rel_elem]
embed_comp_mixin [definition, in embed_comp_mixin]
embed_hom [definition, in embed_hom]
embed_order_mixin [definition, in embed_order_mixin]
embed_func [definition, in embed_func]
embed_ep_roundtrip1 [lemma, in embed_ep_roundtrip1]
embed_ep_roundtrip2 [lemma, in embed_ep_roundtrip2]
embed_rel [definition, in embed_rel]
embed_unlift [lemma, in embed_unlift]
embed_lift' [lemma, in embed_lift']
embed_directed0 [projection, in embed_directed0]
embed_directed2 [projection, in embed_directed2]
embed_func_directed0 [lemma, in embed_func_directed0]
embed_func_directed2 [lemma, in embed_func_directed2]
embed_order [definition, in embed_order]
embed_ep_pair [definition, in embed_ep_pair]
embed_ident [definition, in embed_ident]
embed_image_inhabited [lemma, in embed_image_inhabited]
embed_reflects [projection, in embed_reflects]
embed_map [projection, in embed_map]
embed_image [definition, in embed_image]
embed_unlift' [lemma, in embed_unlift']
embed_initiate [definition, in embed_initiate]
embed_cat_axioms [lemma, in embed_cat_axioms]
embed_mono [projection, in embed_mono]
embed_lift [lemma, in embed_lift]
empty [definition, in empty]
emptypo [definition, in emptypo]
empty_plotkin [definition, in empty_plotkin]
empty_elem [lemma, in empty_elem]
empty_semidirected [lemma, in empty_semidirected]
empty_dir [definition, in empty_dir]
enumbool [definition, in enumbool]
Enumtype [abbreviation, in Enumtype]
enumtype [abbreviation, in enumtype]
enumtype [module, in enumtype]
enumtype.carrier [projection, in carrier]
enumtype.Enumtype [constructor, in Enumtype]
enumtype.enumtype [record, in enumtype]
enumtype.enumtype_plotkin [definition, in enumtype_plotkin]
enumtype.enumtype_set [projection, in enumtype_set]
enumtype.enumtype_complete [projection, in enumtype_complete]
enumtype.enumtype_has_normals [lemma, in enumtype_has_normals]
enumtype.enumtype_dec [projection, in enumtype_dec]
enumtype.enumtype_effective [definition, in enumtype_effective]
enumtype.eq_mixin [definition, in eq_mixin]
enumtype.ord [definition, in ord]
enumtype.order_discrete [lemma, in order_discrete]
enumtype.preord_mixin [definition, in preord_mixin]
enumtype.setoid [definition, in setoid]
enumtype.strong_eq [lemma, in strong_eq]
enum_lift [definition, in enum_lift]
env [abbreviation, in env]
env [abbreviation, in env]
ENV [module, in ENV]
ENV [module, in ENV]
env_input.A [definition, in A]
env_input.A [definition, in A]
env_input.F [definition, in F]
env_input.F [definition, in F]
env_supp_inenv [lemma, in env_supp_inenv]
env_supp_inenv [lemma, in env_supp_inenv]
env_dec [lemma, in env_dec]
env_dec [lemma, in env_dec]
env_input.Adec [definition, in Adec]
env_input.Adec [definition, in Adec]
env_input [module, in env_input]
env_input [module, in env_input]
epic [section, in epic]
epic.C [variable, in C]
epimorphism [record, in epimorphism]
Epimorphism [constructor, in Epimorphism]
epi_comp_mixin [definition, in epi_comp_mixin]
EPI_COMP [definition, in EPI_COMP]
epi_compose [definition, in epi_compose]
epi_eq [definition, in epi_eq]
epi_id [definition, in epi_id]
epi_axiom [projection, in epi_axiom]
EPI_EQ [definition, in EPI_EQ]
epi_hom [projection, in epi_hom]
epi_cat_axioms [definition, in epi_cat_axioms]
EPI_CAT [definition, in EPI_CAT]
EpPair [constructor, in EpPair]
eprod [definition, in eprod]
eprod_elem [lemma, in eprod_elem]
ep_pairs.embed_func_ep_pair.X [variable, in X]
ep_pairs.ep_pair_embed_func.X [variable, in X]
ep_pairs.embed_func_ep_pair.Y [variable, in Y]
ep_pairs.ep_pair_embed_func.Y [variable, in Y]
ep_pairs.ep_pair_embed_func.e [variable, in e]
ep_pairs.ep_pair_embed_func.p [variable, in p]
ep_pairs.ep_pair_embed_func.embed_func.x [variable, in x]
ep_pairs [section, in ep_pairs]
ep_pair_eq [definition, in ep_pair_eq]
ep_ident [projection, in ep_ident]
ep_embed [definition, in ep_embed]
ep_id [definition, in ep_id]
ep_pairs.embed_func_ep_pair [section, in embed_func_ep_pair]
ep_semidec [lemma, in ep_semidec]
ep_pairs.ep_pair_embed_func.embed_func [section, in embed_func]
ep_pair_comp_mixin [definition, in ep_pair_comp_mixin]
ep_embedding [definition, in ep_embedding]
ep_pair [record, in ep_pair]
ep_pairs.ep_pair_embed_func [section, in ep_pair_embed_func]
ep_cat_axioms [lemma, in ep_cat_axioms]
ep_pair_eq_mixin [definition, in ep_pair_eq_mixin]
ep_pairs.ep_pair_embed_func.ep [variable, in ep]
ep_pairs.hf [variable, in hf]
ep_set [definition, in ep_set]
ep_pair_comp [definition, in ep_pair_comp]
ep_correct [projection, in ep_correct]
ep_pairs.ep_pair_embed_func.Hep [variable, in Hep]
ep_compose [definition, in ep_compose]
ep_pairs.embed_func_ep_pair.embed [variable, in embed]
ep_pair_embed_eq_proj_eq [lemma, in ep_pair_embed_eq_proj_eq]
Eq [module, in Eq]
EqDec [constructor, in EqDec]
eqdec [projection, in eqdec]
eq_ord' [lemma, in eq_ord']
eq_refl [lemma, in eq_refl]
eq_trans [lemma, in eq_trans]
eq_op [definition, in eq_op]
eq_dec [record, in eq_dec]
eq_symm [lemma, in eq_symm]
eq_ord [lemma, in eq_ord]
Eq.carrier [projection, in carrier]
Eq.eq [projection, in eq]
Eq.Mixin [constructor, in Mixin]
Eq.mixin [projection, in mixin]
Eq.mixin_of [record, in mixin_of]
Eq.Pack [constructor, in Pack]
Eq.refl [projection, in refl]
Eq.symm [projection, in symm]
Eq.trans [projection, in trans]
Eq.type [record, in type]
erel [definition, in erel]
erel_inv_image [definition, in erel_inv_image]
erel_inv_image_elem [lemma, in erel_inv_image_elem]
erel_image [definition, in erel_image]
erel_image_elem [lemma, in erel_image_elem]
eS [constructor, in eS]
eS [constructor, in eS]
eset [abbreviation, in eset]
eset [module, in eset]
esets [library]
eset_theory [definition, in eset_theory]
eset.eimage [definition, in eimage]
eset.emember [definition, in emember]
eset.eset [definition, in eset]
eset.eset [section, in eset]
eset.esingle [definition, in esingle]
eset.eunion [definition, in eunion]
eset.mixin [lemma, in mixin]
esubset [definition, in esubset]
esubset_dec [definition, in esubset_dec]
esubset_dec_elem [lemma, in esubset_dec_elem]
esubset_elem [lemma, in esubset_elem]
esum [definition, in esum]
esum_right_elem [lemma, in esum_right_elem]
esum_left_elem [lemma, in esum_left_elem]
eta_semvalue [lemma, in eta_semvalue]
eval [inductive, in eval]
eval [inductive, in eval]
eval [inductive, in eval]
eval [inductive, in eval]
eval_no_redex [lemma, in eval_no_redex]
eval_alpha [lemma, in eval_alpha]
eval_alpha [lemma, in eval_alpha]
eval_app_congruence [lemma, in eval_app_congruence]
eval_app_congruence [lemma, in eval_app_congruence]
eval_eq [lemma, in eval_eq]
eval_eq [lemma, in eval_eq]
eval_eq [lemma, in eval_eq]
eval_eq [lemma, in eval_eq]
eval_trans [lemma, in eval_trans]
eval_trans [lemma, in eval_trans]
eval_trans [lemma, in eval_trans]
eval_trans [lemma, in eval_trans]
eval_lrapp_congruence [lemma, in eval_lrapp_congruence]
eval_lrapp_congruence [lemma, in eval_lrapp_congruence]
eval_value [lemma, in eval_value]
eval_value [lemma, in eval_value]
eval_value [lemma, in eval_value]
eval_value [lemma, in eval_value]
expF [definition, in expF]
expF_decompose [section, in expF_decompose]
expF_decompose.I [variable, in I]
expF_decompose.CC1 [variable, in CC1]
expF_decompose.CC2 [variable, in CC2]
expF_decompose.DS1 [variable, in DS1]
expF_decompose.DS2 [variable, in DS2]
expF_continuous [lemma, in expF_continuous]
expF_decompose.decompose1 [variable, in decompose1]
expF_decompose.decompose2 [variable, in decompose2]
expF_decompose.hf [variable, in hf]
exp_functor.A [variable, in A]
exp_functor.B [variable, in B]
exp_functor.C [variable, in C]
exp_functor.D [variable, in D]
exp_functor.f [variable, in f]
exp_functor.g [variable, in g]
exp_functor [section, in exp_functor]
exp_fmap_ident [lemma, in exp_fmap_ident]
exp_eq_axiom [projection, in exp_eq_axiom]
exp_support [projection, in exp_support]
exp_papp [definition, in exp_papp]
exp_fmap_func [definition, in exp_fmap_func]
exp_functor.hf [variable, in hf]
exp_fmap_respects [lemma, in exp_fmap_respects]
exp_fmap_compose [lemma, in exp_fmap_compose]
exp_support_axiom [projection, in exp_support_axiom]
exp_map [projection, in exp_map]
exp_fmap [definition, in exp_fmap]
exp_functor [library]
extend_shift_alpha [lemma, in extend_shift_alpha]
extend_shift_alpha [lemma, in extend_shift_alpha]
ex_finset_semidec [definition, in ex_finset_semidec]
ex_finset_setdec [definition, in ex_finset_setdec]
eY [constructor, in eY]


F

fconst [definition, in fconst]
fconst_continuous [lemma, in fconst_continuous]
finbool [definition, in finbool]
find_inhabitant' [definition, in find_inhabitant']
find_inhabitant [definition, in find_inhabitant]
FINPROD [module, in FINPROD]
finprod [definition, in finprod]
finprod [module, in finprod]
finprod [library]
FINPROD_INPUT.A [axiom, in A]
FINPROD_INPUT.F [axiom, in F]
FINPROD_INPUT.Adec [axiom, in Adec]
finprod_elem [lemma, in finprod_elem]
FINPROD_INPUT [module, in FINPROD_INPUT]
FINPROD.A [axiom, in A]
FINPROD.Adec [axiom, in Adec]
finprod.bind [definition, in bind]
FINPROD.bind [definition, in bind]
finprod.bind_unbind [lemma, in bind_unbind]
FINPROD.bind_unbind [axiom, in bind_unbind]
finprod.bind_weaken [lemma, in bind_weaken]
finprod.castty [abbreviation, in castty]
finprod.cxt [abbreviation, in cxt]
finprod.empty_cxt_uniq [lemma, in empty_cxt_uniq]
finprod.empty_cxt_le [lemma, in empty_cxt_le]
finprod.empty_cxt_inh [definition, in empty_cxt_inh]
finprod.env [definition, in env]
finprod.env_incl_wk [lemma, in env_incl_wk]
finprod.env_incl [definition, in env_incl]
finprod.env_supp [definition, in env_supp]
finprod.env_supported [definition, in env_supported]
finprod.extend_map [definition, in extend_map]
FINPROD.F [axiom, in F]
finprod.finprod [definition, in finprod]
FINPROD.finprod [axiom, in finprod]
finprod.finprod_proj_commute [lemma, in finprod_proj_commute]
FINPROD.finprod_proj_commute [axiom, in finprod_proj_commute]
finprod.finprod_universal [lemma, in finprod_universal]
FINPROD.finprod_universal [axiom, in finprod_universal]
finprod.inenv [definition, in inenv]
finprod.internals [module, in finprod.internals]
finprod.internals.codom [definition, in codom]
finprod.internals.codom_eff [definition, in codom_eff]
finprod.internals.codom_enum [definition, in codom_enum]
finprod.internals.codom_out [definition, in codom_out]
finprod.internals.codom_in' [definition, in codom_in']
finprod.internals.codom_avoid [constructor, in codom_avoid]
finprod.internals.codom_has_normals [lemma, in codom_has_normals]
finprod.internals.codom_out' [definition, in codom_out']
finprod.internals.codom_elem [constructor, in codom_elem]
finprod.internals.codom_plotkin [definition, in codom_plotkin]
finprod.internals.empty_cxt_rel [definition, in empty_cxt_rel]
finprod.internals.empty_ctx [definition, in empty_ctx]
finprod.internals.enum_finprod_complete [lemma, in enum_finprod_complete]
finprod.internals.enum_finprod [definition, in enum_finprod]
finprod.internals.finprod [definition, in finprod]
finprod.internals.finprod_codom_ord_mixin [definition, in finprod_codom_ord_mixin]
finprod.internals.finprod_univ_rel.X [variable, in X]
finprod.internals.finprod_univ_rel.f [variable, in f]
finprod.internals.finprod_codom_ord [definition, in finprod_codom_ord]
finprod.internals.finprod_univ_commute [lemma, in finprod_univ_commute]
finprod.internals.finprod_univ_axiom [lemma, in finprod_univ_axiom]
finprod.internals.finprod_dec [definition, in finprod_dec]
finprod.internals.finprod_plotkin [definition, in finprod_plotkin]
finprod.internals.finprod_ord_mixin [definition, in finprod_ord_mixin]
finprod.internals.finprod_univ_rel.finprod_univ_rel [variable, in finprod_univ_rel]
finprod.internals.finprod_univ_rel [section, in finprod_univ_rel]
finprod.internals.finprod_univ_rel [definition, in finprod_univ_rel]
finprod.internals.finprod_univ_rel_elem [lemma, in finprod_univ_rel_elem]
finprod.internals.finprod_elem [definition, in finprod_elem]
finprod.internals.finprod_univ_rel.Hf [variable, in Hf]
finprod.internals.finprod_codom_weaken [definition, in finprod_codom_weaken]
finprod.internals.finprod_ord [definition, in finprod_ord]
finprod.internals.finprod_effective [definition, in finprod_effective]
finprod.internals.finprod_has_normals [lemma, in finprod_has_normals]
finprod.internals.finprod_univ_rel.ls [variable, in ls]
finprod.internals.finprod_univ [definition, in finprod_univ]
finprod.internals.finprod_codom [inductive, in finprod_codom]
finprod.internals.finprod_univ_rel.avd [variable, in avd]
finprod.internals.f_cons_mono [lemma, in f_cons_mono]
finprod.internals.f_cons [definition, in f_cons]
finprod.internals.f_cons_hd_tl [lemma, in f_cons_hd_tl]
finprod.internals.f_hd' [definition, in f_hd']
finprod.internals.f_cons_reflects1 [lemma, in f_cons_reflects1]
finprod.internals.f_cons_reflects2 [lemma, in f_cons_reflects2]
finprod.internals.f_hd [definition, in f_hd]
finprod.internals.f_cons' [definition, in f_cons']
finprod.internals.f_tl [definition, in f_tl]
finprod.internals.f_tl' [definition, in f_tl']
finprod.internals.ord [definition, in ord]
finprod.internals.ord_weaken [definition, in ord_weaken]
finprod.internals.proj [definition, in proj]
finprod.internals.proj_rel_elem [lemma, in proj_rel_elem]
finprod.internals.proj_rel [definition, in proj_rel]
finprod.lookup [definition, in lookup]
FINPROD.lookup [definition, in lookup]
finprod.lookup_eq [lemma, in lookup_eq]
FINPROD.lookup_eq [lemma, in lookup_eq]
finprod.lookup_app [lemma, in lookup_app]
finprod.lookup_neq [lemma, in lookup_neq]
FINPROD.lookup_neq [lemma, in lookup_neq]
finprod.mk_finprod [definition, in mk_finprod]
FINPROD.mk_finprod [axiom, in mk_finprod]
finprod.mk_finprod_compose_commute [lemma, in mk_finprod_compose_commute]
FINPROD.mk_finprod_compose_commute [axiom, in mk_finprod_compose_commute]
finprod.newestvar [definition, in newestvar]
finprod.proj [definition, in proj]
FINPROD.proj [axiom, in proj]
finprod.proj_bind_neq [lemma, in proj_bind_neq]
FINPROD.proj_bind_neq [axiom, in proj_bind_neq]
finprod.proj_weaken [lemma, in proj_weaken]
finprod.proj_bind [lemma, in proj_bind]
FINPROD.proj_bind [axiom, in proj_bind]
finprod.proj_bind_eq [lemma, in proj_bind_eq]
FINPROD.proj_bind_eq [axiom, in proj_bind_eq]
finprod.shift_vars' [lemma, in shift_vars']
finprod.shift_vars [definition, in shift_vars]
finprod.subst [definition, in subst]
finprod.subst_soundness_lemma [lemma, in subst_soundness_lemma]
finprod.subst_denote [definition, in subst_denote]
finprod.subst_soundness [lemma, in subst_soundness]
finprod.TermModel [constructor, in TermModel]
finprod.termmodel [section, in termmodel]
finprod.termmodel [record, in termmodel]
finprod.termmodel.tm [variable, in tm]
finprod.termmodel.varmap_compose.f [variable, in f]
finprod.termmodel.varmap_compose.g [variable, in g]
finprod.termmodel.varmap_compose [section, in varmap_compose]
finprod.termmodel.varmap_compose.Γ₁ [variable, in Γ₁]
finprod.termmodel.varmap_compose.Γ₂ [variable, in Γ₂]
finprod.termmodel.varmap_compose.Γ₃ [variable, in Γ₃]
finprod.term_subst_soundness [lemma, in term_subst_soundness]
finprod.tm_denote_var [projection, in tm_denote_var]
finprod.tm_traverse [projection, in tm_traverse]
finprod.tm_wk [definition, in tm_wk]
finprod.tm_traverse_correct [projection, in tm_traverse_correct]
finprod.tm_subst [definition, in tm_subst]
finprod.tm_var [projection, in tm_var]
finprod.tm_denote [projection, in tm_denote]
finprod.ty [definition, in ty]
FINPROD.ty [definition, in ty]
finprod.unbind [definition, in unbind]
FINPROD.unbind [definition, in unbind]
finprod.unbind_lemma [lemma, in unbind_lemma]
FINPROD.unbind_lemma [lemma, in unbind_lemma]
finprod.varmap [definition, in varmap]
finprod.varmap [section, in varmap]
finprod.varmap_denote [definition, in varmap_denote]
finprod.varmap_compose [definition, in varmap_compose]
finprod.varmap_extend_bind [lemma, in varmap_extend_bind]
finprod.varmap_compose_denote [lemma, in varmap_compose_denote]
finprod.varmap_shift_bind [lemma, in varmap_shift_bind]
finprod.varmap_denote_proj [lemma, in varmap_denote_proj]
finprod.varmap_var_id [lemma, in varmap_var_id]
finprod.varmap.tm [variable, in tm]
finprod.varmap.tm_weaken [variable, in tm_weaken]
finprod.varmap.tm_var [variable, in tm_var]
finprod.weaken_fresh [lemma, in weaken_fresh]
finprod.weaken_map [definition, in weaken_map]
finprod.weaken_denote [definition, in weaken_denote]
finprod.weaken_map_denote [lemma, in weaken_map_denote]
finprod.weaken_term_denote [lemma, in weaken_term_denote]
finrel_decompose [lemma, in finrel_decompose]
finset [abbreviation, in finset]
finset [module, in finset]
finsets [library]
finset_sub_image [lemma, in finset_sub_image]
finset_remove_elem [lemma, in finset_remove_elem]
finset_remove_length1 [lemma, in finset_remove_length1]
finset_remove_length2 [lemma, in finset_remove_length2]
finset_in_dec [lemma, in finset_in_dec]
finset_theory [definition, in finset_theory]
finset_remove [definition, in finset_remove]
finset_decompose [lemma, in finset_decompose]
finset_dec [definition, in finset_dec]
finset_find_dec' [lemma, in finset_find_dec']
finset_cons_eq [lemma, in finset_cons_eq]
finset_find_dec [lemma, in finset_find_dec]
finset.fimage [definition, in fimage]
finset.finset [section, in finset]
finset.fmember [definition, in fmember]
finset.fset [definition, in fset]
finset.fsingle [definition, in fsingle]
finset.funion [definition, in funion]
finset.mixin [definition, in mixin]
finsubset [definition, in finsubset]
finsubset [section, in finsubset]
finsubsets [definition, in finsubsets]
finsubsets_complete [lemma, in finsubsets_complete]
finsubset_dec' [lemma, in finsubset_dec']
finsubset_elem [lemma, in finsubset_elem]
finsubset_dec [lemma, in finsubset_dec]
finsubset.A [variable, in A]
finsubset.Hdec [variable, in Hdec]
finsubset.HP [variable, in HP]
finsubset.P [variable, in P]
finsum [definition, in finsum]
finsum_right_elem [lemma, in finsum_right_elem]
finsum_left_elem [lemma, in finsum_left_elem]
fintype [abbreviation, in fintype]
fintype [module, in fintype]
Fintype [abbreviation, in Fintype]
fintype.carrier [projection, in carrier]
fintype.eq_mixin [definition, in eq_mixin]
fintype.fintype [record, in fintype]
fintype.Fintype [constructor, in Fintype]
fintype.fintype_effective [definition, in fintype_effective]
fintype.fintype_list [projection, in fintype_list]
fintype.fintype_complete [projection, in fintype_complete]
fintype.fintype_plotkin [definition, in fintype_plotkin]
fintype.fintype_has_normals [definition, in fintype_has_normals]
fintype.fintype_dec [projection, in fintype_dec]
fintype.ord [definition, in ord]
fintype.order_discrete [lemma, in order_discrete]
fintype.preord_mixin [definition, in preord_mixin]
fintype.setoid [definition, in setoid]
fintype.strong_eq [lemma, in strong_eq]
fin_intersect [definition, in fin_intersect]
fin_list_intersect [definition, in fin_list_intersect]
fin_list_intersect_elem [lemma, in fin_list_intersect_elem]
fin_intersect_elem [lemma, in fin_intersect_elem]
fixes [definition, in fixes]
fixes [section, in fixes]
fixes [library]
fixes_step [definition, in fixes_step]
fixes_mono [lemma, in fixes_mono]
fixes_eq [lemma, in fixes_eq]
fixes_step' [definition, in fixes_step']
fixes_unroll [lemma, in fixes_unroll]
fixes_compose_commute [lemma, in fixes_compose_commute]
fixes.A [variable, in A]
fixes.f [variable, in f]
fixes.Γ [variable, in Γ]
fixpoint [definition, in fixpoint]
fixpoint [section, in fixpoint]
fixpoint [definition, in fixpoint]
fixpoint [section, in fixpoint]
fixpoint [definition, in fixpoint]
fixpoint_alt_iso [definition, in fixpoint_alt_iso]
fixpoint_iso [definition, in fixpoint_iso]
fixpoint_iso [definition, in fixpoint_iso]
fixpoint_iso [definition, in fixpoint_iso]
fixpoint_alg [definition, in fixpoint_alg]
fixpoint_alt [definition, in fixpoint_alt]
fixpoint_embed [definition, in fixpoint_embed]
fixpoint_alt_out_in [lemma, in fixpoint_alt_out_in]
fixpoint_alt_in_out [lemma, in fixpoint_alt_in_out]
fixpoint_initial [definition, in fixpoint_initial]
fixpoint_initial [definition, in fixpoint_initial]
fixpoint_initial [definition, in fixpoint_initial]
fixpoint_alt_in [definition, in fixpoint_alt_in]
fixpoint_alt_out [definition, in fixpoint_alt_out]
fixpoint.BL [variable, in BL]
fixpoint.C [variable, in C]
fixpoint.cata [section, in cata]
fixpoint.cata.AG [variable, in AG]
fixpoint.colimit_cocone [variable, in colimit_cocone]
fixpoint.F [variable, in F]
fixpoint.F [variable, in F]
fixpoint.Fcontinuous [variable, in Fcontinuous]
fixpoint.Fcontinuous [variable, in Fcontinuous]
fixpoint.has_colimits [variable, in has_colimits]
fix_not_value [lemma, in fix_not_value]
flat [definition, in flat]
flat [library]
flat_cases.A [variable, in A]
flat_cases.B [variable, in B]
flat_cases.X [variable, in X]
flat_cases'_strict [lemma, in flat_cases'_strict]
flat_cases.f [variable, in f]
flat_cases [definition, in flat_cases]
flat_cases [section, in flat_cases]
flat_cases' [definition, in flat_cases']
flat_cases_elem' [lemma, in flat_cases_elem']
flat_cases'_semvalue [lemma, in flat_cases'_semvalue]
flat_cases_univ' [lemma, in flat_cases_univ']
flat_cases_rel_elem [lemma, in flat_cases_rel_elem]
flat_cases_univ [lemma, in flat_cases_univ]
flat_elem'_ignores_arg [lemma, in flat_elem'_ignores_arg]
flat_elem'_inj [lemma, in flat_elem'_inj]
flat_cases_rel [definition, in flat_cases_rel]
flat_elem_inj [lemma, in flat_elem_inj]
flat_elem_canon [lemma, in flat_elem_canon]
flat_elem'_semvalue [lemma, in flat_elem'_semvalue]
flat_elem' [definition, in flat_elem']
flat_elem [definition, in flat_elem]
flat_cases_commute [lemma, in flat_cases_commute]
flat_cases_commute [lemma, in flat_cases_commute]
flat_cases_elem [lemma, in flat_cases_elem]
forgetEMBED [definition, in forgetEMBED]
forgetEMBED_map [definition, in forgetEMBED_map]
forgetEMBED_continuous [lemma, in forgetEMBED_continuous]
forgetPLT [definition, in forgetPLT]
forgetPLT_ob [definition, in forgetPLT_ob]
forgetPLT_map [definition, in forgetPLT_map]
fresh [section, in fresh]
fresh_atom_is_fresh' [lemma, in fresh_atom_is_fresh']
fresh_atom_is_fresh [lemma, in fresh_atom_is_fresh]
fresh_idents_inhabited [lemma, in fresh_idents_inhabited]
fresh_atom [definition, in fresh_atom]
fresh_idents [definition, in fresh_idents]
fresh.atoms [variable, in atoms]
fstF [definition, in fstF]
fstF_continuous [lemma, in fstF_continuous]
fstF_continuous [section, in fstF_continuous]
fstF_continuous.C [variable, in C]
fstF_continuous.D [variable, in D]
fstF_continuous.I [variable, in I]
fstF_cocone [definition, in fstF_cocone]
fstF_continuous' [lemma, in fstF_continuous']
fstF_continuous.CC [variable, in CC]
fstF_continuous.DS [variable, in DS]
fstF_continuous.Hcolim [variable, in Hcolim]
fstF_univ [definition, in fstF_univ]
FUNC [definition, in FUNC]
FuncComp [definition, in FuncComp]
functor [abbreviation, in functor]
Functor [abbreviation, in Functor]
Functor [module, in Functor]
FunctorCompose [definition, in FunctorCompose]
FunctorIdent [definition, in FunctorIdent]
functor_compose.C [variable, in C]
functor_compose.D [variable, in D]
functor_compose.E [variable, in E]
functor_compose [section, in functor_compose]
Functor.compose [projection, in compose]
Functor.functor [record, in functor]
Functor.functor [section, in functor]
Functor.Functor [constructor, in Functor]
Functor.functor.C [variable, in C]
Functor.functor.D [variable, in D]
Functor.hom_map [projection, in hom_map]
Functor.ident [projection, in ident]
Functor.ob_map [projection, in ob_map]
Functor.respects [projection, in respects]
fundamental_lemma [lemma, in fundamental_lemma]
fundamental_lemma [lemma, in fundamental_lemma]
fundamental_lemma [lemma, in fundamental_lemma]
fundamental_lemma [lemma, in fundamental_lemma]
fundamental_lemma' [lemma, in fundamental_lemma']
fundamental_lemma' [lemma, in fundamental_lemma']
fundamental_lemma' [lemma, in fundamental_lemma']
fundamental_lemma' [lemma, in fundamental_lemma']
f_explode [lemma, in f_explode]


G

greatest_lower_bound [definition, in greatest_lower_bound]
groupoid [abbreviation, in groupoid]
Groupoid [abbreviation, in Groupoid]
Groupoid [module, in Groupoid]
Groupoid.Axioms [constructor, in Axioms]
Groupoid.axioms [record, in axioms]
Groupoid.category [definition, in category]
Groupoid.cat_axioms [projection, in cat_axioms]
Groupoid.comp [definition, in comp]
Groupoid.comp_mixin [projection, in comp_mixin]
Groupoid.comp' [definition, in comp']
Groupoid.eq [definition, in eq]
Groupoid.eq_mixin [projection, in eq_mixin]
Groupoid.eq' [definition, in eq']
Groupoid.groupoid [record, in groupoid]
Groupoid.groupoid [section, in groupoid]
Groupoid.Groupoid [constructor, in Groupoid]
Groupoid.groupoid_axioms [projection, in groupoid_axioms]
Groupoid.groupoid.axioms [section, in axioms]
Groupoid.groupoid.axioms.inv [variable, in inv]
Groupoid.groupoid.cat_axioms [variable, in cat_axioms]
Groupoid.groupoid.comp [variable, in comp]
Groupoid.groupoid.eq [variable, in eq]
Groupoid.groupoid.hom [variable, in hom]
Groupoid.groupoid.ob [variable, in ob]
Groupoid.hom [projection, in hom]
Groupoid.inv [projection, in inv]
Groupoid.inv_op [definition, in inv_op]
Groupoid.inv_id1 [projection, in inv_id1]
Groupoid.inv_id2 [projection, in inv_id2]
Groupoid.Mixin [constructor, in Mixin]
Groupoid.mixin [projection, in mixin]
Groupoid.mixin_of [record, in mixin_of]
Groupoid.ob [projection, in ob]


H

has_normals [definition, in has_normals]
hom [abbreviation, in hom]
hom [abbreviation, in hom]
HOM [definition, in HOM]
homl [abbreviation, in homl]
hommap [projection, in hommap]
hommap_eq [projection, in hommap_eq]
hommap_axiom [projection, in hommap_axiom]
homr [abbreviation, in homr]
hom_eq [definition, in hom_eq]
hom_rel_pair_map [lemma, in hom_rel_pair_map]
hom_order [definition, in hom_order]
hom1_ident [definition, in hom1_ident]
hom1_compose [definition, in hom1_compose]
hom2 [abbreviation, in hom2]
HSle0 [lemma, in HSle0]


I

identF_continuous [lemma, in identF_continuous]
idents_length.len [variable, in len]
idents_find_len_aux [lemma, in idents_find_len_aux]
idents_wf [definition, in idents_wf]
idents_out [definition, in idents_out]
idents_length.len0 [variable, in len0]
idents_step [definition, in idents_step]
idents_inv [definition, in idents_inv]
idents_set [definition, in idents_set]
idents_length [section, in idents_length]
idents_find [lemma, in idents_find]
ident_ordering [lemma, in ident_ordering]
ident_image_dir [lemma, in ident_image_dir]
ident_op [definition, in ident_op]
ident_rel [definition, in ident_rel]
ident_elem [lemma, in ident_elem]
idx [projection, in idx]
if_not_value [lemma, in if_not_value]
if_not_value [lemma, in if_not_value]
image [definition, in image]
image_compose.A [variable, in A]
image_compose.B [variable, in B]
image_compose.C [variable, in C]
image_compose.T [variable, in T]
image_compose.f [variable, in f]
image_compose.g [variable, in g]
image_axiom0 [lemma, in image_axiom0]
image_axiom1 [lemma, in image_axiom1]
image_axiom2 [lemma, in image_axiom2]
image_compose.XS [variable, in XS]
image_axiom1' [lemma, in image_axiom1']
image_compose [lemma, in image_compose]
image_compose [section, in image_compose]
incl [definition, in incl]
incl_refl [lemma, in incl_refl]
incl_unlift [lemma, in incl_unlift]
incl_trans [lemma, in incl_trans]
inenv [abbreviation, in inenv]
inenv [abbreviation, in inenv]
inenv_varcong [lemma, in inenv_varcong]
inenv_varcong [lemma, in inenv_varcong]
inert [inductive, in inert]
inert_IF1 [constructor, in inert_IF1]
inert_IF2 [constructor, in inert_IF2]
inert_S1 [constructor, in inert_S1]
inert_S2 [constructor, in inert_S2]
inert_K [constructor, in inert_K]
inert_Y [constructor, in inert_Y]
inert_semvalue [lemma, in inert_semvalue]
inflate [definition, in inflate]
inflate' [definition, in inflate']
inh [definition, in inh]
inhabited [definition, in inhabited]
inhabited_einhabited [lemma, in inhabited_einhabited]
inh_eq [lemma, in inh_eq]
inh_sub [lemma, in inh_sub]
inh_image [lemma, in inh_image]
inh_dec [lemma, in inh_dec]
Initialized [abbreviation, in Initialized]
Initialized [module, in Initialized]
initialized [abbreviation, in initialized]
initialized_mixin [definition, in initialized_mixin]
initialized_nominal [definition, in initialized_nominal]
Initialized.axiom [projection, in axiom]
Initialized.category [definition, in category]
Initialized.cat_axioms [projection, in cat_axioms]
Initialized.comp [definition, in comp]
Initialized.comp_mixin [projection, in comp_mixin]
Initialized.eq [definition, in eq]
Initialized.eq_mixin [projection, in eq_mixin]
Initialized.eq' [definition, in eq']
Initialized.hom [projection, in hom]
Initialized.Initialized [constructor, in Initialized]
Initialized.initialized [record, in initialized]
Initialized.initialized [section, in initialized]
Initialized.initialized.eq [variable, in eq]
Initialized.initialized.hom [variable, in hom]
Initialized.initialized.ob [variable, in ob]
Initialized.initiate [projection, in initiate]
Initialized.initiate_op [definition, in initiate_op]
Initialized.initium [projection, in initium]
Initialized.initium_op [definition, in initium_op]
Initialized.Mixin [constructor, in Mixin]
Initialized.mixin [projection, in mixin]
Initialized.mixin_of [record, in mixin_of]
Initialized.ob [projection, in ob]
initiate [abbreviation, in initiate]
initiate [definition, in initiate]
initiate_univ [lemma, in initiate_univ]
initius [definition, in initius]
initius_mixin [definition, in initius_mixin]
initius_eq_mixin [definition, in initius_eq_mixin]
injectA [definition, in injectA]
inj_pair2_ty [lemma, in inj_pair2_ty]
inj_pair2_ty [lemma, in inj_pair2_ty]
inj_pair2_ty [lemma, in inj_pair2_ty]
inj_pair2_ty [lemma, in inj_pair2_ty]
inl_commute [lemma, in inl_commute]
inr_commute [lemma, in inr_commute]
insert_index [definition, in insert_index]
insert_index [definition, in insert_index]
inset_decset [definition, in inset_decset]
intersection [definition, in intersection]
intersection_elem [lemma, in intersection_elem]
intersect_approx [lemma, in intersect_approx]
inv_compose [lemma, in inv_compose]
inv_id1 [lemma, in inv_id1]
inv_id2 [lemma, in inv_id2]
inv_inj [lemma, in inv_inj]
inv_inv [lemma, in inv_inv]
inv_eq [lemma, in inv_eq]
in_unlift [lemma, in in_unlift]
iota1_dir [lemma, in iota1_dir]
iota1_cases_commute [lemma, in iota1_cases_commute]
iota1_elem [lemma, in iota1_elem]
iota1_ordering [lemma, in iota1_ordering]
iota1_rel [definition, in iota1_rel]
iota2_elem [lemma, in iota2_elem]
iota2_ordering [lemma, in iota2_ordering]
iota2_cases_commute [lemma, in iota2_cases_commute]
iota2_rel [definition, in iota2_rel]
iota2_dir [lemma, in iota2_dir]
IsEP [constructor, in IsEP]
Iset [definition, in Iset]
iso [section, in iso]
isomorphism [record, in isomorphism]
Isomorphism [constructor, in Isomorphism]
iso_groupoid_mixin [definition, in iso_groupoid_mixin]
iso_cat_axioms [definition, in iso_cat_axioms]
iso_axiom1 [projection, in iso_axiom1]
iso_axiom2 [projection, in iso_axiom2]
iso_hom'' [definition, in iso_hom'']
iso_hom [projection, in iso_hom]
iso_comp_mixin [definition, in iso_comp_mixin]
iso_eq [definition, in iso_eq]
iso_inv [projection, in iso_inv]
iso_id [definition, in iso_id]
iso_hom' [definition, in iso_hom']
iso_compose [definition, in iso_compose]
iso_inverse [definition, in iso_inverse]
ISO_GROUPOID [definition, in ISO_GROUPOID]
iso.C [variable, in C]
is_ep_pair [record, in is_ep_pair]
is_joinable_unmap_rel [lemma, in is_joinable_unmap_rel]
is_joinable_relation [definition, in is_joinable_relation]
is_joinable_rel_dec [lemma, in is_joinable_rel_dec]
is_joinable_rel_dec' [lemma, in is_joinable_rel_dec']
is_joinable_rel_dec0 [lemma, in is_joinable_rel_dec0]
is_joinable_map_rel [lemma, in is_joinable_map_rel]
is_mub_complete [definition, in is_mub_complete]
iterF [definition, in iterF]
iterF [definition, in iterF]
iter_chain.X [variable, in X]
iter_le [lemma, in iter_le]
iter_hom_proof_irr [lemma, in iter_hom_proof_irr]
iter_hom_proof_irr [lemma, in iter_hom_proof_irr]
iter_chain_base [lemma, in iter_chain_base]
iter_chain.base [variable, in base]
iter_chain.step_base [variable, in step_base]
iter_set_directed [lemma, in iter_set_directed]
iter_chain [definition, in iter_chain]
iter_chain [section, in iter_chain]
iter_hom [definition, in iter_hom]
iter_hom [definition, in iter_hom]
iter_chain_set [definition, in iter_chain_set]
iter_chain_step [lemma, in iter_chain_step]
iter_chain.step [variable, in step]
iter_chain.hf [variable, in hf]
iter_chain.step_mono [variable, in step_mono]


J

joinable [library]
joinable_plt.HBplt [variable, in HBplt]
joinable_plt.A [variable, in A]
joinable_plt.B [variable, in B]
joinable_plt.join_rel_normal.P [variable, in P]
joinable_plt.join_rel_normal.Q [variable, in Q]
joinable_rel_ord_mixin [definition, in joinable_rel_ord_mixin]
joinable_relation [definition, in joinable_relation]
joinable_rel_order [definition, in joinable_rel_order]
joinable_rel_effective [definition, in joinable_rel_effective]
joinable_plt.join_rel_normal [section, in join_rel_normal]
joinable_plt.join_rel_normal.HP [variable, in HP]
joinable_plt.join_rel_normal.HQ [variable, in HQ]
joinable_plt.HAeff [variable, in HAeff]
joinable_ord_dec [lemma, in joinable_ord_dec]
joinable_plt.hf [variable, in hf]
joinable_rels_normal [lemma, in joinable_rels_normal]
joinable_plt.HBeff [variable, in HBeff]
joinable_rel_ord [definition, in joinable_rel_ord]
joinable_rel_plt [definition, in joinable_rel_plt]
joinable_plt.HAplt [variable, in HAplt]
joinable_rel_has_normals [lemma, in joinable_rel_has_normals]
joinable_plt [section, in joinable_plt]


K

kleene_chain [definition, in kleene_chain]
kleene_chain_alt [definition, in kleene_chain_alt]


L

L [abbreviation, in L]
lamModelCBN [definition, in lamModelCBN]
lamModelCBN_iso [lemma, in lamModelCBN_iso]
lamModelCBV [definition, in lamModelCBV]
lamModelCBV_iso [lemma, in lamModelCBV_iso]
lam_termmodel [definition, in lam_termmodel]
lam_termmodel [definition, in lam_termmodel]
lam_models [library]
Le [abbreviation, in Le]
least_upper_bound [definition, in least_upper_bound]
left_right_finset_finsum [lemma, in left_right_finset_finsum]
left_finset_elem [lemma, in left_finset_elem]
left_whisker [definition, in left_whisker]
left_finset [definition, in left_finset]
lfp [definition, in lfp]
lfp [section, in lfp]
lfp_fixpoint [lemma, in lfp_fixpoint]
lfp_least [lemma, in lfp_least]
lfp_uniform [lemma, in lfp_uniform]
lfp.f [variable, in f]
lfp.Hpointed [variable, in Hpointed]
lfp.X [variable, in X]
lib_eq [definition, in lib_eq]
lift [definition, in lift]
lift [definition, in lift]
liftEMBED [definition, in liftEMBED]
liftEMBED_map [definition, in liftEMBED_map]
liftEMBED_continuous [lemma, in liftEMBED_continuous]
liftF [definition, in liftF]
liftPPLT [definition, in liftPPLT]
liftPPLT_rel_elem [lemma, in liftPPLT_rel_elem]
liftPPLT_ob [definition, in liftPPLT_ob]
liftPPLT_rel [definition, in liftPPLT_rel]
liftPPLT_map [definition, in liftPPLT_map]
liftup [definition, in liftup]
lift_prod'_natural [lemma, in lift_prod'_natural]
lift_plt_pointed [instance, in lift_plt_pointed]
lift_prod_pair' [lemma, in lift_prod_pair']
lift_unit [definition, in lift_unit]
lift_map [definition, in lift_map]
lift_unit' [definition, in lift_unit']
lift_mub_closure [definition, in lift_mub_closure]
lift_plotkin [definition, in lift_plotkin]
lift_prod_pair [lemma, in lift_prod_pair]
lift_map_eq [lemma, in lift_map_eq]
lift_mixin [definition, in lift_mixin]
lift_map_id [lemma, in lift_map_id]
lift_unit_id1 [lemma, in lift_unit_id1]
lift_unit_id2 [lemma, in lift_unit_id2]
lift_ord [definition, in lift_ord]
lift_prod_natural [lemma, in lift_prod_natural]
lift_has_normals [lemma, in lift_has_normals]
lift_prod [definition, in lift_prod]
lift_map_compose [lemma, in lift_map_compose]
lift_prod' [definition, in lift_prod']
lift_prod_id1 [lemma, in lift_prod_id1]
lift_prod_id2 [lemma, in lift_prod_id2]
limord [definition, in limord]
limord_univ [definition, in limord_univ]
limord_univ_uniq [lemma, in limord_univ_uniq]
limord_effective [definition, in limord_effective]
limord_mixin [definition, in limord_mixin]
limord_univ_commute [lemma, in limord_univ_commute]
limord_plotkin [definition, in limord_plotkin]
limord_has_normals [lemma, in limord_has_normals]
LimSet [constructor, in LimSet]
limset [record, in limset]
limset_spoke_commute [lemma, in limset_spoke_commute]
limset_enum [definition, in limset_enum]
limset_spoke [definition, in limset_spoke]
limset_order_trans [lemma, in limset_order_trans]
limset_order_dec [lemma, in limset_order_dec]
limset_order_exists_forall [lemma, in limset_order_exists_forall]
limset_order_refl [lemma, in limset_order_refl]
limset_order [definition, in limset_order]
list_finsubsets [definition, in list_finsubsets]
list_finsubsets_complete [lemma, in list_finsubsets_complete]
list_finsubsets_correct [lemma, in list_finsubsets_correct]
Lower [constructor, in Lower]
lower_bound [definition, in lower_bound]
lower_set [definition, in lower_set]
LR [definition, in LR]
LR [definition, in LR]
LR [definition, in LR]
LR [definition, in LR]
lrapp [definition, in lrapp]
lrapp [definition, in lrapp]
lrhyps [definition, in lrhyps]
lrhyps [definition, in lrhyps]
lrsem [definition, in lrsem]
lrsem [definition, in lrsem]
lrsemapp [definition, in lrsemapp]
lrsemapp [definition, in lrsemapp]
lrsemapp_equiv [lemma, in lrsemapp_equiv]
lrsemapp_equiv [lemma, in lrsemapp_equiv]
lrsyn [definition, in lrsyn]
lrsyn [definition, in lrsyn]
lrtys [definition, in lrtys]
lrtys [definition, in lrtys]
LR_IF [lemma, in LR_IF]
LR_IF [lemma, in LR_IF]
LR_I [lemma, in LR_I]
LR_I [lemma, in LR_I]
LR_K [lemma, in LR_K]
LR_K [lemma, in LR_K]
LR_S [lemma, in LR_S]
LR_S [lemma, in LR_S]
LR_Y [lemma, in LR_Y]
LR_Ybody [lemma, in LR_Ybody]
LR_admissible [lemma, in LR_admissible]
LR_admissible [lemma, in LR_admissible]
LR_alpha_cong [lemma, in LR_alpha_cong]
LR_under_apply [lemma, in LR_under_apply]
LR_under_apply [lemma, in LR_under_apply]
LR_equiv [lemma, in LR_equiv]
LR_equiv [lemma, in LR_equiv]
LR_equiv [lemma, in LR_equiv]
LR_equiv [lemma, in LR_equiv]
L_reflects [lemma, in L_reflects]
L_mono [lemma, in L_mono]
L_hom_rel [lemma, in L_hom_rel]


M

map_rel.f [variable, in f]
map_rel.g [variable, in g]
map_rel_in [lemma, in map_rel_in]
map_rel [definition, in map_rel]
map_rel [section, in map_rel]
map_indexes [definition, in map_indexes]
map_rel_inh [lemma, in map_rel_inh]
maximal_lower_bound [definition, in maximal_lower_bound]
max_len [definition, in max_len]
max_len_le [lemma, in max_len_le]
maybe [definition, in maybe]
member_eq [lemma, in member_eq]
member_inhabited [lemma, in member_inhabited]
minimal_upper_bound_ok [lemma, in minimal_upper_bound_ok]
minimal_upper_bound [definition, in minimal_upper_bound]
mkrel [definition, in mkrel]
mkrel_ord [lemma, in mkrel_ord]
mkrel_mono [lemma, in mkrel_mono]
mkrel_mono' [lemma, in mkrel_mono']
mkrel_dec [lemma, in mkrel_dec]
mkrel_dir [lemma, in mkrel_dir]
mk_pair [definition, in mk_pair]
mk_disc_cases_rel [definition, in mk_disc_cases_rel]
mk_disc_cases_elem [lemma, in mk_disc_cases_elem]
mono [section, in mono]
monomorphism [record, in monomorphism]
Monomorphism [constructor, in Monomorphism]
mono_cat_axioms [definition, in mono_cat_axioms]
MONO_COMP [definition, in MONO_COMP]
mono_compose [definition, in mono_compose]
mono_comp_mixin [definition, in mono_comp_mixin]
MONO_EQ [definition, in MONO_EQ]
MONO_CAT [definition, in MONO_CAT]
mono_axiom [projection, in mono_axiom]
mono_eq [definition, in mono_eq]
mono_id [definition, in mono_id]
mono_hom [projection, in mono_hom]
mono.C [variable, in C]
mub_finset_dec [lemma, in mub_finset_dec]
mub_closure [projection, in mub_closure]
mub_clos_smallest [projection, in mub_clos_smallest]
mub_closed [definition, in mub_closed]
mub_clos_mub [projection, in mub_clos_mub]
mub_complete [projection, in mub_complete]
mub_clos_idem [lemma, in mub_clos_idem]
mub_closed_intersect [lemma, in mub_closed_intersect]
mub_clos_mono [lemma, in mub_clos_mono]
mub_clos_incl [projection, in mub_clos_incl]
mub_closed_normal_set [lemma, in mub_closed_normal_set]


N

nat_dirord [definition, in nat_dirord]
nat_ord [definition, in nat_ord]
nat_eff [definition, in nat_eff]
Ndisc_ord [definition, in Ndisc_ord]
ne_finsubsets_complete [lemma, in ne_finsubsets_complete]
ne_finsubsets [definition, in ne_finsubsets]
nil_subset [lemma, in nil_subset]
nil_elem [lemma, in nil_elem]
Niter_succ [lemma, in Niter_succ]
NomColim [constructor, in NomColim]
NomExp [constructor, in NomExp]
nominal [abbreviation, in nominal]
NOMINAL [abbreviation, in NOMINAL]
Nominal [module, in Nominal]
nominal [library]
nominal_fixpoint.F [variable, in F]
nominal_directed_colimits.I [variable, in I]
nominal_directed_colimits.DS [variable, in DS]
nominal_fixpoint.HF [variable, in HF]
nominal_directed_colimits [section, in nominal_directed_colimits]
nominal_directed_colimits.nom_colimit_univ.YC [variable, in YC]
nominal_directed_colimits.nom_colimit_univ [section, in nom_colimit_univ]
nominal_fixpoint [section, in nominal_fixpoint]
Nominal.carrier [projection, in carrier]
Nominal.category_axioms [lemma, in category_axioms]
Nominal.comp [definition, in comp]
Nominal.compose [definition, in compose]
Nominal.comp_mixin [definition, in comp_mixin]
Nominal.eq [definition, in eq]
Nominal.equivariant [projection, in equivariant]
Nominal.eq_mixin [projection, in eq_mixin]
Nominal.eq_axiom [projection, in eq_axiom]
Nominal.hom [record, in hom]
Nominal.Hom [constructor, in Hom]
Nominal.hom_eq [definition, in hom_eq]
Nominal.hom_eq_mixin [definition, in hom_eq_mixin]
Nominal.ident [definition, in ident]
Nominal.map [projection, in map]
Nominal.Mixin [constructor, in Mixin]
Nominal.mixin_of [record, in mixin_of]
Nominal.NOMINAL [definition, in NOMINAL]
Nominal.nominal_mixin [projection, in nominal_mixin]
Nominal.nom_support [definition, in nom_support]
Nominal.nom_ident [projection, in nom_ident]
Nominal.nom_comp [projection, in nom_comp]
Nominal.Ob [constructor, in Ob]
Nominal.ob [record, in ob]
Nominal.ob_eq [definition, in ob_eq]
Nominal.papp [projection, in papp]
Nominal.papp_op [definition, in papp_op]
Nominal.papp_respects [projection, in papp_respects]
Nominal.support [projection, in support]
Nominal.support_axiom [projection, in support_axiom]
Nominal.support_op [definition, in support_op]
Nominal.support_papp [projection, in support_papp]
nom_sum_papp [definition, in nom_sum_papp]
nom_compose' [lemma, in nom_compose']
nom_sum.A [variable, in A]
nom_sum.B [variable, in B]
nom_compose [lemma, in nom_compose]
nom_terminated_mixin [definition, in nom_terminated_mixin]
nom_terminated [definition, in nom_terminated]
nom_has_colimits [definition, in nom_has_colimits]
nom_ident' [lemma, in nom_ident']
nom_colimit_papp [definition, in nom_colimit_papp]
nom_sum [definition, in nom_sum]
nom_sum [section, in nom_sum]
nom_cartesian_mixin [definition, in nom_cartesian_mixin]
nom_ccc [definition, in nom_ccc]
nom_colimit_cocone [definition, in nom_colimit_cocone]
nom_sum_support [definition, in nom_sum_support]
nom_prod_eq_mixin [definition, in nom_prod_eq_mixin]
nom_colimit_commute [lemma, in nom_colimit_commute]
nom_terminus [definition, in nom_terminus]
nom_colimit_eq_mixin [definition, in nom_colimit_eq_mixin]
nom_colimit_equiv [definition, in nom_colimit_equiv]
nom_apply [definition, in nom_apply]
nom_colimit_univ_defn [definition, in nom_colimit_univ_defn]
nom_ident [lemma, in nom_ident]
nom_prod [definition, in nom_prod]
nom_terminate [definition, in nom_terminate]
nom_ccc_mixin [definition, in nom_ccc_mixin]
nom_colimit_spoke [definition, in nom_colimit_spoke]
nom_cartesian [definition, in nom_cartesian]
nom_exp_eq [definition, in nom_exp_eq]
nom_pairing [definition, in nom_pairing]
nom_sum_eq_mixin [definition, in nom_sum_eq_mixin]
nom_colim_elem [projection, in nom_colim_elem]
nom_terminus_mixin [definition, in nom_terminus_mixin]
nom_colimit_uniq [lemma, in nom_colimit_uniq]
nom_colimit_univ [definition, in nom_colimit_univ]
nom_sum_equiv [definition, in nom_sum_equiv]
nom_exp [definition, in nom_exp]
nom_colimit_type [record, in nom_colimit_type]
nom_curry [definition, in nom_curry]
nom_colimit_mixin [definition, in nom_colimit_mixin]
nom_pi1 [definition, in nom_pi1]
nom_pi2 [definition, in nom_pi2]
nom_terminus_eq_mixin [definition, in nom_terminus_eq_mixin]
nom_prod_mixin [definition, in nom_prod_mixin]
nom_exp_type [record, in nom_exp_type]
nom_exp_eq_mixin [definition, in nom_exp_eq_mixin]
nom_colim_idx [projection, in nom_colim_idx]
nom_colimit [definition, in nom_colimit]
nom_exp_mixin [definition, in nom_exp_mixin]
nom_sum_mixin [definition, in nom_sum_mixin]
nonbottom [definition, in nonbottom]
normalizing [lemma, in normalizing]
normalizing [lemma, in normalizing]
normal_sets.A [variable, in A]
normal_sets.normal_mubs.H [variable, in H]
normal_sets.normal_mubs.P [variable, in P]
normal_sets.normal_mubs.Q [variable, in Q]
normal_sets.normal_mubs.X [variable, in X]
normal_sets.normal_mubs.Y [variable, in Y]
normal_mubs' [lemma, in normal_mubs']
normal_has_ubs [lemma, in normal_has_ubs]
normal_set_mub_closed [lemma, in normal_set_mub_closed]
normal_sub_mub_closed_dec [lemma, in normal_sub_mub_closed_dec]
normal_sets.plt_normal.Hplt [variable, in Hplt]
normal_sets.Hnorm [variable, in Hnorm]
normal_sets.normal_mubs.Hinh [variable, in Hinh]
normal_sets.normal_mubs [section, in normal_mubs]
normal_sets.normal_mubs.H0 [variable, in H0]
normal_sets.normal_mubs.H1 [variable, in H1]
normal_sets.normal_mubs.H2 [variable, in H2]
normal_sets.OD [variable, in OD]
normal_set [definition, in normal_set]
normal_sets.hf [variable, in hf]
normal_sets [section, in normal_sets]
normal_set_mub_closed_sets [lemma, in normal_set_mub_closed_sets]
normal_sets.Heff [variable, in Heff]
normal_sub_mub_dec [lemma, in normal_sub_mub_dec]
normal_set_mub_closure [lemma, in normal_set_mub_closure]
normal_has_mubs [lemma, in normal_has_mubs]
normal_sets.plt_normal [section, in plt_normal]
norm_plt [definition, in norm_plt]
norm_closure [definition, in norm_closure]
notations [library]
NT [abbreviation, in NT]
NT [module, in NT]
nt [abbreviation, in nt]
NTCAT [definition, in NTCAT]
NTComp [definition, in NTComp]
NTCompHoriz [definition, in NTCompHoriz]
NTEQ [definition, in NTEQ]
nt_assoc [definition, in nt_assoc]
nt_cat_axioms [lemma, in nt_cat_axioms]
nt_unit1 [definition, in nt_unit1]
nt_unit2 [definition, in nt_unit2]
NT.axiom [projection, in axiom]
NT.compose [definition, in compose]
NT.ident [definition, in ident]
NT.NT [constructor, in NT]
NT.nt [record, in nt]
NT.nt [section, in nt]
NT.NTComp_mixin [definition, in NTComp_mixin]
NT.NTEQ_mixin [definition, in NTEQ_mixin]
NT.NT_mixins.C [variable, in C]
NT.nt_compose.C [variable, in C]
NT.NT_mixins.D [variable, in D]
NT.nt_compose.D [variable, in D]
NT.nt_compose.E [variable, in E]
NT.NT_mixins [section, in NT_mixins]
NT.nt_compose [section, in nt_compose]
NT.nt.C [variable, in C]
NT.nt.D [variable, in D]
NT.nt.F [variable, in F]
NT.nt.G [variable, in G]
NT.pushnt [definition, in pushnt]
NT.stacknt [definition, in stacknt]
NT.transform [projection, in transform]


O

ob [abbreviation, in ob]
ob [abbreviation, in ob]
obeq [projection, in obeq]
obl [abbreviation, in obl]
obmap [projection, in obmap]
obr [abbreviation, in obr]
ONE [definition, in ONE]
OrdDec [constructor, in OrdDec]
orddec [projection, in orddec]
ord_trans [lemma, in ord_trans]
ord_dec [record, in ord_dec]
ord_antisym [lemma, in ord_antisym]
ord_refl [lemma, in ord_refl]


P

pairF [definition, in pairF]
pairF [section, in pairF]
pairF_continuous.C [variable, in C]
pairF_continuous.D [variable, in D]
pairF_continuous.E [variable, in E]
pairF_continuous.F [variable, in F]
pairF_continuous.G [variable, in G]
pairF_continuous.cocones.I [variable, in I]
pairF_continuous.cocones.DS [variable, in DS]
pairF_continuous [lemma, in pairF_continuous]
pairF_continuous [section, in pairF_continuous]
pairF_continuous.cocones [section, in cocones]
pairF_continuous.HcontF [variable, in HcontF]
pairF_continuous.HcontG [variable, in HcontG]
pairF.C [variable, in C]
pairF.D [variable, in D]
pairF.E [variable, in E]
pairF.F [variable, in F]
pairF.G [variable, in G]
pairing [definition, in pairing]
pairing [library]
pairing_unpairing [lemma, in pairing_unpairing]
pairing_univ [lemma, in pairing_univ]
pairing00 [lemma, in pairing00]
pairing01 [lemma, in pairing01]
pairing10 [lemma, in pairing10]
pairing11 [lemma, in pairing11]
pair_rel_eq [lemma, in pair_rel_eq]
pair_rel_elem' [lemma, in pair_rel_elem']
pair_rel_universal_le [lemma, in pair_rel_universal_le]
pair_rel [definition, in pair_rel]
pair_proj_commute1 [lemma, in pair_proj_commute1]
pair_proj_commute2 [lemma, in pair_proj_commute2]
pair_right_continuous [lemma, in pair_right_continuous]
pair_bottom1 [lemma, in pair_bottom1]
pair_bottom2 [lemma, in pair_bottom2]
pair_map [definition, in pair_map]
pair_rel_ordering [lemma, in pair_rel_ordering]
pair_right [definition, in pair_right]
pair_proj_commute1_le [lemma, in pair_proj_commute1_le]
pair_rel_order' [lemma, in pair_rel_order']
pair_left_continuous [lemma, in pair_left_continuous]
pair_rel_dir [lemma, in pair_rel_dir]
pair_proj_commute2_le [lemma, in pair_proj_commute2_le]
pair_rel_universal [lemma, in pair_rel_universal]
pair_left [definition, in pair_left]
pair_rel_elem [lemma, in pair_rel_elem]
pair_rel' [definition, in pair_rel']
papp_inj [lemma, in papp_inj]
pdom_sort [inductive, in pdom_sort]
pdom_fmap [definition, in pdom_fmap]
pdom_map_lower_ord [lemma, in pdom_map_lower_ord]
pdom_map [definition, in pdom_map]
pdom_map_upper_ord [lemma, in pdom_map_upper_ord]
Perm [module, in Perm]
perm [abbreviation, in perm]
PERM [abbreviation, in PERM]
perms [definition, in perms]
perms_neq_nil [lemma, in perms_neq_nil]
perms_len [lemma, in perms_len]
permutations [library]
perm_commute [lemma, in perm_commute]
Perm.assoc [lemma, in assoc]
Perm.category_axioms [lemma, in category_axioms]
Perm.comp [definition, in comp]
Perm.compose [definition, in compose]
Perm.comp_mixin [definition, in comp_mixin]
Perm.eq [definition, in eq]
Perm.eq_mixin [definition, in eq_mixin]
Perm.f [projection, in f]
Perm.fg [projection, in fg]
Perm.f_inj [lemma, in f_inj]
Perm.g [projection, in g]
Perm.gf [projection, in gf]
Perm.groupoid [definition, in groupoid]
Perm.groupoid_mixin [definition, in groupoid_mixin]
Perm.g_inj [lemma, in g_inj]
Perm.ident [definition, in ident]
Perm.inv [definition, in inv]
Perm.inv_id1 [lemma, in inv_id1]
Perm.inv_id2 [lemma, in inv_id2]
Perm.Perm [constructor, in Perm]
Perm.perm [record, in perm]
Perm.PERM [definition, in PERM]
Perm.perm_support [definition, in perm_support]
Perm.support [projection, in support]
Perm.support_perm' [lemma, in support_perm']
Perm.support_axiom [projection, in support_axiom]
Perm.support_perm [lemma, in support_perm]
Perm.swap [definition, in swap]
Perm.swap_swap [lemma, in swap_swap]
Perm.swap_swizzle [lemma, in swap_swizzle]
Perm.swap_same_id [lemma, in swap_same_id]
Perm.swap_self_inv [lemma, in swap_self_inv]
pe_ident [projection, in pe_ident]
pi1 [definition, in pi1]
pi1_rel_ordering [lemma, in pi1_rel_ordering]
pi1_rel [definition, in pi1_rel]
pi1_rel_elem [lemma, in pi1_rel_elem]
pi1_greatest [lemma, in pi1_greatest]
pi1_rel_dir [lemma, in pi1_rel_dir]
pi2 [definition, in pi2]
pi2_rel_ordering [lemma, in pi2_rel_ordering]
pi2_rel_elem [lemma, in pi2_rel_elem]
pi2_rel [definition, in pi2_rel]
pi2_greatest [lemma, in pi2_greatest]
pi2_rel_dir [lemma, in pi2_rel_dir]
plotkin [library]
PlotkinOrder [constructor, in PlotkinOrder]
plotkin_sum [definition, in plotkin_sum]
plotkin_order [record, in plotkin_order]
plotkin_prod [definition, in plotkin_prod]
plotkin_forget [definition, in plotkin_forget]
PLT [abbreviation, in PLT]
PLT [module, in PLT]
PLT [abbreviation, in PLT]
plt_hom_adj [definition, in plt_hom_adj]
plt_const.A [variable, in A]
plt_const.B [variable, in B]
plt_const.b [variable, in b]
plt_const_rel [definition, in plt_const_rel]
plt_hom_adj' [definition, in plt_hom_adj']
plt_hom_adj1 [lemma, in plt_hom_adj1]
plt_hom_adj2 [lemma, in plt_hom_adj2]
plt_const [definition, in plt_const]
plt_const [section, in plt_const]
PLT_adjoint [definition, in PLT_adjoint]
plt_terminate_univ [lemma, in plt_terminate_univ]
plt_strict_compose [lemma, in plt_strict_compose]
plt_bot_None [lemma, in plt_bot_None]
plt_has_normals [lemma, in plt_has_normals]
PLT_EP [definition, in PLT_EP]
plt_bot_chomp [lemma, in plt_bot_chomp]
plt_const.hf [variable, in hf]
plt_semvalue_bot [lemma, in plt_semvalue_bot]
plt_const_rel_elem [lemma, in plt_const_rel_elem]
PLT.app [definition, in app]
PLT.app_hom_rel [lemma, in app_hom_rel]
PLT.carrier [projection, in carrier]
PLT.cartesian [definition, in cartesian]
PLT.cartesian_mixin [definition, in cartesian_mixin]
PLT.cartesian_closed_mixin [definition, in cartesian_closed_mixin]
PLT.cartesian_closed [definition, in cartesian_closed]
PLT.cat_axioms [lemma, in cat_axioms]
PLT.Class [constructor, in Class]
PLT.class [projection, in class]
PLT.class_of [record, in class_of]
PLT.cls_effective [projection, in cls_effective]
PLT.cls_plotkin [projection, in cls_plotkin]
PLT.cls_preord [projection, in cls_preord]
PLT.cocartesian [definition, in cocartesian]
PLT.cocartesian_mixin [definition, in cocartesian_mixin]
PLT.comp [definition, in comp]
PLT.compose [definition, in compose]
PLT.compose_mono [lemma, in compose_mono]
PLT.compose_hom_rel [lemma, in compose_hom_rel]
PLT.comp_mixin [definition, in comp_mixin]
PLT.curry [definition, in curry]
PLT.curry_mono [lemma, in curry_mono]
PLT.curry_apply2 [lemma, in curry_apply2]
PLT.curry_apply3 [lemma, in curry_apply3]
PLT.curry_eq [lemma, in curry_eq]
PLT.curry_compose_commute [lemma, in curry_compose_commute]
PLT.curry_apply [lemma, in curry_apply]
PLT.curry_universal [lemma, in curry_universal]
PLT.curry_hom_rel [lemma, in curry_hom_rel]
PLT.dec [definition, in dec]
PLT.effective [definition, in effective]
PLT.empty [definition, in empty]
PLT.exp [definition, in exp]
PLT.hom [record, in hom]
PLT.Hom [constructor, in Hom]
PLT.homset_cpo_mixin [definition, in homset_cpo_mixin]
PLT.homset_sup [definition, in homset_sup]
PLT.homset_cpo [definition, in homset_cpo]
PLT.hom_eq [definition, in hom_eq]
PLT.hom_ord [definition, in hom_ord]
PLT.hom_ord_mixin [definition, in hom_ord_mixin]
PLT.hom_rel [projection, in hom_rel]
PLT.hom_order [projection, in hom_order]
PLT.hom_eq_mixin [definition, in hom_eq_mixin]
PLT.hom_rel' [definition, in hom_rel']
PLT.hom_directed [projection, in hom_directed]
PLT.ident [definition, in ident]
PLT.initialized_mixin [definition, in initialized_mixin]
PLT.initiate [definition, in initiate]
PLT.initiate_univ [lemma, in initiate_univ]
PLT.iota1 [definition, in iota1]
PLT.iota1_cases_commute [lemma, in iota1_cases_commute]
PLT.iota2 [definition, in iota2]
PLT.iota2_cases_commute [lemma, in iota2_cases_commute]
PLT.Ob [constructor, in Ob]
PLT.ob [record, in ob]
PLT.ord [definition, in ord]
PLT.pair [definition, in pair]
PLT.pair_map_pair [lemma, in pair_map_pair]
PLT.pair_mono [lemma, in pair_mono]
PLT.pair_universal [lemma, in pair_universal]
PLT.pair_le_commute1 [lemma, in pair_le_commute1]
PLT.pair_le_commute2 [lemma, in pair_le_commute2]
PLT.pair_map_eq [lemma, in pair_map_eq]
PLT.pair_hom_rel [lemma, in pair_hom_rel]
PLT.pair_commute1 [lemma, in pair_commute1]
PLT.pair_commute2 [lemma, in pair_commute2]
PLT.pair_map [definition, in pair_map]
PLT.pair_map' [definition, in pair_map']
PLT.pair_eq [lemma, in pair_eq]
PLT.pair_universal_le [lemma, in pair_universal_le]
PLT.pair_compose_commute [lemma, in pair_compose_commute]
PLT.pi1 [definition, in pi1]
PLT.pi2 [definition, in pi2]
PLT.plotkin [definition, in plotkin]
PLT.PLT [definition, in PLT]
PLT.PLT [section, in PLT]
PLT.PLT.hf [variable, in hf]
PLT.PLT.homset_cpo.A [variable, in A]
PLT.PLT.homset_cpo.B [variable, in B]
PLT.PLT.homset_cpo [section, in homset_cpo]
PLT.prod [definition, in prod]
PLT.sum [definition, in sum]
PLT.sum_cases_universal [lemma, in sum_cases_universal]
PLT.sum_cases_hom_rel [lemma, in sum_cases_hom_rel]
PLT.sum_cases_eq [lemma, in sum_cases_eq]
PLT.sum_cases_mono [lemma, in sum_cases_mono]
PLT.sum_cases [definition, in sum_cases]
PLT.terminate [definition, in terminate]
PLT.terminated [definition, in terminated]
PLT.terminated_mixin [definition, in terminated_mixin]
PLT.terminate_le_univ [lemma, in terminate_le_univ]
PLT.unit [definition, in unit]
plug [definition, in plug]
plug [definition, in plug]
plug [definition, in plug]
plug [definition, in plug]
pointed [record, in pointed]
PolynomialCategory [abbreviation, in PolynomialCategory]
PolynomialCategory [module, in PolynomialCategory]
PolynomialCategory.cartesian [definition, in cartesian]
PolynomialCategory.cartesian_mixin [projection, in cartesian_mixin]
PolynomialCategory.cartesian_closed [definition, in cartesian_closed]
PolynomialCategory.category [definition, in category]
PolynomialCategory.cat_axioms [projection, in cat_axioms]
PolynomialCategory.ccc_mixin [projection, in ccc_mixin]
PolynomialCategory.cocartesian [definition, in cocartesian]
PolynomialCategory.cocartesian_mixin [projection, in cocartesian_mixin]
PolynomialCategory.comp [definition, in comp]
PolynomialCategory.comp_mixin [projection, in comp_mixin]
PolynomialCategory.distributive [definition, in distributive]
PolynomialCategory.distributive_mixin [projection, in distributive_mixin]
PolynomialCategory.eq [definition, in eq]
PolynomialCategory.eq_mixin [projection, in eq_mixin]
PolynomialCategory.hom [projection, in hom]
PolynomialCategory.initialized [definition, in initialized]
PolynomialCategory.initialized_mixin [projection, in initialized_mixin]
PolynomialCategory.ob [projection, in ob]
PolynomialCategory.PolynomialCategory [constructor, in PolynomialCategory]
PolynomialCategory.polynomial_category [record, in polynomial_category]
PolynomialCategory.terminated [definition, in terminated]
PolynomialCategory.terminated_mixin [projection, in terminated_mixin]
polynomial_category [abbreviation, in polynomial_category]
postcompose [definition, in postcompose]
postcompose_continuous [lemma, in postcompose_continuous]
powerdom [module, in powerdom]
powerdom [library]
powerdomain [abbreviation, in powerdomain]
powerdomainF [definition, in powerdomainF]
powerdomain_continuous [lemma, in powerdomain_continuous]
powerdom_decompose.I [variable, in I]
powerdom_functor.X [variable, in X]
powerdom_functor.Y [variable, in Y]
powerdom_functor.sort [variable, in sort]
powerdom_decompose [section, in powerdom_decompose]
powerdom_decompose.CC [variable, in CC]
powerdom_decompose.DS [variable, in DS]
powerdom_decompose.hf [variable, in hf]
powerdom_functor.hf [variable, in hf]
powerdom_functor [section, in powerdom_functor]
powerdom_decompose.decompose [variable, in decompose]
powerdom.all_tokens [definition, in all_tokens]
powerdom.concat_elem_mono [lemma, in concat_elem_mono]
powerdom.concat_elem [definition, in concat_elem]
powerdom.concat_in [lemma, in concat_in]
powerdom.convex_union_natural [lemma, in convex_union_natural]
powerdom.convex_ord_trans [lemma, in convex_ord_trans]
powerdom.convex_ord_refl [lemma, in convex_ord_refl]
powerdom.convex_preord_mixin [definition, in convex_preord_mixin]
powerdom.convex_ord [definition, in convex_ord]
powerdom.elem [projection, in elem]
powerdom.elem_inh [projection, in elem_inh]
powerdom.empty [definition, in empty]
powerdom.empty_elem [definition, in empty_elem]
powerdom.empty_join1 [lemma, in empty_join1]
powerdom.empty_join2 [lemma, in empty_join2]
powerdom.empty_rel [definition, in empty_rel]
powerdom.empty_unit2 [lemma, in empty_unit2]
powerdom.empty_unit [lemma, in empty_unit]
powerdom.empty_natural [lemma, in empty_natural]
powerdom.empty_rel_elem [lemma, in empty_rel_elem]
powerdom.enum_elems_complete [lemma, in enum_elems_complete]
powerdom.enum_elems [definition, in enum_elems]
powerdom.fmap [definition, in fmap]
powerdom.fmap_rel_elem [lemma, in fmap_rel_elem]
powerdom.fmap_upper_semidec [lemma, in fmap_upper_semidec]
powerdom.fmap_convex_semidec [lemma, in fmap_convex_semidec]
powerdom.fmap_lower_semidec [lemma, in fmap_lower_semidec]
powerdom.fmap_convex [definition, in fmap_convex]
powerdom.fmap_monotone [lemma, in fmap_monotone]
powerdom.fmap_convex_rel [definition, in fmap_convex_rel]
powerdom.fmap_lower [definition, in fmap_lower]
powerdom.fmap_convex_swell [lemma, in fmap_convex_swell]
powerdom.fmap_respects [lemma, in fmap_respects]
powerdom.fmap_lower_rel [definition, in fmap_lower_rel]
powerdom.fmap_upper_rel [definition, in fmap_upper_rel]
powerdom.fmap_spec [definition, in fmap_spec]
powerdom.fmap_rel [definition, in fmap_rel]
powerdom.fmap_upper [definition, in fmap_upper]
powerdom.join [definition, in join]
powerdom.joinNT [definition, in joinNT]
powerdom.join_rel [definition, in join_rel]
powerdom.join_rel_elem [lemma, in join_rel_elem]
powerdom.join_natural [lemma, in join_natural]
powerdom.lower_ord_refl [lemma, in lower_ord_refl]
powerdom.lower_ord [definition, in lower_ord]
powerdom.lower_ord_trans [lemma, in lower_ord_trans]
powerdom.lower_ord_dec [lemma, in lower_ord_dec]
powerdom.lower_preord_mixin [definition, in lower_preord_mixin]
powerdom.lower_union_natural1 [lemma, in lower_union_natural1]
powerdom.lower_union_natural2 [lemma, in lower_union_natural2]
powerdom.monad_assoc [lemma, in monad_assoc]
powerdom.monad_unit1 [lemma, in monad_unit1]
powerdom.monad_unit2 [lemma, in monad_unit2]
powerdom.normal_pdoms_in [lemma, in normal_pdoms_in]
powerdom.normal_pdoms [definition, in normal_pdoms]
powerdom.normal_pdoms_in' [lemma, in normal_pdoms_in']
powerdom.pdomain [definition, in pdomain]
powerdom.PdomElem [constructor, in PdomElem]
powerdom.pdom_plt [definition, in pdom_plt]
powerdom.pdom_elem [record, in pdom_elem]
powerdom.pdom_effective [definition, in pdom_effective]
powerdom.pdom_elem_eq_upper [lemma, in pdom_elem_eq_upper]
powerdom.pdom_elem_eq_eq [lemma, in pdom_elem_eq_eq]
powerdom.pdom_elem_eq_le [lemma, in pdom_elem_eq_le]
powerdom.pdom_has_normals [lemma, in pdom_has_normals]
powerdom.pdom_elem_eq_lower [lemma, in pdom_elem_eq_lower]
powerdom.pdom_fmap_id [lemma, in pdom_fmap_id]
powerdom.pdom_ord_dec [lemma, in pdom_ord_dec]
powerdom.pdom_ord [definition, in pdom_ord]
powerdom.pdom_fmap_compose [lemma, in pdom_fmap_compose]
powerdom.powerdom [section, in powerdom]
powerdom.powerdomain [definition, in powerdomain]
powerdom.powerdom.hf [variable, in hf]
powerdom.powerdom.orders [section, in orders]
powerdom.powerdom.orders.X [variable, in X]
powerdom.powerdom.orders.Xeff [variable, in Xeff]
powerdom.powerdom.orders.Xplt [variable, in Xplt]
powerdom.powerdom.powerdomain_fmap.X [variable, in X]
powerdom.powerdom.powerdomain_fmap.Y [variable, in Y]
powerdom.powerdom.powerdomain_fmap.f [variable, in f]
powerdom.powerdom.powerdomain_fmap [section, in powerdomain_fmap]
powerdom.select_pdom_elems [definition, in select_pdom_elems]
powerdom.select_pdoms_in [lemma, in select_pdoms_in]
powerdom.select_pdoms_in' [lemma, in select_pdoms_in']
powerdom.single [definition, in single]
powerdom.singleNT [definition, in singleNT]
powerdom.single_elem [definition, in single_elem]
powerdom.single_natural [lemma, in single_natural]
powerdom.single_elem_mono [lemma, in single_elem_mono]
powerdom.single_rel [definition, in single_rel]
powerdom.single_rel_elem [lemma, in single_rel_elem]
powerdom.union [definition, in union]
powerdom.union_rel_elem [lemma, in union_rel_elem]
powerdom.union_assoc_le [lemma, in union_assoc_le]
powerdom.union_idem [lemma, in union_idem]
powerdom.union_elem_convex_ord [lemma, in union_elem_convex_ord]
powerdom.union_elem_lower_ord [lemma, in union_elem_lower_ord]
powerdom.union_elem_upper_ord [lemma, in union_elem_upper_ord]
powerdom.union_rel [definition, in union_rel]
powerdom.union_lower [lemma, in union_lower]
powerdom.union_assoc [lemma, in union_assoc]
powerdom.union_elem [definition, in union_elem]
powerdom.union_join [lemma, in union_join]
powerdom.union_elem_pdom_ord [lemma, in union_elem_pdom_ord]
powerdom.union_commute [lemma, in union_commute]
powerdom.union_upper [lemma, in union_upper]
powerdom.union_commute_le [lemma, in union_commute_le]
powerdom.upper_ord_refl [lemma, in upper_ord_refl]
powerdom.upper_preord_mixin [definition, in upper_preord_mixin]
powerdom.upper_ord [definition, in upper_ord]
powerdom.upper_ord_trans [lemma, in upper_ord_trans]
powerdom.upper_union_natural [lemma, in upper_union_natural]
powerdom.upper_ord_dec [lemma, in upper_ord_dec]
PPLT_EMBED_initialized [definition, in PPLT_EMBED_initialized]
PPLT_EMBED_initialized_mixin [definition, in PPLT_EMBED_initialized_mixin]
precompose [definition, in precompose]
precompose_continuous [lemma, in precompose_continuous]
PREORD [definition, in PREORD]
Preord [module, in Preord]
preord [abbreviation, in preord]
preord [library]
preord_initialized_mixin [definition, in preord_initialized_mixin]
Preord_Eq [definition, in Preord_Eq]
preord_hom_eq [definition, in preord_hom_eq]
preord_eq [lemma, in preord_eq]
preord_terminated [definition, in preord_terminated]
preord_ord [lemma, in preord_ord]
preord_apply [definition, in preord_apply]
preord_cartesian_mixin [definition, in preord_cartesian_mixin]
preord_terminated_mixin [definition, in preord_terminated_mixin]
preord_initiate [definition, in preord_initiate]
preord_initialized [definition, in preord_initialized]
PREORD_concrete [definition, in PREORD_concrete]
preord_curry [definition, in preord_curry]
preord_terminate [definition, in preord_terminate]
preord_ccc_mixin [definition, in preord_ccc_mixin]
preord_cartesian [definition, in preord_cartesian]
PREORD_EQ_DEC [definition, in PREORD_EQ_DEC]
preord_comp [definition, in preord_comp]
preord_ccc [definition, in preord_ccc]
Preord.axiom [projection, in axiom]
Preord.carrier [projection, in carrier]
Preord.cat_axioms [lemma, in cat_axioms]
Preord.compose [definition, in compose]
Preord.comp_mixin [definition, in comp_mixin]
Preord.eq [definition, in eq]
Preord.eq_mixin [definition, in eq_mixin]
Preord.hom [record, in hom]
Preord.Hom [constructor, in Hom]
Preord.hom_eq [definition, in hom_eq]
Preord.hom_ord [definition, in hom_ord]
Preord.ident [definition, in ident]
Preord.map [projection, in map]
Preord.Mixin [constructor, in Mixin]
Preord.mixin [projection, in mixin]
Preord.mixin_of [record, in mixin_of]
Preord.ord [projection, in ord]
Preord.ord_mixin [definition, in ord_mixin]
Preord.ord_eq [definition, in ord_eq]
Preord.ord_op [definition, in ord_op]
Preord.Pack [constructor, in Pack]
Preord.refl [projection, in refl]
Preord.trans [projection, in trans]
Preord.type [record, in type]
PROD [abbreviation, in PROD]
PROD [module, in PROD]
prodF [definition, in prodF]
prodF_continuous [lemma, in prodF_continuous]
prod_functor.A [variable, in A]
prod_functor.B [variable, in B]
prod_functor.C [variable, in C]
prod_functor.D [variable, in D]
prod_functor.f [variable, in f]
prod_functor.g [variable, in g]
prod_fmap [definition, in prod_fmap]
prod_preord [definition, in prod_preord]
prod_functor.hf [variable, in hf]
prod_has_normals [lemma, in prod_has_normals]
prod_ord [definition, in prod_ord]
prod_functor [section, in prod_functor]
PROD.comp_mixin [definition, in comp_mixin]
PROD.Hom [constructor, in Hom]
PROD.homl [projection, in homl]
PROD.homr [projection, in homr]
PROD.hom_eq [definition, in hom_eq]
PROD.hom_comp [definition, in hom_comp]
PROD.hom_eq_mixin [definition, in hom_eq_mixin]
PROD.hom_equiv [definition, in hom_equiv]
PROD.Ob [constructor, in Ob]
PROD.obl [projection, in obl]
PROD.obr [projection, in obr]
PROD.PROD [definition, in PROD]
PROD.product_category.C [variable, in C]
PROD.product_category.D [variable, in D]
PROD.product_category [section, in product_category]
PROD.prod_cat_axioms [lemma, in prod_cat_axioms]
PROD.prod_compose [definition, in prod_compose]
PROD.prod_ident [definition, in prod_ident]
PROD.prod_ob [record, in prod_ob]
PROD.prod_hom [record, in prod_hom]
profinite [library]
profinite_adj [library]
proj [abbreviation, in proj]
proj [abbreviation, in proj]
project [projection, in project]
project_rel [definition, in project_rel]
project_rel_elem [lemma, in project_rel_elem]
project_hom [definition, in project_hom]
projF [section, in projF]
projF.C [variable, in C]
projF.D [variable, in D]
proj1_commute [lemma, in proj1_commute]
proj2_commute [lemma, in proj2_commute]
prove_directed [lemma, in prove_directed]
pseudofunctor [abbreviation, in pseudofunctor]
Pseudofunctor [abbreviation, in Pseudofunctor]
Pseudofunctor [module, in Pseudofunctor]
Pseudofunctor.assoc [projection, in assoc]
Pseudofunctor.compose [projection, in compose]
Pseudofunctor.compose_natural [projection, in compose_natural]
Pseudofunctor.hom_map [projection, in hom_map]
Pseudofunctor.ident [projection, in ident]
Pseudofunctor.ob_map [projection, in ob_map]
Pseudofunctor.pseudofunctor [record, in pseudofunctor]
Pseudofunctor.Pseudofunctor [constructor, in Pseudofunctor]
Pseudofunctor.unit1 [projection, in unit1]
Pseudofunctor.unit2 [projection, in unit2]
Psi_inv_reflects [lemma, in Psi_inv_reflects]
Psi_inv_mono [lemma, in Psi_inv_mono]
Psi_mono [lemma, in Psi_mono]
Psi_reflects [lemma, in Psi_reflects]
Pullback [abbreviation, in Pullback]
Pullback [module, in Pullback]
pullback [abbreviation, in pullback]
Pullback.axiom1 [projection, in axiom1]
Pullback.axiom2 [projection, in axiom2]
Pullback.commute [projection, in commute]
Pullback.commuting_square [definition, in commuting_square]
Pullback.is_pullback [projection, in is_pullback]
Pullback.map [projection, in map]
Pullback.pb_lemma1_comm [lemma, in pb_lemma1_comm]
Pullback.pb_ob [projection, in pb_ob]
Pullback.pb_f [projection, in pb_f]
Pullback.pb_g [projection, in pb_g]
Pullback.Pullback [constructor, in Pullback]
Pullback.pullback [record, in pullback]
Pullback.pullback [section, in pullback]
Pullback.pullback_lemma.C [variable, in C]
Pullback.pullback_lemma.pullback_lemma1.pb_map.H [variable, in H]
Pullback.pullback_lemma.pullback_lemma1.pb_map.Q [variable, in Q]
Pullback.pullback_lemma.R [variable, in R]
Pullback.pullback_lemma.S [variable, in S]
Pullback.pullback_lemma.W [variable, in W]
Pullback.pullback_lemma.X [variable, in X]
Pullback.pullback_lemma.Y [variable, in Y]
Pullback.pullback_lemma.Z [variable, in Z]
Pullback.pullback_lemma.pullback_lemma1.pb_map.p [variable, in p]
Pullback.pullback_lemma.pullback_lemma1.pb_map.q [variable, in q]
Pullback.pullback_lemma.pullback_lemma1.pb_map [section, in pb_map]
Pullback.pullback_lemma1 [definition, in pullback_lemma1]
Pullback.pullback_lemma.pullback_lemma1 [section, in pullback_lemma1]
Pullback.pullback_lemma [section, in pullback_lemma]
Pullback.pullback_lemma.pullback_lemma1.PB1 [variable, in PB1]
Pullback.pullback_lemma.pullback_lemma1.PB2 [variable, in PB2]
Pullback.pullback_lemma.f1 [variable, in f1]
Pullback.pullback_lemma.f2 [variable, in f2]
Pullback.pullback_lemma.f3 [variable, in f3]
Pullback.pullback_lemma.g1 [variable, in g1]
Pullback.pullback_lemma.g2 [variable, in g2]
Pullback.pullback_lemma.h1 [variable, in h1]
Pullback.pullback_lemma.h2 [variable, in h2]
Pullback.pullback_lemma_map2 [definition, in pullback_lemma_map2]
Pullback.pullback_lemma1_map1 [definition, in pullback_lemma1_map1]
Pullback.pullback.C [variable, in C]
Pullback.square [record, in square]
Pullback.Square [constructor, in Square]
Pullback.uniq [projection, in uniq]


R

redex [inductive, in redex]
redex [inductive, in redex]
redex_I [constructor, in redex_I]
redex_I [constructor, in redex_I]
redex_K [constructor, in redex_K]
redex_K [constructor, in redex_K]
redex_S [constructor, in redex_S]
redex_S [constructor, in redex_S]
redex_Y [constructor, in redex_Y]
redex_IFtrue [constructor, in redex_IFtrue]
redex_IFtrue [constructor, in redex_IFtrue]
redex_eq [lemma, in redex_eq]
redex_eq [lemma, in redex_eq]
redex_IFfalse [constructor, in redex_IFfalse]
redex_IFfalse [constructor, in redex_IFfalse]
redex_inert_false [lemma, in redex_inert_false]
redex_soundness [lemma, in redex_soundness]
redex_soundness [lemma, in redex_soundness]
redex_or_inert' [lemma, in redex_or_inert']
redex_or_inert [lemma, in redex_or_inert]
repack [definition, in repack]
repack_equal [lemma, in repack_equal]
right_finset_elem [lemma, in right_finset_elem]
right_finset [definition, in right_finset]
right_whisker [definition, in right_whisker]
RS_elem' [lemma, in RS_elem']
RS_elem [lemma, in RS_elem]
R'_R [lemma, in R'_R]


S

scott_induction [lemma, in scott_induction]
select_jrels_elem1 [lemma, in select_jrels_elem1]
select_jrels_elem2 [lemma, in select_jrels_elem2]
select_jrels [definition, in select_jrels]
semidec [record, in semidec]
Semidec [constructor, in Semidec]
semidec_disj [definition, in semidec_disj]
semidec_true [definition, in semidec_true]
semidec_iff [lemma, in semidec_iff]
semidec_conj [definition, in semidec_conj]
semidec_ex [lemma, in semidec_ex]
semidec_in [lemma, in semidec_in]
semidec_false [definition, in semidec_false]
semidirected_cl [definition, in semidirected_cl]
semvalue [definition, in semvalue]
semvalue_le [lemma, in semvalue_le]
semvalue_equiv [lemma, in semvalue_equiv]
semvalue_app_out1' [lemma, in semvalue_app_out1']
semvalue_app_out2' [lemma, in semvalue_app_out2']
semvalue_sup [lemma, in semvalue_sup]
semvalue_sup [lemma, in semvalue_sup]
semvalue_lrsemapp_out [lemma, in semvalue_lrsemapp_out]
semvalue_strict_app_out1 [lemma, in semvalue_strict_app_out1]
semvalue_strict_app_out2 [lemma, in semvalue_strict_app_out2]
SET [definition, in SET]
SET [module, in SET]
set [abbreviation, in set]
set [module, in set]
setdec [projection, in setdec]
Setdec [constructor, in Setdec]
sets [library]
SET_terminate [definition, in SET_terminate]
SET_terminus [definition, in SET_terminus]
set_preord [definition, in set_preord]
set_dec [record, in set_dec]
SET_COMP [definition, in SET_COMP]
SET_terminated [definition, in SET_terminated]
SET_EQ [definition, in SET_EQ]
SET_concrete [definition, in SET_concrete]
SET.carrier [projection, in carrier]
SET.compose [definition, in compose]
SET.hom [record, in hom]
SET.Hom [constructor, in Hom]
SET.hom_axiom [projection, in hom_axiom]
SET.hom_map [projection, in hom_map]
SET.ident [definition, in ident]
set.image [projection, in image]
set.image_axiom0 [projection, in image_axiom0]
set.image_axiom1 [projection, in image_axiom1]
set.image_axiom2 [projection, in image_axiom2]
set.member [projection, in member]
set.member_eq [projection, in member_eq]
set.Mixin [constructor, in Mixin]
SET.mixin [projection, in mixin]
set.mixin [projection, in mixin]
set.mixin_def.incl [variable, in incl]
set.mixin_def.union [variable, in union]
set.mixin_def.image [variable, in image]
set.mixin_of [record, in mixin_of]
set.mixin_def.member [variable, in member]
set.mixin_def.single [variable, in single]
set.mixin_def [section, in mixin_def]
set.mixin_def.set [variable, in set]
SET.Ob [constructor, in Ob]
SET.ob [record, in ob]
set.set [projection, in set]
SET.set_ob_Eq [definition, in set_ob_Eq]
set.set_preord [definition, in set_preord]
SET.set_hom_comp [definition, in set_hom_comp]
SET.set_hom_eq [definition, in set_hom_eq]
set.single [projection, in single]
set.single_axiom [projection, in single_axiom]
set.theory [record, in theory]
set.Theory [constructor, in Theory]
set.union [projection, in union]
set.union_axiom [projection, in union_axiom]
single [definition, in single]
single_axiom [lemma, in single_axiom]
ski [library]
skiy [library]
smash_prod_spec [inductive, in smash_prod_spec]
smash_prod [definition, in smash_prod]
smash_prod_iff [lemma, in smash_prod_iff]
smash_some [constructor, in smash_some]
smash_unsmash [lemma, in smash_unsmash]
smash_none [constructor, in smash_none]
sndF [definition, in sndF]
sndF_continuous.C [variable, in C]
sndF_continuous.D [variable, in D]
sndF_continuous.I [variable, in I]
sndF_cocone [definition, in sndF_cocone]
sndF_continuous.CC [variable, in CC]
sndF_continuous.DS [variable, in DS]
sndF_continuous [lemma, in sndF_continuous]
sndF_continuous [section, in sndF_continuous]
sndF_univ [definition, in sndF_univ]
sndF_continuous.Hcolim [variable, in Hcolim]
sndF_continuous' [lemma, in sndF_continuous']
soundness [lemma, in soundness]
soundness [lemma, in soundness]
soundness [lemma, in soundness]
soundness [lemma, in soundness]
strictify [section, in strictify]
strictify_le [lemma, in strictify_le]
strictify_largest [lemma, in strictify_largest]
strictify.f [variable, in f]
strictify.strictify [variable, in strictify]
strictify.X [variable, in X]
strictify.Y [variable, in Y]
strict_app' [definition, in strict_app']
strict_app [definition, in strict_app]
strict_curry_compose_commute' [lemma, in strict_curry_compose_commute']
strict_map [lemma, in strict_map]
strict_app_bot' [lemma, in strict_app_bot']
strict_curry'_semvalue2 [lemma, in strict_curry'_semvalue2]
strict_curry_app2' [lemma, in strict_curry_app2']
strict_curry_app [lemma, in strict_curry_app]
strict_curry_monotone [lemma, in strict_curry_monotone]
strict_app_bot [lemma, in strict_app_bot]
strict_curry'_eq [lemma, in strict_curry'_eq]
strict_curry'_monotone [lemma, in strict_curry'_monotone]
strict_curry_app_converse [lemma, in strict_curry_app_converse]
strict_curry'_semvalue [lemma, in strict_curry'_semvalue]
strict_curry_app' [lemma, in strict_curry_app']
strict_curry_app2 [lemma, in strict_curry_app2]
strict_curry' [definition, in strict_curry']
strict_curry_eq [lemma, in strict_curry_eq]
strict_curry_compose_commute [lemma, in strict_curry_compose_commute]
strict_curry [definition, in strict_curry]
strict_utils [library]
string_ord [definition, in string_ord]
string_ord_mixin [definition, in string_ord_mixin]
st_lam_fix [library]
st_lam [library]
subst [abbreviation, in subst]
subst [abbreviation, in subst]
subst_alpha_ident [lemma, in subst_alpha_ident]
subst_alpha_ident [lemma, in subst_alpha_ident]
subst_soundness [lemma, in subst_soundness]
subst_soundness [lemma, in subst_soundness]
subst_weaken_alpha [lemma, in subst_weaken_alpha]
subst_weaken_alpha [lemma, in subst_weaken_alpha]
sumF [definition, in sumF]
sumF_continuous [lemma, in sumF_continuous]
sumprod_functor [library]
sum_functor.A [variable, in A]
sum_functor.B [variable, in B]
sum_functor.C [variable, in C]
sum_functor.D [variable, in D]
sum_functor.f [variable, in f]
sum_functor.g [variable, in g]
sum_cases_univ [lemma, in sum_cases_univ]
sum_cases_ordering [lemma, in sum_cases_ordering]
sum_preord [definition, in sum_preord]
sum_fmap_func [definition, in sum_fmap_func]
sum_cases_dir [lemma, in sum_cases_dir]
sum_functor [section, in sum_functor]
sum_map [definition, in sum_map]
sum_functor.hf [variable, in hf]
sum_fmap [definition, in sum_fmap]
sum_cases_elem [lemma, in sum_cases_elem]
sum_cases [definition, in sum_cases]
sum_ord [definition, in sum_ord]
sum_has_normals [lemma, in sum_has_normals]
Support [module, in Support]
Supported [abbreviation, in Supported]
supported [abbreviation, in supported]
support_axiom [lemma, in support_axiom]
support_axiom' [lemma, in support_axiom']
support_papp [lemma, in support_papp]
Support.carrier [projection, in carrier]
Support.disjoint [definition, in disjoint]
Support.support [projection, in support]
Support.Supported [constructor, in Supported]
Support.supported [record, in supported]
sup_equiv [lemma, in sup_equiv]
sup_monotone [lemma, in sup_monotone]
swap_induction [lemma, in swap_induction]
swap_induction' [lemma, in swap_induction']
swap_commute' [lemma, in swap_commute']
swap_commute [lemma, in swap_commute]
swell [lemma, in swell]
swelling_lemma [lemma, in swelling_lemma]
swell_inductive_step [lemma, in swell_inductive_step]
swell_row [lemma, in swell_row]
swell_relation [lemma, in swell_relation]
swell_aux [lemma, in swell_aux]


T

tapp [constructor, in tapp]
tapp [constructor, in tapp]
tapp [constructor, in tapp]
tapp [constructor, in tapp]
tbool [constructor, in tbool]
tbool [constructor, in tbool]
tbool [constructor, in tbool]
tbool [constructor, in tbool]
term [inductive, in term]
term [inductive, in term]
term [inductive, in term]
term [inductive, in term]
Terminated [abbreviation, in Terminated]
Terminated [module, in Terminated]
terminated [abbreviation, in terminated]
Terminated.axiom [projection, in axiom]
Terminated.category [definition, in category]
Terminated.cat_axioms [projection, in cat_axioms]
Terminated.comp [definition, in comp]
Terminated.comp_mixin [projection, in comp_mixin]
Terminated.eq [definition, in eq]
Terminated.eq_mixin [projection, in eq_mixin]
Terminated.eq' [definition, in eq']
Terminated.hom [projection, in hom]
Terminated.Mixin [constructor, in Mixin]
Terminated.mixin [projection, in mixin]
Terminated.mixin_of [record, in mixin_of]
Terminated.ob [projection, in ob]
Terminated.terminate [projection, in terminate]
Terminated.Terminated [constructor, in Terminated]
Terminated.terminated [record, in terminated]
Terminated.terminated [section, in terminated]
Terminated.terminated.eq [variable, in eq]
Terminated.terminated.hom [variable, in hom]
Terminated.terminated.ob [variable, in ob]
Terminated.terminate_op [definition, in terminate_op]
Terminated.terminus [projection, in terminus]
Terminated.terminus_op [definition, in terminus_op]
terminate_le_cancel [lemma, in terminate_le_cancel]
terminate_univ [lemma, in terminate_univ]
terminate_cancel [lemma, in terminate_cancel]
term_wk_ident [lemma, in term_wk_ident]
term_wk_ident [lemma, in term_wk_ident]
term_subst [abbreviation, in term_subst]
term_subst [abbreviation, in term_subst]
term_wk [abbreviation, in term_wk]
term_wk [abbreviation, in term_wk]
term_subst_cong [lemma, in term_subst_cong]
term_subst_cong [lemma, in term_subst_cong]
term_subst_wk_cong [lemma, in term_subst_wk_cong]
term_subst_wk_cong [lemma, in term_subst_wk_cong]
term_wk_compose [lemma, in term_wk_compose]
term_wk_compose [lemma, in term_wk_compose]
term_wk_compose' [lemma, in term_wk_compose']
term_wk_compose' [lemma, in term_wk_compose']
test_functor_assocative_convertability.C [variable, in C]
test_functor_assocative_convertability.D [variable, in D]
test_functor_assocative_convertability.E [variable, in E]
test_functor_assocative_convertability.F [variable, in F]
test_functor_assocative_convertability.G [variable, in G]
test_functor_assocative_convertability.H [variable, in H]
test_functor_assocative_convertability [section, in test_functor_assocative_convertability]
test_functor_assocative_convertability.I [variable, in I]
tfix [constructor, in tfix]
tI [constructor, in tI]
tI [constructor, in tI]
tif [constructor, in tif]
tif [constructor, in tif]
tIF [constructor, in tIF]
tIF [constructor, in tIF]
tK [constructor, in tK]
tK [constructor, in tK]
tlam [constructor, in tlam]
tlam [constructor, in tlam]
tmsize [definition, in tmsize]
total_fixpoint.A [variable, in A]
total_fixpoint.F [variable, in F]
total_fixpoint.h [variable, in h]
total_fixpoint [section, in total_fixpoint]
total_fixpoint.BL [variable, in BL]
total_fixpoint.Fcontinuous [variable, in Fcontinuous]
traverse [definition, in traverse]
traverse [section, in traverse]
traverse [definition, in traverse]
traverse [section, in traverse]
traverse_correct [lemma, in traverse_correct]
traverse_correct [lemma, in traverse_correct]
traverse.rename_var [variable, in rename_var]
traverse.rename_var [variable, in rename_var]
traverse.thingy [variable, in thingy]
traverse.thingy [variable, in thingy]
traverse.thingy_term [variable, in thingy_term]
traverse.thingy_term [variable, in thingy_term]
traverse.varmap_denote_proj [variable, in varmap_denote_proj]
traverse.varmap_denote_proj [variable, in varmap_denote_proj]
traverse.weaken_vars [variable, in weaken_vars]
traverse.weaken_vars [variable, in weaken_vars]
traverse.weaken_sem_bind [variable, in weaken_sem_bind]
traverse.weaken_sem_bind [variable, in weaken_sem_bind]
tS [constructor, in tS]
tS [constructor, in tS]
tvar [constructor, in tvar]
tvar [constructor, in tvar]
tY [constructor, in tY]
ty [inductive, in ty]
ty [inductive, in ty]
ty [inductive, in ty]
ty [inductive, in ty]
tydom [definition, in tydom]
tydom [definition, in tydom]
tydom [definition, in tydom]
tydom [definition, in tydom]
TYPE [abbreviation, in TYPE]
TYPE [module, in TYPE]
TYPE.compose [definition, in compose]
TYPE.ident [definition, in ident]
TYPE.thom [definition, in thom]
TYPE.tob [definition, in tob]
TYPE.TYPE [definition, in TYPE]
ty_arrow [constructor, in ty_arrow]
ty_arrow [constructor, in ty_arrow]
ty_arrow [constructor, in ty_arrow]
ty_arrow [constructor, in ty_arrow]
ty_bool [constructor, in ty_bool]
ty_bool [constructor, in ty_bool]
ty_bool [constructor, in ty_bool]
ty_bool [constructor, in ty_bool]
ty_dec [lemma, in ty_dec]
ty_dec [lemma, in ty_dec]


U

U [abbreviation, in U]
ub_cons [lemma, in ub_cons]
ub_nil [lemma, in ub_nil]
Ue [abbreviation, in Ue]
unenumerate [definition, in unenumerate]
unenumerate_uniq [lemma, in unenumerate_uniq]
unenumerate_set_inhabited [lemma, in unenumerate_set_inhabited]
unenumerate_correct [lemma, in unenumerate_correct]
unenumerate_reflects [lemma, in unenumerate_reflects]
unenumerate_set [definition, in unenumerate_set]
unfold [section, in unfold]
unfold_stream [definition, in unfold_stream]
unfold_find [lemma, in unfold_find]
unfold.A [variable, in A]
unfold.ind_step [variable, in ind_step]
unfold.invariant [variable, in invariant]
unfold.out_prop [variable, in out_prop]
unfold.step [variable, in step]
unfold.wf [variable, in wf]
unfold.wf_rel [variable, in wf_rel]
unfold.X [variable, in X]
unimage_jrel [definition, in unimage_jrel]
unimage_jrel_order [lemma, in unimage_jrel_order]
unimage_jrel_directed [lemma, in unimage_jrel_directed]
union [definition, in union]
union_axiom [lemma, in union_axiom]
union2 [definition, in union2]
union2_elem [lemma, in union2_elem]
unitpo [definition, in unitpo]
unitpo_dec [lemma, in unitpo_dec]
unit_plotkin [definition, in unit_plotkin]
unlift_list [definition, in unlift_list]
unlift_app [lemma, in unlift_app]
unmap_rel_sub [lemma, in unmap_rel_sub]
unmap_rel [lemma, in unmap_rel]
unpairing [definition, in unpairing]
unpairing_pairing [lemma, in unpairing_pairing]
unsmash_prod [definition, in unsmash_prod]
unsmash_smash [lemma, in unsmash_smash]
Upper [constructor, in Upper]
upper_bound_dec [lemma, in upper_bound_dec]
upper_bound_ok [lemma, in upper_bound_ok]
upper_set [definition, in upper_set]
upper_bound [definition, in upper_bound]
use_ord [lemma, in use_ord]
U_mono [lemma, in U_mono]
U_hom_rel [lemma, in U_hom_rel]
U_reflects [lemma, in U_reflects]
U_bottom_least [lemma, in U_bottom_least]


V

value [definition, in value]
value [definition, in value]
value_inert_semvalue [lemma, in value_inert_semvalue]
value_semvalue [lemma, in value_semvalue]
value_semvalue [lemma, in value_semvalue]
value_app_inv [lemma, in value_app_inv]
varcong_eq [lemma, in varcong_eq]
varcong_eq [lemma, in varcong_eq]
varcong_inenv1 [lemma, in varcong_inenv1]
varcong_inenv1 [lemma, in varcong_inenv1]
varcong_inenv2 [lemma, in varcong_inenv2]
varcong_inenv2 [lemma, in varcong_inenv2]
var_cong_sym [lemma, in var_cong_sym]
var_cong_sym [lemma, in var_cong_sym]
var_cong_trans [lemma, in var_cong_trans]
var_cong_trans [lemma, in var_cong_trans]
var_cong_refl [lemma, in var_cong_refl]
var_cong_refl [lemma, in var_cong_refl]
var_cong [inductive, in var_cong]
var_cong [inductive, in var_cong]
vcong_here [constructor, in vcong_here]
vcong_here [constructor, in vcong_here]
vcong_there [constructor, in vcong_there]
vcong_there [constructor, in vcong_there]


W

weak_countable_choice [lemma, in weak_countable_choice]
wf_idents_wf [lemma, in wf_idents_wf]


Y

Ybody [definition, in Ybody]
Ybody_unroll [lemma, in Ybody_unroll]
Ydefn [section, in Ydefn]
Ydefn.σ₁ [variable, in σ₁]
Ydefn.σ₂ [variable, in σ₂]
Ysem [definition, in Ysem]


other

_ ⇒ _ (bicategory_scope) [notation, in :bicategory_scope:x_'⇒'_x]
_ ◃ _ (bicategory_scope) [notation, in :bicategory_scope:x_'◃'_x]
_ → _ (bicategory_scope) [notation, in :bicategory_scope:x_'→'_x]
_ ▹ _ (bicategory_scope) [notation, in :bicategory_scope:x_'▹'_x]
_ · _ (category_hom_scope) [notation, in :category_hom_scope:x_'·'_x]
id ( _ ) (category_hom_scope) [notation, in :category_hom_scope:'id'_'('_x_')']
_ ↔ _ (category_hom_scope) [notation, in :category_hom_scope:x_'↔'_x]
_ ⇒ _ (category_ob_scope) [notation, in :category_ob_scope:x_'⇒'_x]
∗ (category_ops_scope) [notation, in :category_ops_scope:'∗']
_ ▹ _ (category_hom_scope) [notation, in :category_hom_scope:x_'▹'_x]
π₁ (category_ops_scope) [notation, in :category_ops_scope:'π₁']
π₂ (category_ops_scope) [notation, in :category_ops_scope:'π₂']
! (category_ob_scope) [notation, in :category_ob_scope:'!']
¡ (category_ob_scope) [notation, in :category_ob_scope:'¡']
_ ↠ _ (category_hom_scope) [notation, in :category_hom_scope:x_'↠'_x]
_ × _ (category_ob_scope) [notation, in :category_ob_scope:x_'×'_x]
_ # _ (category_hom_scope) [notation, in :category_hom_scope:x_'#'_x]
_ ◃ _ (category_hom_scope) [notation, in :category_hom_scope:x_'◃'_x]
Λ _ (category_ops_scope) [notation, in :category_ops_scope:'Λ'_x]
〈 _ , _ 〉 (category_ops_scope) [notation, in :category_ops_scope:'〈'_x_','_x_'〉']
_ + _ (category_ob_scope) [notation, in :category_ob_scope:x_'+'_x]
id (category_hom_scope) [notation, in :category_hom_scope:'id']
_ → _ (category_hom_scope) [notation, in :category_hom_scope:x_'→'_x]
_ ↣ _ (category_hom_scope) [notation, in :category_hom_scope:x_'↣'_x]
_ ⁻¹ (category_hom_scope) [notation, in :category_hom_scope:x_'⁻¹']
ι₁ (category_ops_scope) [notation, in :category_ops_scope:'ι₁']
ι₂ (category_ops_scope) [notation, in :category_ops_scope:'ι₂']
_ ∘ _ (category_hom_scope) [notation, in :category_hom_scope:x_'∘'_x]
⊥ (cpo_scope) [notation, in :cpo_scope:'⊥']
∐ _ (cpo_scope) [notation, in :cpo_scope:'∐'_x]
_ ≈ _ (equiv_scope) [notation, in :equiv_scope:x_'≈'_x]
_ ≉ _ (equiv_scope) [notation, in :equiv_scope:x_'≉'_x]
〚 _ 〛 (lam_scope) [notation, in :lam_scope:'〚'_x_'〛']
〚 _ 〛 (lam_scope) [notation, in :lam_scope:'〚'_x_'〛']
_ • _ (lam_scope) [notation, in :lam_scope:x_'•'_x]
_ • _ (lam_scope) [notation, in :lam_scope:x_'•'_x]
_ ⊸ _ (plt_scope) [notation, in :plt_scope:x_'⊸'_x]
Λ _ (plt_scope) [notation, in :plt_scope:'Λ'_x]
π₁ (plt_scope) [notation, in :plt_scope:'π₁']
π₂ (plt_scope) [notation, in :plt_scope:'π₂']
_ ⇒ _ (plt_scope) [notation, in :plt_scope:x_'⇒'_x]
0 (plt_scope) [notation, in :plt_scope:'0']
1 (plt_scope) [notation, in :plt_scope:'1']
_ × _ (plt_scope) [notation, in :plt_scope:x_'×'_x]
_ + _ (plt_scope) [notation, in :plt_scope:x_'+'_x]
_ ⊕ _ (plt_scope) [notation, in :plt_scope:x_'⊕'_x]
《 _ , _ 》 (plt_scope) [notation, in :plt_scope:'《'_x_','_x_'》']
ι₁ (plt_scope) [notation, in :plt_scope:'ι₁']
ι₂ (plt_scope) [notation, in :plt_scope:'ι₂']
_ ⊗ _ (plt_scope) [notation, in :plt_scope:x_'⊗'_x]
〈 _ , _ 〉 (plt_scope) [notation, in :plt_scope:'〈'_x_','_x_'〉']
_ ≥ _ (preord_scope) [notation, in :preord_scope:x_'≥'_x]
_ ≰ _ (preord_scope) [notation, in :preord_scope:x_'≰'_x]
_ ≱ _ (preord_scope) [notation, in :preord_scope:x_'≱'_x]
_ ≤ _ (preord_scope) [notation, in :preord_scope:x_'≤'_x]
_ ∈ _ (set_scope) [notation, in :set_scope:x_'∈'_x]
∪ _ (set_scope) [notation, in :set_scope:'∪'_x]
_ ∉ _ (set_scope) [notation, in :set_scope:x_'∉'_x]
_ ⊆ _ (set_scope) [notation, in :set_scope:x_'⊆'_x]
〚 _ 〛 (ski_scope) [notation, in :ski_scope:'〚'_x_'〛']
〚 _ 〛 (ski_scope) [notation, in :ski_scope:'〚'_x_'〛']
Λ _ (ski_scope) [notation, in :ski_scope:'Λ'_x]
_ • _ (ski_scope) [notation, in :ski_scope:x_'•'_x]
_ • _ (ski_scope) [notation, in :ski_scope:x_'•'_x]
_ ⇒ _ (ty_scope) [notation, in :ty_scope:x_'⇒'_x]
_ ⇒ _ (ty_scope) [notation, in :ty_scope:x_'⇒'_x]
_ ⇒ _ (ty_scope) [notation, in :ty_scope:x_'⇒'_x]
_ ⇒ _ (ty_scope) [notation, in :ty_scope:x_'⇒'_x]
2 (ty_scope) [notation, in :ty_scope:'2']
2 (ty_scope) [notation, in :ty_scope:'2']
2 (ty_scope) [notation, in :ty_scope:'2']
2 (ty_scope) [notation, in :ty_scope:'2']
_ ↓ [notation, in ::x_'↓']
_ ↓ [notation, in ::x_'↓']
_ ✧ _ [notation, in ::x_'✧'_x]
_ • _ [notation, in ::x_'•'_x]
_ ⋆ _ [notation, in ::x_'⋆'_x]
_ · _ [notation, in ::x_'·'_x]
_ ⇓ _ [notation, in ::x_'⇓'_x]
_ ⇓ _ [notation, in ::x_'⇓'_x]
_ ⇀ _ [notation, in ::x_'⇀'_x]
_ ⇋ _ [notation, in ::x_'⇋'_x]
_ ♯ _ [notation, in ::x_'♯'_x]
_ ✦ _ [notation, in ::x_'✦'_x]
fresh [ _ , .. , _ ] [notation, in ::'fresh'_'['_x_','_'..'_','_x_']']
Id [notation, in ::'Id']
Id ( _ ) [notation, in ::'Id'_'('_x_')']
‖ _ ‖ [notation, in ::'‖'_x_'‖']
∂PLT [notation, in ::'∂PLT']
[notation, in ::'∅']
Ψ⁻¹ [notation, in ::'Ψ⁻¹']
ν _ , _ [notation, in ::'ν'_x_','_x]
Ψ [abbreviation, in Ψ]
γ [abbreviation, in γ]
ε [abbreviation, in ε]
η [abbreviation, in η]



Instance Index

C

cppo_pointed [in cppo_pointed]


L

lift_plt_pointed [in lift_plt_pointed]



Projection Index

A

Adjunction.adjoint_axiom1 [in adjoint_axiom1]
Adjunction.adjoint_axiom2 [in adjoint_axiom2]
Adjunction.counit [in counit]
Adjunction.unit [in unit]
Alg.carrier [in carrier]
Alg.cata [in cata]
Alg.cata_axiom [in cata_axiom]
Alg.hom_axiom [in hom_axiom]
Alg.hom_map [in hom_map]
Alg.init [in init]
Alg.iota [in iota]


B

Bicategory.assoc [in assoc]
Bicategory.associator_pentagon [in associator_pentagon]
Bicategory.assoc_natural [in assoc_natural]
Bicategory.cat_axioms [in cat_axioms]
Bicategory.comp [in comp]
Bicategory.CompHom [in CompHom]
Bicategory.CompHoriz [in CompHoriz]
Bicategory.eq [in eq]
Bicategory.hom [in hom]
Bicategory.hom2 [in hom2]
Bicategory.Ident [in Ident]
Bicategory.mixin [in mixin]
Bicategory.ob [in ob]
Bicategory.unitor_triangle [in unitor_triangle]
Bicategory.unit1 [in unit1]
Bicategory.unit1_natural [in unit1_natural]
Bicategory.unit2 [in unit2]
Bicategory.unit2_natural [in unit2_natural]
bottom [in bottom]
bottom_least [in bottom_least]


C

CartesianClosed.apply [in apply]
CartesianClosed.cartesian_mixin [in cartesian_mixin]
CartesianClosed.cat_axioms [in cat_axioms]
CartesianClosed.ccc_axioms [in ccc_axioms]
CartesianClosed.comp_mixin [in comp_mixin]
CartesianClosed.curry [in curry]
CartesianClosed.curry_univ [in curry_univ]
CartesianClosed.curry_commute [in curry_commute]
CartesianClosed.eq_mixin [in eq_mixin]
CartesianClosed.exp [in exp]
CartesianClosed.hom [in hom]
CartesianClosed.mixin [in mixin]
CartesianClosed.ob [in ob]
CartesianClosed.terminated_mixin [in terminated_mixin]
Cartesian.cartesian_axioms [in cartesian_axioms]
Cartesian.cat_axioms [in cat_axioms]
Cartesian.comp_mixin [in comp_mixin]
Cartesian.eq_mixin [in eq_mixin]
Cartesian.hom [in hom]
Cartesian.mixin [in mixin]
Cartesian.ob [in ob]
Cartesian.pairing [in pairing]
Cartesian.pairing_univ [in pairing_univ]
Cartesian.product [in product]
Cartesian.proj1 [in proj1]
Cartesian.proj1_commute [in proj1_commute]
Cartesian.proj2 [in proj2]
Cartesian.proj2_commute [in proj2_commute]
Cartesian.term_mixin [in term_mixin]
Category.assoc [in assoc]
Category.cat_axioms [in cat_axioms]
Category.comp [in comp]
Category.eq [in eq]
Category.hom [in hom]
Category.ident1 [in ident1]
Category.ident2 [in ident2]
Category.ob [in ob]
Category.respects [in respects]
choose_ub_set [in choose_ub_set]
Cocartesian.cat_axioms [in cat_axioms]
Cocartesian.cocartesian_axioms [in cocartesian_axioms]
Cocartesian.comp_mixin [in comp_mixin]
Cocartesian.either [in either]
Cocartesian.either_univ [in either_univ]
Cocartesian.eq_mixin [in eq_mixin]
Cocartesian.hom [in hom]
Cocartesian.init_mixin [in init_mixin]
Cocartesian.inl [in inl]
Cocartesian.inl_commute [in inl_commute]
Cocartesian.inr [in inr]
Cocartesian.inr_commute [in inr_commute]
Cocartesian.mixin [in mixin]
Cocartesian.ob [in ob]
Cocartesian.sum [in sum]
cocone_spoke [in cocone_spoke]
cocone_commute [in cocone_commute]
cocone_point [in cocone_point]
colim_commute [in colim_commute]
colim_uniq [in colim_uniq]
colim_univ [in colim_univ]
color_prop [in color_prop]
color_eq [in color_eq]
color_union [in color_union]
color_image [in color_image]
color_single [in color_single]
Comp.comp [in comp]
Comp.hom [in hom]
Comp.identity [in identity]
Comp.mixin [in mixin]
Comp.ob [in ob]
Cone.axiom [in axiom]
Cone.hom_axiom [in hom_axiom]
Cone.hom_map [in hom_map]
Cone.point [in point]
Cone.spoke [in spoke]
CPO.carrier [in carrier]
CPO.cont [in cont]
CPO.cpo_mixin [in cpo_mixin]
CPO.map [in map]
CPO.mono [in mono]
CPO.ord_mixin [in ord_mixin]
CPO.sup [in sup]
CPO.sup_is_ub [in sup_is_ub]
CPO.sup_is_least [in sup_is_least]


D

decset [in decset]
decset_correct [in decset_correct]
dir_preord [in dir_preord]
dir_effective [in dir_effective]
Distributive.cartesian_mixin [in cartesian_mixin]
Distributive.cat_axioms [in cat_axioms]
Distributive.cocartesian_mixin [in cocartesian_mixin]
Distributive.comp_mixin [in comp_mixin]
Distributive.distrib_law [in distrib_law]
Distributive.eq_mixin [in eq_mixin]
Distributive.hom [in hom]
Distributive.initialized_mixin [in initialized_mixin]
Distributive.mixin [in mixin]
Distributive.ob [in ob]
Distributive.terminated_mixin [in terminated_mixin]
ds_compose [in ds_compose]
ds_hom [in ds_hom]
ds_F [in ds_F]
ds_ident [in ds_ident]


E

eff_ord_dec [in eff_ord_dec]
eff_enum [in eff_enum]
eff_complete [in eff_complete]
elem [in elem]
embed [in embed]
embed_directed0 [in embed_directed0]
embed_directed2 [in embed_directed2]
embed_reflects [in embed_reflects]
embed_map [in embed_map]
embed_mono [in embed_mono]
enumtype.carrier [in carrier]
enumtype.enumtype_set [in enumtype_set]
enumtype.enumtype_complete [in enumtype_complete]
enumtype.enumtype_dec [in enumtype_dec]
epi_axiom [in epi_axiom]
epi_hom [in epi_hom]
ep_ident [in ep_ident]
ep_correct [in ep_correct]
eqdec [in eqdec]
Eq.carrier [in carrier]
Eq.eq [in eq]
Eq.mixin [in mixin]
Eq.refl [in refl]
Eq.symm [in symm]
Eq.trans [in trans]
exp_eq_axiom [in exp_eq_axiom]
exp_support [in exp_support]
exp_support_axiom [in exp_support_axiom]
exp_map [in exp_map]


F

finprod.tm_denote_var [in tm_denote_var]
finprod.tm_traverse [in tm_traverse]
finprod.tm_traverse_correct [in tm_traverse_correct]
finprod.tm_var [in tm_var]
finprod.tm_denote [in tm_denote]
fintype.carrier [in carrier]
fintype.fintype_list [in fintype_list]
fintype.fintype_complete [in fintype_complete]
fintype.fintype_dec [in fintype_dec]
Functor.compose [in compose]
Functor.hom_map [in hom_map]
Functor.ident [in ident]
Functor.ob_map [in ob_map]
Functor.respects [in respects]


G

Groupoid.cat_axioms [in cat_axioms]
Groupoid.comp_mixin [in comp_mixin]
Groupoid.eq_mixin [in eq_mixin]
Groupoid.groupoid_axioms [in groupoid_axioms]
Groupoid.hom [in hom]
Groupoid.inv [in inv]
Groupoid.inv_id1 [in inv_id1]
Groupoid.inv_id2 [in inv_id2]
Groupoid.mixin [in mixin]
Groupoid.ob [in ob]


H

hommap [in hommap]
hommap_eq [in hommap_eq]
hommap_axiom [in hommap_axiom]


I

idx [in idx]
Initialized.axiom [in axiom]
Initialized.cat_axioms [in cat_axioms]
Initialized.comp_mixin [in comp_mixin]
Initialized.eq_mixin [in eq_mixin]
Initialized.hom [in hom]
Initialized.initiate [in initiate]
Initialized.initium [in initium]
Initialized.mixin [in mixin]
Initialized.ob [in ob]
iso_axiom1 [in iso_axiom1]
iso_axiom2 [in iso_axiom2]
iso_hom [in iso_hom]
iso_inv [in iso_inv]


M

mono_axiom [in mono_axiom]
mono_hom [in mono_hom]
mub_closure [in mub_closure]
mub_clos_smallest [in mub_clos_smallest]
mub_clos_mub [in mub_clos_mub]
mub_complete [in mub_complete]
mub_clos_incl [in mub_clos_incl]


N

Nominal.carrier [in carrier]
Nominal.equivariant [in equivariant]
Nominal.eq_mixin [in eq_mixin]
Nominal.eq_axiom [in eq_axiom]
Nominal.map [in map]
Nominal.nominal_mixin [in nominal_mixin]
Nominal.nom_ident [in nom_ident]
Nominal.nom_comp [in nom_comp]
Nominal.papp [in papp]
Nominal.papp_respects [in papp_respects]
Nominal.support [in support]
Nominal.support_axiom [in support_axiom]
Nominal.support_papp [in support_papp]
nom_colim_elem [in nom_colim_elem]
nom_colim_idx [in nom_colim_idx]
NT.axiom [in axiom]
NT.transform [in transform]


O

obeq [in obeq]
obmap [in obmap]
orddec [in orddec]


P

Perm.f [in f]
Perm.fg [in fg]
Perm.g [in g]
Perm.gf [in gf]
Perm.support [in support]
Perm.support_axiom [in support_axiom]
pe_ident [in pe_ident]
PLT.carrier [in carrier]
PLT.class [in class]
PLT.cls_effective [in cls_effective]
PLT.cls_plotkin [in cls_plotkin]
PLT.cls_preord [in cls_preord]
PLT.hom_rel [in hom_rel]
PLT.hom_order [in hom_order]
PLT.hom_directed [in hom_directed]
PolynomialCategory.cartesian_mixin [in cartesian_mixin]
PolynomialCategory.cat_axioms [in cat_axioms]
PolynomialCategory.ccc_mixin [in ccc_mixin]
PolynomialCategory.cocartesian_mixin [in cocartesian_mixin]
PolynomialCategory.comp_mixin [in comp_mixin]
PolynomialCategory.distributive_mixin [in distributive_mixin]
PolynomialCategory.eq_mixin [in eq_mixin]
PolynomialCategory.hom [in hom]
PolynomialCategory.initialized_mixin [in initialized_mixin]
PolynomialCategory.ob [in ob]
PolynomialCategory.terminated_mixin [in terminated_mixin]
powerdom.elem [in elem]
powerdom.elem_inh [in elem_inh]
Preord.axiom [in axiom]
Preord.carrier [in carrier]
Preord.map [in map]
Preord.mixin [in mixin]
Preord.ord [in ord]
Preord.refl [in refl]
Preord.trans [in trans]
PROD.homl [in homl]
PROD.homr [in homr]
PROD.obl [in obl]
PROD.obr [in obr]
project [in project]
Pseudofunctor.assoc [in assoc]
Pseudofunctor.compose [in compose]
Pseudofunctor.compose_natural [in compose_natural]
Pseudofunctor.hom_map [in hom_map]
Pseudofunctor.ident [in ident]
Pseudofunctor.ob_map [in ob_map]
Pseudofunctor.unit1 [in unit1]
Pseudofunctor.unit2 [in unit2]
Pullback.axiom1 [in axiom1]
Pullback.axiom2 [in axiom2]
Pullback.commute [in commute]
Pullback.is_pullback [in is_pullback]
Pullback.map [in map]
Pullback.pb_ob [in pb_ob]
Pullback.pb_f [in pb_f]
Pullback.pb_g [in pb_g]
Pullback.uniq [in uniq]


S

setdec [in setdec]
SET.carrier [in carrier]
SET.hom_axiom [in hom_axiom]
SET.hom_map [in hom_map]
set.image [in image]
set.image_axiom0 [in image_axiom0]
set.image_axiom1 [in image_axiom1]
set.image_axiom2 [in image_axiom2]
set.member [in member]
set.member_eq [in member_eq]
SET.mixin [in mixin]
set.mixin [in mixin]
set.set [in set]
set.single [in single]
set.single_axiom [in single_axiom]
set.union [in union]
set.union_axiom [in union_axiom]
Support.carrier [in carrier]
Support.support [in support]


T

Terminated.axiom [in axiom]
Terminated.cat_axioms [in cat_axioms]
Terminated.comp_mixin [in comp_mixin]
Terminated.eq_mixin [in eq_mixin]
Terminated.hom [in hom]
Terminated.mixin [in mixin]
Terminated.ob [in ob]
Terminated.terminate [in terminate]
Terminated.terminus [in terminus]



Record Index

A

Adjunction.adjunction [in adjunction]
Alg.alg [in alg]
Alg.alg_hom [in alg_hom]
Alg.initial_alg [in initial_alg]


B

Bicategory.bicategory [in bicategory]
Bicategory.mixin_of [in mixin_of]


C

CartesianClosed.axioms [in axioms]
CartesianClosed.cartesian_closed [in cartesian_closed]
CartesianClosed.mixin_of [in mixin_of]
Cartesian.axioms [in axioms]
Cartesian.cartesian [in cartesian]
Cartesian.mixin_of [in mixin_of]
Category.axioms [in axioms]
Category.category [in category]
Cocartesian.axioms [in axioms]
Cocartesian.cocartesian [in cocartesian]
Cocartesian.mixin_of [in mixin_of]
cocone [in cocone]
color [in color]
Comp.mixin_of [in mixin_of]
Comp.type [in type]
concrete [in concrete]
Cone.cone [in cone]
Cone.cone_hom [in cone_hom]
CPO.hom [in hom]
CPO.mixin_of [in mixin_of]
CPO.type [in type]


D

directed_preord [in directed_preord]
directed_colimit [in directed_colimit]
directed_system [in directed_system]
Distributive.distributive [in distributive]
Distributive.mixin_of [in mixin_of]


E

effective_order [in effective_order]
embedding [in embedding]
enumtype.enumtype [in enumtype]
epimorphism [in epimorphism]
ep_pair [in ep_pair]
eq_dec [in eq_dec]
Eq.mixin_of [in mixin_of]
Eq.type [in type]


F

finprod.termmodel [in termmodel]
fintype.fintype [in fintype]
Functor.functor [in functor]


G

Groupoid.axioms [in axioms]
Groupoid.groupoid [in groupoid]
Groupoid.mixin_of [in mixin_of]


I

Initialized.initialized [in initialized]
Initialized.mixin_of [in mixin_of]
isomorphism [in isomorphism]
is_ep_pair [in is_ep_pair]


L

limset [in limset]


M

monomorphism [in monomorphism]


N

Nominal.hom [in hom]
Nominal.mixin_of [in mixin_of]
Nominal.ob [in ob]
nom_colimit_type [in nom_colimit_type]
nom_exp_type [in nom_exp_type]
NT.nt [in nt]


O

ord_dec [in ord_dec]


P

Perm.perm [in perm]
plotkin_order [in plotkin_order]
PLT.class_of [in class_of]
PLT.hom [in hom]
PLT.ob [in ob]
pointed [in pointed]
PolynomialCategory.polynomial_category [in polynomial_category]
powerdom.pdom_elem [in pdom_elem]
Preord.hom [in hom]
Preord.mixin_of [in mixin_of]
Preord.type [in type]
PROD.prod_ob [in prod_ob]
PROD.prod_hom [in prod_hom]
Pseudofunctor.pseudofunctor [in pseudofunctor]
Pullback.pullback [in pullback]
Pullback.square [in square]


S

semidec [in semidec]
set_dec [in set_dec]
SET.hom [in hom]
set.mixin_of [in mixin_of]
SET.ob [in ob]
set.theory [in theory]
Support.supported [in supported]


T

Terminated.mixin_of [in mixin_of]
Terminated.terminated [in terminated]



Lemma Index

A

adequacy [in adequacy]
adequacy [in adequacy]
adequacy [in adequacy]
adequacy [in adequacy]
adj_inv_eq_converse [in adj_inv_eq_converse]
adj_counit_inv_ntish [in adj_counit_inv_ntish]
adj_counit_rel_elem [in adj_counit_rel_elem]
adj_unit_rel_elem [in adj_unit_rel_elem]
adj_counit_inv_largest [in adj_counit_inv_largest]
adj_counit_inv_eq [in adj_counit_inv_eq]
adj_counit_inv_le [in adj_counit_inv_le]
adj_inv_eq [in adj_inv_eq]
Alg.cata_axiom' [in cata_axiom']
Alg.initial_inj_epic [in initial_inj_epic]
Alg.in_out [in in_out]
Alg.out_in [in out_in]
all_jrels_complete [in all_jrels_complete]
all_finset_setdec_elem [in all_finset_setdec_elem]
all_jrels_inh' [in all_jrels_inh']
all_jrels_inh [in all_jrels_inh]
alpha_cong_denote' [in alpha_cong_denote']
alpha_cong_denote' [in alpha_cong_denote']
alpha_eq_trans [in alpha_eq_trans]
alpha_eq_trans [in alpha_eq_trans]
alpha_eq_sym [in alpha_eq_sym]
alpha_eq_sym [in alpha_eq_sym]
alpha_cong_eq [in alpha_cong_eq]
alpha_cong_eq [in alpha_cong_eq]
alpha_cong_wk [in alpha_cong_wk]
alpha_cong_wk [in alpha_cong_wk]
alpha_eq_refl [in alpha_eq_refl]
alpha_eq_refl [in alpha_eq_refl]
alpha_cong_denote [in alpha_cong_denote]
alpha_cong_denote [in alpha_cong_denote]
alpha_cong_value [in alpha_cong_value]
alpha_cong_value [in alpha_cong_value]
antistrict_pair_commute1 [in antistrict_pair_commute1]
antistrict_pair_commute2 [in antistrict_pair_commute2]
antistrict_nonbottom [in antistrict_nonbottom]
apply_acceptable_ok [in apply_acceptable_ok]
apply_rel_elem [in apply_rel_elem]
apply_acceptable_dec [in apply_acceptable_dec]
apply_rel_dir [in apply_rel_dir]
apply_rel_ordering [in apply_rel_ordering]
app_not_value [in app_not_value]
app_not_value [in app_not_value]
app_elem [in app_elem]
atom_strong_eq [in atom_strong_eq]


B

bilimit_cpo_colimit [in bilimit_cpo_colimit]
bilimit_cpo_colimit1 [in bilimit_cpo_colimit1]
bilimit_cpo_colimit2 [in bilimit_cpo_colimit2]
binding_fmap_ident [in binding_fmap_ident]
binding_fmap_compose [in binding_fmap_compose]
binding_equiv_forall [in binding_equiv_forall]
binding_fmap_respects [in binding_fmap_respects]


C

canonical_bool [in canonical_bool]
cast_iso1 [in cast_iso1]
cast_iso2 [in cast_iso2]
cast_dec_id [in cast_dec_id]
cast_refl [in cast_refl]
cast_compose [in cast_compose]
cast_rel_elem [in cast_rel_elem]
cata_hom_iter_hom [in cata_hom_iter_hom]
cbnLamF_continuous [in cbnLamF_continuous]
cbvLamF_continuous [in cbvLamF_continuous]
chain_induction [in chain_induction]
check_inh [in check_inh]
choose_elem [in choose_elem]
choose_ub [in choose_ub]
choose_finset_sub [in choose_finset_sub]
choose_finset_in [in choose_finset_in]
colimit_decompose [in colimit_decompose]
composeF_continuous [in composeF_continuous]
compose_directed [in compose_directed]
compose_ident_rel1 [in compose_ident_rel1]
compose_ident_rel2 [in compose_ident_rel2]
compose_elem [in compose_elem]
compose_ordering [in compose_ordering]
compose_term_subst [in compose_term_subst]
compose_term_subst [in compose_term_subst]
compose_assoc [in compose_assoc]
cons_elem [in cons_elem]
cons_subset [in cons_subset]
cons_morphism [in cons_morphism]
continuous_equiv [in continuous_equiv]
continuous_pair [in continuous_pair]
continuous_sequence [in continuous_sequence]
continuous_pi1 [in continuous_pi1]
continuous_pi2 [in continuous_pi2]
countable_indefinite_description [in countable_indefinite_description]
CPO.axiom [in axiom]
CPO.cat_axioms [in cat_axioms]
CPO.continuous_sup [in continuous_sup]
CPO.continuous_sup' [in continuous_sup']
CPO.sup_is_lub [in sup_is_lub]
cppo_bot_least [in cppo_bot_least]
curry_rel_ordering [in curry_rel_ordering]
curry_acceptable_semidec [in curry_acceptable_semidec]
curry_commute2 [in curry_commute2]
curry_commute3 [in curry_commute3]
curry_apply [in curry_apply]
curry_universal [in curry_universal]
curry_univ [in curry_univ]
curry_commute [in curry_commute]
curry_rel_elem [in curry_rel_elem]
curry_rel_dir [in curry_rel_dir]


D

dec_conj [in dec_conj]
deflate_inflate0' [in deflate_inflate0']
deflate_inflate1' [in deflate_inflate1']
deflate_inflate' [in deflate_inflate']
deflate_inflate0 [in deflate_inflate0]
deflate_inflate1 [in deflate_inflate1]
deflate_inflate [in deflate_inflate]
deflate00 [in deflate00]
deflate00' [in deflate00']
deflate01 [in deflate01]
deflate01' [in deflate01']
deflate10 [in deflate10]
deflate10' [in deflate10']
deflate11 [in deflate11]
deflate11' [in deflate11']
denote_bottom_nonvalue [in denote_bottom_nonvalue]
denote_bottom_nonvalue [in denote_bottom_nonvalue]
directed_joinables [in directed_joinables]
disc_elem_inj [in disc_elem_inj]
disc_cases_elem [in disc_cases_elem]
disc_cases_univ [in disc_cases_univ]
disc_cases_commute [in disc_cases_commute]
disc_cases_elem' [in disc_cases_elem']


E

eff_in_dec [in eff_in_dec]
either_univ [in either_univ]
elem_inh [in elem_inh]
elist_elem [in elist_elem]
embed_func_is_ep_pair [in embed_func_is_ep_pair]
embed_func_reflects [in embed_func_reflects]
embed_rel_elem [in embed_rel_elem]
embed_ep_roundtrip1 [in embed_ep_roundtrip1]
embed_ep_roundtrip2 [in embed_ep_roundtrip2]
embed_unlift [in embed_unlift]
embed_lift' [in embed_lift']
embed_func_directed0 [in embed_func_directed0]
embed_func_directed2 [in embed_func_directed2]
embed_image_inhabited [in embed_image_inhabited]
embed_unlift' [in embed_unlift']
embed_cat_axioms [in embed_cat_axioms]
embed_lift [in embed_lift]
empty_elem [in empty_elem]
empty_semidirected [in empty_semidirected]
enumtype.enumtype_has_normals [in enumtype_has_normals]
enumtype.order_discrete [in order_discrete]
enumtype.strong_eq [in strong_eq]
env_supp_inenv [in env_supp_inenv]
env_supp_inenv [in env_supp_inenv]
env_dec [in env_dec]
env_dec [in env_dec]
eprod_elem [in eprod_elem]
ep_semidec [in ep_semidec]
ep_cat_axioms [in ep_cat_axioms]
ep_pair_embed_eq_proj_eq [in ep_pair_embed_eq_proj_eq]
eq_ord' [in eq_ord']
eq_refl [in eq_refl]
eq_trans [in eq_trans]
eq_symm [in eq_symm]
eq_ord [in eq_ord]
erel_inv_image_elem [in erel_inv_image_elem]
erel_image_elem [in erel_image_elem]
eset.mixin [in mixin]
esubset_dec_elem [in esubset_dec_elem]
esubset_elem [in esubset_elem]
esum_right_elem [in esum_right_elem]
esum_left_elem [in esum_left_elem]
eta_semvalue [in eta_semvalue]
eval_no_redex [in eval_no_redex]
eval_alpha [in eval_alpha]
eval_alpha [in eval_alpha]
eval_app_congruence [in eval_app_congruence]
eval_app_congruence [in eval_app_congruence]
eval_eq [in eval_eq]
eval_eq [in eval_eq]
eval_eq [in eval_eq]
eval_eq [in eval_eq]
eval_trans [in eval_trans]
eval_trans [in eval_trans]
eval_trans [in eval_trans]
eval_trans [in eval_trans]
eval_lrapp_congruence [in eval_lrapp_congruence]
eval_lrapp_congruence [in eval_lrapp_congruence]
eval_value [in eval_value]
eval_value [in eval_value]
eval_value [in eval_value]
eval_value [in eval_value]
expF_continuous [in expF_continuous]
exp_fmap_ident [in exp_fmap_ident]
exp_fmap_respects [in exp_fmap_respects]
exp_fmap_compose [in exp_fmap_compose]
extend_shift_alpha [in extend_shift_alpha]
extend_shift_alpha [in extend_shift_alpha]


F

fconst_continuous [in fconst_continuous]
finprod_elem [in finprod_elem]
finprod.bind_unbind [in bind_unbind]
finprod.bind_weaken [in bind_weaken]
finprod.empty_cxt_uniq [in empty_cxt_uniq]
finprod.empty_cxt_le [in empty_cxt_le]
finprod.env_incl_wk [in env_incl_wk]
finprod.finprod_proj_commute [in finprod_proj_commute]
finprod.finprod_universal [in finprod_universal]
finprod.internals.codom_has_normals [in codom_has_normals]
finprod.internals.enum_finprod_complete [in enum_finprod_complete]
finprod.internals.finprod_univ_commute [in finprod_univ_commute]
finprod.internals.finprod_univ_axiom [in finprod_univ_axiom]
finprod.internals.finprod_univ_rel_elem [in finprod_univ_rel_elem]
finprod.internals.finprod_has_normals [in finprod_has_normals]
finprod.internals.f_cons_mono [in f_cons_mono]
finprod.internals.f_cons_hd_tl [in f_cons_hd_tl]
finprod.internals.f_cons_reflects1 [in f_cons_reflects1]
finprod.internals.f_cons_reflects2 [in f_cons_reflects2]
finprod.internals.proj_rel_elem [in proj_rel_elem]
finprod.lookup_eq [in lookup_eq]
FINPROD.lookup_eq [in lookup_eq]
finprod.lookup_app [in lookup_app]
finprod.lookup_neq [in lookup_neq]
FINPROD.lookup_neq [in lookup_neq]
finprod.mk_finprod_compose_commute [in mk_finprod_compose_commute]
finprod.proj_bind_neq [in proj_bind_neq]
finprod.proj_weaken [in proj_weaken]
finprod.proj_bind [in proj_bind]
finprod.proj_bind_eq [in proj_bind_eq]
finprod.shift_vars' [in shift_vars']
finprod.subst_soundness_lemma [in subst_soundness_lemma]
finprod.subst_soundness [in subst_soundness]
finprod.term_subst_soundness [in term_subst_soundness]
finprod.unbind_lemma [in unbind_lemma]
FINPROD.unbind_lemma [in unbind_lemma]
finprod.varmap_extend_bind [in varmap_extend_bind]
finprod.varmap_compose_denote [in varmap_compose_denote]
finprod.varmap_shift_bind [in varmap_shift_bind]
finprod.varmap_denote_proj [in varmap_denote_proj]
finprod.varmap_var_id [in varmap_var_id]
finprod.weaken_fresh [in weaken_fresh]
finprod.weaken_map_denote [in weaken_map_denote]
finprod.weaken_term_denote [in weaken_term_denote]
finrel_decompose [in finrel_decompose]
finset_sub_image [in finset_sub_image]
finset_remove_elem [in finset_remove_elem]
finset_remove_length1 [in finset_remove_length1]
finset_remove_length2 [in finset_remove_length2]
finset_in_dec [in finset_in_dec]
finset_decompose [in finset_decompose]
finset_find_dec' [in finset_find_dec']
finset_cons_eq [in finset_cons_eq]
finset_find_dec [in finset_find_dec]
finsubsets_complete [in finsubsets_complete]
finsubset_dec' [in finsubset_dec']
finsubset_elem [in finsubset_elem]
finsubset_dec [in finsubset_dec]
finsum_right_elem [in finsum_right_elem]
finsum_left_elem [in finsum_left_elem]
fintype.order_discrete [in order_discrete]
fintype.strong_eq [in strong_eq]
fin_list_intersect_elem [in fin_list_intersect_elem]
fin_intersect_elem [in fin_intersect_elem]
fixes_mono [in fixes_mono]
fixes_eq [in fixes_eq]
fixes_unroll [in fixes_unroll]
fixes_compose_commute [in fixes_compose_commute]
fixpoint_alt_out_in [in fixpoint_alt_out_in]
fixpoint_alt_in_out [in fixpoint_alt_in_out]
fix_not_value [in fix_not_value]
flat_cases'_strict [in flat_cases'_strict]
flat_cases_elem' [in flat_cases_elem']
flat_cases'_semvalue [in flat_cases'_semvalue]
flat_cases_univ' [in flat_cases_univ']
flat_cases_rel_elem [in flat_cases_rel_elem]
flat_cases_univ [in flat_cases_univ]
flat_elem'_ignores_arg [in flat_elem'_ignores_arg]
flat_elem'_inj [in flat_elem'_inj]
flat_elem_inj [in flat_elem_inj]
flat_elem_canon [in flat_elem_canon]
flat_elem'_semvalue [in flat_elem'_semvalue]
flat_cases_commute [in flat_cases_commute]
flat_cases_commute [in flat_cases_commute]
flat_cases_elem [in flat_cases_elem]
forgetEMBED_continuous [in forgetEMBED_continuous]
fresh_atom_is_fresh' [in fresh_atom_is_fresh']
fresh_atom_is_fresh [in fresh_atom_is_fresh]
fresh_idents_inhabited [in fresh_idents_inhabited]
fstF_continuous [in fstF_continuous]
fstF_continuous' [in fstF_continuous']
fundamental_lemma [in fundamental_lemma]
fundamental_lemma [in fundamental_lemma]
fundamental_lemma [in fundamental_lemma]
fundamental_lemma [in fundamental_lemma]
fundamental_lemma' [in fundamental_lemma']
fundamental_lemma' [in fundamental_lemma']
fundamental_lemma' [in fundamental_lemma']
fundamental_lemma' [in fundamental_lemma']
f_explode [in f_explode]


H

hom_rel_pair_map [in hom_rel_pair_map]
HSle0 [in HSle0]


I

identF_continuous [in identF_continuous]
idents_find_len_aux [in idents_find_len_aux]
idents_find [in idents_find]
ident_ordering [in ident_ordering]
ident_image_dir [in ident_image_dir]
ident_elem [in ident_elem]
if_not_value [in if_not_value]
if_not_value [in if_not_value]
image_axiom0 [in image_axiom0]
image_axiom1 [in image_axiom1]
image_axiom2 [in image_axiom2]
image_axiom1' [in image_axiom1']
image_compose [in image_compose]
incl_refl [in incl_refl]
incl_unlift [in incl_unlift]
incl_trans [in incl_trans]
inenv_varcong [in inenv_varcong]
inenv_varcong [in inenv_varcong]
inert_semvalue [in inert_semvalue]
inhabited_einhabited [in inhabited_einhabited]
inh_eq [in inh_eq]
inh_sub [in inh_sub]
inh_image [in inh_image]
inh_dec [in inh_dec]
initiate_univ [in initiate_univ]
inj_pair2_ty [in inj_pair2_ty]
inj_pair2_ty [in inj_pair2_ty]
inj_pair2_ty [in inj_pair2_ty]
inj_pair2_ty [in inj_pair2_ty]
inl_commute [in inl_commute]
inr_commute [in inr_commute]
intersection_elem [in intersection_elem]
intersect_approx [in intersect_approx]
inv_compose [in inv_compose]
inv_id1 [in inv_id1]
inv_id2 [in inv_id2]
inv_inj [in inv_inj]
inv_inv [in inv_inv]
inv_eq [in inv_eq]
in_unlift [in in_unlift]
iota1_dir [in iota1_dir]
iota1_cases_commute [in iota1_cases_commute]
iota1_elem [in iota1_elem]
iota1_ordering [in iota1_ordering]
iota2_elem [in iota2_elem]
iota2_ordering [in iota2_ordering]
iota2_cases_commute [in iota2_cases_commute]
iota2_dir [in iota2_dir]
is_joinable_unmap_rel [in is_joinable_unmap_rel]
is_joinable_rel_dec [in is_joinable_rel_dec]
is_joinable_rel_dec' [in is_joinable_rel_dec']
is_joinable_rel_dec0 [in is_joinable_rel_dec0]
is_joinable_map_rel [in is_joinable_map_rel]
iter_le [in iter_le]
iter_hom_proof_irr [in iter_hom_proof_irr]
iter_hom_proof_irr [in iter_hom_proof_irr]
iter_chain_base [in iter_chain_base]
iter_set_directed [in iter_set_directed]
iter_chain_step [in iter_chain_step]


J

joinable_ord_dec [in joinable_ord_dec]
joinable_rels_normal [in joinable_rels_normal]
joinable_rel_has_normals [in joinable_rel_has_normals]


L

lamModelCBN_iso [in lamModelCBN_iso]
lamModelCBV_iso [in lamModelCBV_iso]
left_right_finset_finsum [in left_right_finset_finsum]
left_finset_elem [in left_finset_elem]
lfp_fixpoint [in lfp_fixpoint]
lfp_least [in lfp_least]
lfp_uniform [in lfp_uniform]
liftEMBED_continuous [in liftEMBED_continuous]
liftPPLT_rel_elem [in liftPPLT_rel_elem]
lift_prod'_natural [in lift_prod'_natural]
lift_prod_pair' [in lift_prod_pair']
lift_prod_pair [in lift_prod_pair]
lift_map_eq [in lift_map_eq]
lift_map_id [in lift_map_id]
lift_unit_id1 [in lift_unit_id1]
lift_unit_id2 [in lift_unit_id2]
lift_prod_natural [in lift_prod_natural]
lift_has_normals [in lift_has_normals]
lift_map_compose [in lift_map_compose]
lift_prod_id1 [in lift_prod_id1]
lift_prod_id2 [in lift_prod_id2]
limord_univ_uniq [in limord_univ_uniq]
limord_univ_commute [in limord_univ_commute]
limord_has_normals [in limord_has_normals]
limset_spoke_commute [in limset_spoke_commute]
limset_order_trans [in limset_order_trans]
limset_order_dec [in limset_order_dec]
limset_order_exists_forall [in limset_order_exists_forall]
limset_order_refl [in limset_order_refl]
list_finsubsets_complete [in list_finsubsets_complete]
list_finsubsets_correct [in list_finsubsets_correct]
lrsemapp_equiv [in lrsemapp_equiv]
lrsemapp_equiv [in lrsemapp_equiv]
LR_IF [in LR_IF]
LR_IF [in LR_IF]
LR_I [in LR_I]
LR_I [in LR_I]
LR_K [in LR_K]
LR_K [in LR_K]
LR_S [in LR_S]
LR_S [in LR_S]
LR_Y [in LR_Y]
LR_Ybody [in LR_Ybody]
LR_admissible [in LR_admissible]
LR_admissible [in LR_admissible]
LR_alpha_cong [in LR_alpha_cong]
LR_under_apply [in LR_under_apply]
LR_under_apply [in LR_under_apply]
LR_equiv [in LR_equiv]
LR_equiv [in LR_equiv]
LR_equiv [in LR_equiv]
LR_equiv [in LR_equiv]
L_reflects [in L_reflects]
L_mono [in L_mono]
L_hom_rel [in L_hom_rel]


M

map_rel_in [in map_rel_in]
map_rel_inh [in map_rel_inh]
max_len_le [in max_len_le]
member_eq [in member_eq]
member_inhabited [in member_inhabited]
minimal_upper_bound_ok [in minimal_upper_bound_ok]
mkrel_ord [in mkrel_ord]
mkrel_mono [in mkrel_mono]
mkrel_mono' [in mkrel_mono']
mkrel_dec [in mkrel_dec]
mkrel_dir [in mkrel_dir]
mk_disc_cases_elem [in mk_disc_cases_elem]
mub_finset_dec [in mub_finset_dec]
mub_clos_idem [in mub_clos_idem]
mub_closed_intersect [in mub_closed_intersect]
mub_clos_mono [in mub_clos_mono]
mub_closed_normal_set [in mub_closed_normal_set]


N

ne_finsubsets_complete [in ne_finsubsets_complete]
nil_subset [in nil_subset]
nil_elem [in nil_elem]
Niter_succ [in Niter_succ]
Nominal.category_axioms [in category_axioms]
nom_compose' [in nom_compose']
nom_compose [in nom_compose]
nom_ident' [in nom_ident']
nom_colimit_commute [in nom_colimit_commute]
nom_ident [in nom_ident]
nom_colimit_uniq [in nom_colimit_uniq]
normalizing [in normalizing]
normalizing [in normalizing]
normal_mubs' [in normal_mubs']
normal_has_ubs [in normal_has_ubs]
normal_set_mub_closed [in normal_set_mub_closed]
normal_sub_mub_closed_dec [in normal_sub_mub_closed_dec]
normal_set_mub_closed_sets [in normal_set_mub_closed_sets]
normal_sub_mub_dec [in normal_sub_mub_dec]
normal_set_mub_closure [in normal_set_mub_closure]
normal_has_mubs [in normal_has_mubs]
nt_cat_axioms [in nt_cat_axioms]


O

ord_trans [in ord_trans]
ord_antisym [in ord_antisym]
ord_refl [in ord_refl]


P

pairF_continuous [in pairF_continuous]
pairing_unpairing [in pairing_unpairing]
pairing_univ [in pairing_univ]
pairing00 [in pairing00]
pairing01 [in pairing01]
pairing10 [in pairing10]
pairing11 [in pairing11]
pair_rel_eq [in pair_rel_eq]
pair_rel_elem' [in pair_rel_elem']
pair_rel_universal_le [in pair_rel_universal_le]
pair_proj_commute1 [in pair_proj_commute1]
pair_proj_commute2 [in pair_proj_commute2]
pair_right_continuous [in pair_right_continuous]
pair_bottom1 [in pair_bottom1]
pair_bottom2 [in pair_bottom2]
pair_rel_ordering [in pair_rel_ordering]
pair_proj_commute1_le [in pair_proj_commute1_le]
pair_rel_order' [in pair_rel_order']
pair_left_continuous [in pair_left_continuous]
pair_rel_dir [in pair_rel_dir]
pair_proj_commute2_le [in pair_proj_commute2_le]
pair_rel_universal [in pair_rel_universal]
pair_rel_elem [in pair_rel_elem]
papp_inj [in papp_inj]
pdom_map_lower_ord [in pdom_map_lower_ord]
pdom_map_upper_ord [in pdom_map_upper_ord]
perms_neq_nil [in perms_neq_nil]
perms_len [in perms_len]
perm_commute [in perm_commute]
Perm.assoc [in assoc]
Perm.category_axioms [in category_axioms]
Perm.f_inj [in f_inj]
Perm.g_inj [in g_inj]
Perm.inv_id1 [in inv_id1]
Perm.inv_id2 [in inv_id2]
Perm.support_perm' [in support_perm']
Perm.support_perm [in support_perm]
Perm.swap_swap [in swap_swap]
Perm.swap_swizzle [in swap_swizzle]
Perm.swap_same_id [in swap_same_id]
Perm.swap_self_inv [in swap_self_inv]
pi1_rel_ordering [in pi1_rel_ordering]
pi1_rel_elem [in pi1_rel_elem]
pi1_greatest [in pi1_greatest]
pi1_rel_dir [in pi1_rel_dir]
pi2_rel_ordering [in pi2_rel_ordering]
pi2_rel_elem [in pi2_rel_elem]
pi2_greatest [in pi2_greatest]
pi2_rel_dir [in pi2_rel_dir]
plt_hom_adj1 [in plt_hom_adj1]
plt_hom_adj2 [in plt_hom_adj2]
plt_terminate_univ [in plt_terminate_univ]
plt_strict_compose [in plt_strict_compose]
plt_bot_None [in plt_bot_None]
plt_has_normals [in plt_has_normals]
plt_bot_chomp [in plt_bot_chomp]
plt_semvalue_bot [in plt_semvalue_bot]
plt_const_rel_elem [in plt_const_rel_elem]
PLT.app_hom_rel [in app_hom_rel]
PLT.cat_axioms [in cat_axioms]
PLT.compose_mono [in compose_mono]
PLT.compose_hom_rel [in compose_hom_rel]
PLT.curry_mono [in curry_mono]
PLT.curry_apply2 [in curry_apply2]
PLT.curry_apply3 [in curry_apply3]
PLT.curry_eq [in curry_eq]
PLT.curry_compose_commute [in curry_compose_commute]
PLT.curry_apply [in curry_apply]
PLT.curry_universal [in curry_universal]
PLT.curry_hom_rel [in curry_hom_rel]
PLT.initiate_univ [in initiate_univ]
PLT.iota1_cases_commute [in iota1_cases_commute]
PLT.iota2_cases_commute [in iota2_cases_commute]
PLT.pair_map_pair [in pair_map_pair]
PLT.pair_mono [in pair_mono]
PLT.pair_universal [in pair_universal]
PLT.pair_le_commute1 [in pair_le_commute1]
PLT.pair_le_commute2 [in pair_le_commute2]
PLT.pair_map_eq [in pair_map_eq]
PLT.pair_hom_rel [in pair_hom_rel]
PLT.pair_commute1 [in pair_commute1]
PLT.pair_commute2 [in pair_commute2]
PLT.pair_eq [in pair_eq]
PLT.pair_universal_le [in pair_universal_le]
PLT.pair_compose_commute [in pair_compose_commute]
PLT.sum_cases_universal [in sum_cases_universal]
PLT.sum_cases_hom_rel [in sum_cases_hom_rel]
PLT.sum_cases_eq [in sum_cases_eq]
PLT.sum_cases_mono [in sum_cases_mono]
PLT.terminate_le_univ [in terminate_le_univ]
postcompose_continuous [in postcompose_continuous]
powerdomain_continuous [in powerdomain_continuous]
powerdom.concat_elem_mono [in concat_elem_mono]
powerdom.concat_in [in concat_in]
powerdom.convex_union_natural [in convex_union_natural]
powerdom.convex_ord_trans [in convex_ord_trans]
powerdom.convex_ord_refl [in convex_ord_refl]
powerdom.empty_join1 [in empty_join1]
powerdom.empty_join2 [in empty_join2]
powerdom.empty_unit2 [in empty_unit2]
powerdom.empty_unit [in empty_unit]
powerdom.empty_natural [in empty_natural]
powerdom.empty_rel_elem [in empty_rel_elem]
powerdom.enum_elems_complete [in enum_elems_complete]
powerdom.fmap_rel_elem [in fmap_rel_elem]
powerdom.fmap_upper_semidec [in fmap_upper_semidec]
powerdom.fmap_convex_semidec [in fmap_convex_semidec]
powerdom.fmap_lower_semidec [in fmap_lower_semidec]
powerdom.fmap_monotone [in fmap_monotone]
powerdom.fmap_convex_swell [in fmap_convex_swell]
powerdom.fmap_respects [in fmap_respects]
powerdom.join_rel_elem [in join_rel_elem]
powerdom.join_natural [in join_natural]
powerdom.lower_ord_refl [in lower_ord_refl]
powerdom.lower_ord_trans [in lower_ord_trans]
powerdom.lower_ord_dec [in lower_ord_dec]
powerdom.lower_union_natural1 [in lower_union_natural1]
powerdom.lower_union_natural2 [in lower_union_natural2]
powerdom.monad_assoc [in monad_assoc]
powerdom.monad_unit1 [in monad_unit1]
powerdom.monad_unit2 [in monad_unit2]
powerdom.normal_pdoms_in [in normal_pdoms_in]
powerdom.normal_pdoms_in' [in normal_pdoms_in']
powerdom.pdom_elem_eq_upper [in pdom_elem_eq_upper]
powerdom.pdom_elem_eq_eq [in pdom_elem_eq_eq]
powerdom.pdom_elem_eq_le [in pdom_elem_eq_le]
powerdom.pdom_has_normals [in pdom_has_normals]
powerdom.pdom_elem_eq_lower [in pdom_elem_eq_lower]
powerdom.pdom_fmap_id [in pdom_fmap_id]
powerdom.pdom_ord_dec [in pdom_ord_dec]
powerdom.pdom_fmap_compose [in pdom_fmap_compose]
powerdom.select_pdoms_in [in select_pdoms_in]
powerdom.select_pdoms_in' [in select_pdoms_in']
powerdom.single_natural [in single_natural]
powerdom.single_elem_mono [in single_elem_mono]
powerdom.single_rel_elem [in single_rel_elem]
powerdom.union_rel_elem [in union_rel_elem]
powerdom.union_assoc_le [in union_assoc_le]
powerdom.union_idem [in union_idem]
powerdom.union_elem_convex_ord [in union_elem_convex_ord]
powerdom.union_elem_lower_ord [in union_elem_lower_ord]
powerdom.union_elem_upper_ord [in union_elem_upper_ord]
powerdom.union_lower [in union_lower]
powerdom.union_assoc [in union_assoc]
powerdom.union_join [in union_join]
powerdom.union_elem_pdom_ord [in union_elem_pdom_ord]
powerdom.union_commute [in union_commute]
powerdom.union_upper [in union_upper]
powerdom.union_commute_le [in union_commute_le]
powerdom.upper_ord_refl [in upper_ord_refl]
powerdom.upper_ord_trans [in upper_ord_trans]
powerdom.upper_union_natural [in upper_union_natural]
powerdom.upper_ord_dec [in upper_ord_dec]
precompose_continuous [in precompose_continuous]
preord_eq [in preord_eq]
preord_ord [in preord_ord]
Preord.cat_axioms [in cat_axioms]
prodF_continuous [in prodF_continuous]
prod_has_normals [in prod_has_normals]
PROD.prod_cat_axioms [in prod_cat_axioms]
project_rel_elem [in project_rel_elem]
proj1_commute [in proj1_commute]
proj2_commute [in proj2_commute]
prove_directed [in prove_directed]
Psi_inv_reflects [in Psi_inv_reflects]
Psi_inv_mono [in Psi_inv_mono]
Psi_mono [in Psi_mono]
Psi_reflects [in Psi_reflects]
Pullback.pb_lemma1_comm [in pb_lemma1_comm]


R

redex_eq [in redex_eq]
redex_eq [in redex_eq]
redex_inert_false [in redex_inert_false]
redex_soundness [in redex_soundness]
redex_soundness [in redex_soundness]
redex_or_inert' [in redex_or_inert']
redex_or_inert [in redex_or_inert]
repack_equal [in repack_equal]
right_finset_elem [in right_finset_elem]
RS_elem' [in RS_elem']
RS_elem [in RS_elem]
R'_R [in R'_R]


S

scott_induction [in scott_induction]
select_jrels_elem1 [in select_jrels_elem1]
select_jrels_elem2 [in select_jrels_elem2]
semidec_iff [in semidec_iff]
semidec_ex [in semidec_ex]
semidec_in [in semidec_in]
semvalue_le [in semvalue_le]
semvalue_equiv [in semvalue_equiv]
semvalue_app_out1' [in semvalue_app_out1']
semvalue_app_out2' [in semvalue_app_out2']
semvalue_sup [in semvalue_sup]
semvalue_sup [in semvalue_sup]
semvalue_lrsemapp_out [in semvalue_lrsemapp_out]
semvalue_strict_app_out1 [in semvalue_strict_app_out1]
semvalue_strict_app_out2 [in semvalue_strict_app_out2]
single_axiom [in single_axiom]
smash_prod_iff [in smash_prod_iff]
smash_unsmash [in smash_unsmash]
sndF_continuous [in sndF_continuous]
sndF_continuous' [in sndF_continuous']
soundness [in soundness]
soundness [in soundness]
soundness [in soundness]
soundness [in soundness]
strictify_le [in strictify_le]
strictify_largest [in strictify_largest]
strict_curry_compose_commute' [in strict_curry_compose_commute']
strict_map [in strict_map]
strict_app_bot' [in strict_app_bot']
strict_curry'_semvalue2 [in strict_curry'_semvalue2]
strict_curry_app2' [in strict_curry_app2']
strict_curry_app [in strict_curry_app]
strict_curry_monotone [in strict_curry_monotone]
strict_app_bot [in strict_app_bot]
strict_curry'_eq [in strict_curry'_eq]
strict_curry'_monotone [in strict_curry'_monotone]
strict_curry_app_converse [in strict_curry_app_converse]
strict_curry'_semvalue [in strict_curry'_semvalue]
strict_curry_app' [in strict_curry_app']
strict_curry_app2 [in strict_curry_app2]
strict_curry_eq [in strict_curry_eq]
strict_curry_compose_commute [in strict_curry_compose_commute]
subst_alpha_ident [in subst_alpha_ident]
subst_alpha_ident [in subst_alpha_ident]
subst_soundness [in subst_soundness]
subst_soundness [in subst_soundness]
subst_weaken_alpha [in subst_weaken_alpha]
subst_weaken_alpha [in subst_weaken_alpha]
sumF_continuous [in sumF_continuous]
sum_cases_univ [in sum_cases_univ]
sum_cases_ordering [in sum_cases_ordering]
sum_cases_dir [in sum_cases_dir]
sum_cases_elem [in sum_cases_elem]
sum_has_normals [in sum_has_normals]
support_axiom [in support_axiom]
support_axiom' [in support_axiom']
support_papp [in support_papp]
sup_equiv [in sup_equiv]
sup_monotone [in sup_monotone]
swap_induction [in swap_induction]
swap_induction' [in swap_induction']
swap_commute' [in swap_commute']
swap_commute [in swap_commute]
swell [in swell]
swelling_lemma [in swelling_lemma]
swell_inductive_step [in swell_inductive_step]
swell_row [in swell_row]
swell_relation [in swell_relation]
swell_aux [in swell_aux]


T

terminate_le_cancel [in terminate_le_cancel]
terminate_univ [in terminate_univ]
terminate_cancel [in terminate_cancel]
term_wk_ident [in term_wk_ident]
term_wk_ident [in term_wk_ident]
term_subst_cong [in term_subst_cong]
term_subst_cong [in term_subst_cong]
term_subst_wk_cong [in term_subst_wk_cong]
term_subst_wk_cong [in term_subst_wk_cong]
term_wk_compose [in term_wk_compose]
term_wk_compose [in term_wk_compose]
term_wk_compose' [in term_wk_compose']
term_wk_compose' [in term_wk_compose']
traverse_correct [in traverse_correct]
traverse_correct [in traverse_correct]
ty_dec [in ty_dec]
ty_dec [in ty_dec]


U

ub_cons [in ub_cons]
ub_nil [in ub_nil]
unenumerate_uniq [in unenumerate_uniq]
unenumerate_set_inhabited [in unenumerate_set_inhabited]
unenumerate_correct [in unenumerate_correct]
unenumerate_reflects [in unenumerate_reflects]
unfold_find [in unfold_find]
unimage_jrel_order [in unimage_jrel_order]
unimage_jrel_directed [in unimage_jrel_directed]
union_axiom [in union_axiom]
union2_elem [in union2_elem]
unitpo_dec [in unitpo_dec]
unlift_app [in unlift_app]
unmap_rel_sub [in unmap_rel_sub]
unmap_rel [in unmap_rel]
unpairing_pairing [in unpairing_pairing]
unsmash_smash [in unsmash_smash]
upper_bound_dec [in upper_bound_dec]
upper_bound_ok [in upper_bound_ok]
use_ord [in use_ord]
U_mono [in U_mono]
U_hom_rel [in U_hom_rel]
U_reflects [in U_reflects]
U_bottom_least [in U_bottom_least]


V

value_inert_semvalue [in value_inert_semvalue]
value_semvalue [in value_semvalue]
value_semvalue [in value_semvalue]
value_app_inv [in value_app_inv]
varcong_eq [in varcong_eq]
varcong_eq [in varcong_eq]
varcong_inenv1 [in varcong_inenv1]
varcong_inenv1 [in varcong_inenv1]
varcong_inenv2 [in varcong_inenv2]
varcong_inenv2 [in varcong_inenv2]
var_cong_sym [in var_cong_sym]
var_cong_sym [in var_cong_sym]
var_cong_trans [in var_cong_trans]
var_cong_trans [in var_cong_trans]
var_cong_refl [in var_cong_refl]
var_cong_refl [in var_cong_refl]


W

weak_countable_choice [in weak_countable_choice]
wf_idents_wf [in wf_idents_wf]


Y

Ybody_unroll [in Ybody_unroll]



Section Index

A

Adjunction.adjunction [in adjunction]
Alg.alg [in alg]
Alg.forget [in forget]


B

Bicategory.bicategory [in bicategory]
bilimit [in bilimit]
bilimit.bilimit_univ [in bilimit_univ]
bottom [in bottom]


C

CartesianClosed.cartesian_closed.axioms [in axioms]
CartesianClosed.cartesian_closed [in cartesian_closed]
Cartesian.cartesian [in cartesian]
Cartesian.cartesian.axioms [in axioms]
cast [in cast]
CAT [in CAT]
category_axioms [in category_axioms]
Category.category [in category]
Cocartesian.cocartesian [in cocartesian]
Cocartesian.cocartesian.axioms [in axioms]
colimit_decompose2 [in colimit_decompose2]
colimit_decompose [in colimit_decompose]
colored_sets.colored_sets [in colored_sets]
colored_sets.colored_sets.cunion [in cunion]
Cone.cone [in cone]
countable_ID [in countable_ID]
CPO.prod [in prod]
curry [in curry]


D

dec_lemmas [in dec_lemmas]
directed_joinables.swell [in swell]
directed_joinables [in directed_joinables]
directed_joinables.swell.swell_relation [in swell_relation]
disc_cases [in disc_cases]
Distributive.distributive [in distributive]


E

epic [in epic]
ep_pairs [in ep_pairs]
ep_pairs.embed_func_ep_pair [in embed_func_ep_pair]
ep_pairs.ep_pair_embed_func.embed_func [in embed_func]
ep_pairs.ep_pair_embed_func [in ep_pair_embed_func]
eset.eset [in eset]
expF_decompose [in expF_decompose]
exp_functor [in exp_functor]


F

finprod.internals.finprod_univ_rel [in finprod_univ_rel]
finprod.termmodel [in termmodel]
finprod.termmodel.varmap_compose [in varmap_compose]
finprod.varmap [in varmap]
finset.finset [in finset]
finsubset [in finsubset]
fixes [in fixes]
fixpoint [in fixpoint]
fixpoint [in fixpoint]
fixpoint.cata [in cata]
flat_cases [in flat_cases]
fresh [in fresh]
fstF_continuous [in fstF_continuous]
functor_compose [in functor_compose]
Functor.functor [in functor]


G

Groupoid.groupoid [in groupoid]
Groupoid.groupoid.axioms [in axioms]


I

idents_length [in idents_length]
image_compose [in image_compose]
Initialized.initialized [in initialized]
iso [in iso]
iter_chain [in iter_chain]


J

joinable_plt.join_rel_normal [in join_rel_normal]
joinable_plt [in joinable_plt]


L

lfp [in lfp]


M

map_rel [in map_rel]
mono [in mono]


N

nominal_directed_colimits [in nominal_directed_colimits]
nominal_directed_colimits.nom_colimit_univ [in nom_colimit_univ]
nominal_fixpoint [in nominal_fixpoint]
nom_sum [in nom_sum]
normal_sets.normal_mubs [in normal_mubs]
normal_sets [in normal_sets]
normal_sets.plt_normal [in plt_normal]
NT.nt [in nt]
NT.NT_mixins [in NT_mixins]
NT.nt_compose [in nt_compose]


P

pairF [in pairF]
pairF_continuous [in pairF_continuous]
pairF_continuous.cocones [in cocones]
plt_const [in plt_const]
PLT.PLT [in PLT]
PLT.PLT.homset_cpo [in homset_cpo]
powerdom_decompose [in powerdom_decompose]
powerdom_functor [in powerdom_functor]
powerdom.powerdom [in powerdom]
powerdom.powerdom.orders [in orders]
powerdom.powerdom.powerdomain_fmap [in powerdomain_fmap]
prod_functor [in prod_functor]
PROD.product_category [in product_category]
projF [in projF]
Pullback.pullback [in pullback]
Pullback.pullback_lemma.pullback_lemma1.pb_map [in pb_map]
Pullback.pullback_lemma.pullback_lemma1 [in pullback_lemma1]
Pullback.pullback_lemma [in pullback_lemma]


S

set.mixin_def [in mixin_def]
sndF_continuous [in sndF_continuous]
strictify [in strictify]
sum_functor [in sum_functor]


T

Terminated.terminated [in terminated]
test_functor_assocative_convertability [in test_functor_assocative_convertability]
total_fixpoint [in total_fixpoint]
traverse [in traverse]
traverse [in traverse]


U

unfold [in unfold]


Y

Ydefn [in Ydefn]



Notation Index

B

_ • _ [in ::x_'•'_x]
_ ⋆ _ [in ::x_'⋆'_x]
Id [in ::'Id']
Id ( _ ) [in ::'Id'_'('_x_')']


C

∐ _ (cpo_scope) [in :cpo_scope:'∐'_x]


other

_ ⇒ _ (bicategory_scope) [in :bicategory_scope:x_'⇒'_x]
_ ◃ _ (bicategory_scope) [in :bicategory_scope:x_'◃'_x]
_ → _ (bicategory_scope) [in :bicategory_scope:x_'→'_x]
_ ▹ _ (bicategory_scope) [in :bicategory_scope:x_'▹'_x]
_ · _ (category_hom_scope) [in :category_hom_scope:x_'·'_x]
id ( _ ) (category_hom_scope) [in :category_hom_scope:'id'_'('_x_')']
_ ↔ _ (category_hom_scope) [in :category_hom_scope:x_'↔'_x]
_ ⇒ _ (category_ob_scope) [in :category_ob_scope:x_'⇒'_x]
∗ (category_ops_scope) [in :category_ops_scope:'∗']
_ ▹ _ (category_hom_scope) [in :category_hom_scope:x_'▹'_x]
π₁ (category_ops_scope) [in :category_ops_scope:'π₁']
π₂ (category_ops_scope) [in :category_ops_scope:'π₂']
! (category_ob_scope) [in :category_ob_scope:'!']
¡ (category_ob_scope) [in :category_ob_scope:'¡']
_ ↠ _ (category_hom_scope) [in :category_hom_scope:x_'↠'_x]
_ × _ (category_ob_scope) [in :category_ob_scope:x_'×'_x]
_ # _ (category_hom_scope) [in :category_hom_scope:x_'#'_x]
_ ◃ _ (category_hom_scope) [in :category_hom_scope:x_'◃'_x]
Λ _ (category_ops_scope) [in :category_ops_scope:'Λ'_x]
〈 _ , _ 〉 (category_ops_scope) [in :category_ops_scope:'〈'_x_','_x_'〉']
_ + _ (category_ob_scope) [in :category_ob_scope:x_'+'_x]
id (category_hom_scope) [in :category_hom_scope:'id']
_ → _ (category_hom_scope) [in :category_hom_scope:x_'→'_x]
_ ↣ _ (category_hom_scope) [in :category_hom_scope:x_'↣'_x]
_ ⁻¹ (category_hom_scope) [in :category_hom_scope:x_'⁻¹']
ι₁ (category_ops_scope) [in :category_ops_scope:'ι₁']
ι₂ (category_ops_scope) [in :category_ops_scope:'ι₂']
_ ∘ _ (category_hom_scope) [in :category_hom_scope:x_'∘'_x]
⊥ (cpo_scope) [in :cpo_scope:'⊥']
∐ _ (cpo_scope) [in :cpo_scope:'∐'_x]
_ ≈ _ (equiv_scope) [in :equiv_scope:x_'≈'_x]
_ ≉ _ (equiv_scope) [in :equiv_scope:x_'≉'_x]
〚 _ 〛 (lam_scope) [in :lam_scope:'〚'_x_'〛']
〚 _ 〛 (lam_scope) [in :lam_scope:'〚'_x_'〛']
_ • _ (lam_scope) [in :lam_scope:x_'•'_x]
_ • _ (lam_scope) [in :lam_scope:x_'•'_x]
_ ⊸ _ (plt_scope) [in :plt_scope:x_'⊸'_x]
Λ _ (plt_scope) [in :plt_scope:'Λ'_x]
π₁ (plt_scope) [in :plt_scope:'π₁']
π₂ (plt_scope) [in :plt_scope:'π₂']
_ ⇒ _ (plt_scope) [in :plt_scope:x_'⇒'_x]
0 (plt_scope) [in :plt_scope:'0']
1 (plt_scope) [in :plt_scope:'1']
_ × _ (plt_scope) [in :plt_scope:x_'×'_x]
_ + _ (plt_scope) [in :plt_scope:x_'+'_x]
_ ⊕ _ (plt_scope) [in :plt_scope:x_'⊕'_x]
《 _ , _ 》 (plt_scope) [in :plt_scope:'《'_x_','_x_'》']
ι₁ (plt_scope) [in :plt_scope:'ι₁']
ι₂ (plt_scope) [in :plt_scope:'ι₂']
_ ⊗ _ (plt_scope) [in :plt_scope:x_'⊗'_x]
〈 _ , _ 〉 (plt_scope) [in :plt_scope:'〈'_x_','_x_'〉']
_ ≥ _ (preord_scope) [in :preord_scope:x_'≥'_x]
_ ≰ _ (preord_scope) [in :preord_scope:x_'≰'_x]
_ ≱ _ (preord_scope) [in :preord_scope:x_'≱'_x]
_ ≤ _ (preord_scope) [in :preord_scope:x_'≤'_x]
_ ∈ _ (set_scope) [in :set_scope:x_'∈'_x]
∪ _ (set_scope) [in :set_scope:'∪'_x]
_ ∉ _ (set_scope) [in :set_scope:x_'∉'_x]
_ ⊆ _ (set_scope) [in :set_scope:x_'⊆'_x]
〚 _ 〛 (ski_scope) [in :ski_scope:'〚'_x_'〛']
〚 _ 〛 (ski_scope) [in :ski_scope:'〚'_x_'〛']
Λ _ (ski_scope) [in :ski_scope:'Λ'_x]
_ • _ (ski_scope) [in :ski_scope:x_'•'_x]
_ • _ (ski_scope) [in :ski_scope:x_'•'_x]
_ ⇒ _ (ty_scope) [in :ty_scope:x_'⇒'_x]
_ ⇒ _ (ty_scope) [in :ty_scope:x_'⇒'_x]
_ ⇒ _ (ty_scope) [in :ty_scope:x_'⇒'_x]
_ ⇒ _ (ty_scope) [in :ty_scope:x_'⇒'_x]
2 (ty_scope) [in :ty_scope:'2']
2 (ty_scope) [in :ty_scope:'2']
2 (ty_scope) [in :ty_scope:'2']
2 (ty_scope) [in :ty_scope:'2']
_ ↓ [in ::x_'↓']
_ ↓ [in ::x_'↓']
_ ✧ _ [in ::x_'✧'_x]
_ • _ [in ::x_'•'_x]
_ ⋆ _ [in ::x_'⋆'_x]
_ · _ [in ::x_'·'_x]
_ ⇓ _ [in ::x_'⇓'_x]
_ ⇓ _ [in ::x_'⇓'_x]
_ ⇀ _ [in ::x_'⇀'_x]
_ ⇋ _ [in ::x_'⇋'_x]
_ ♯ _ [in ::x_'♯'_x]
_ ✦ _ [in ::x_'✦'_x]
fresh [ _ , .. , _ ] [in ::'fresh'_'['_x_','_'..'_','_x_']']
Id [in ::'Id']
Id ( _ ) [in ::'Id'_'('_x_')']
‖ _ ‖ [in ::'‖'_x_'‖']
∂PLT [in ::'∂PLT']
[in ::'∅']
Ψ⁻¹ [in ::'Ψ⁻¹']
ν _ , _ [in ::'ν'_x_','_x]



Constructor Index

A

acong_fix [in acong_fix]
acong_app [in acong_app]
acong_app [in acong_app]
acong_if [in acong_if]
acong_if [in acong_if]
acong_lam [in acong_lam]
acong_lam [in acong_lam]
acong_bool [in acong_bool]
acong_bool [in acong_bool]
acong_var [in acong_var]
acong_var [in acong_var]
Adjunction.Adjunction [in Adjunction]
Alg.Alg [in Alg]
Alg.Alg_hom [in Alg_hom]
Alg.Initial_alg [in Initial_alg]


B

Bicategory.Bicategory [in Bicategory]
Bicategory.Mixin [in Mixin]
bind [in bind]


C

CartesianClosed.Axioms [in Axioms]
CartesianClosed.CartesianClosed [in CartesianClosed]
CartesianClosed.Mixin [in Mixin]
Cartesian.Axioms [in Axioms]
Cartesian.Cartesian [in Cartesian]
Cartesian.Mixin [in Mixin]
Category.Axioms [in Axioms]
Category.Category [in Category]
Cocartesian.Axioms [in Axioms]
Cocartesian.Cocartesian [in Cocartesian]
Cocartesian.Mixin [in Mixin]
Cocone [in Cocone]
Color [in Color]
Comp.Mixin [in Mixin]
Comp.Pack [in Pack]
Concrete [in Concrete]
Cone.Cone [in Cone]
Cone.Cone_hom [in Cone_hom]
Convex [in Convex]
CPO.Hom [in Hom]
CPO.Mixin [in Mixin]
CPO.Pack [in Pack]
cxt_fix [in cxt_fix]
cxt_if [in cxt_if]
cxt_if [in cxt_if]
cxt_appl [in cxt_appl]
cxt_appl [in cxt_appl]
cxt_appl [in cxt_appl]
cxt_appl [in cxt_appl]
cxt_appr [in cxt_appr]
cxt_appr [in cxt_appr]
cxt_appr [in cxt_appr]
cxt_appr [in cxt_appr]
cxt_lam [in cxt_lam]
cxt_lam [in cxt_lam]
cxt_top [in cxt_top]
cxt_top [in cxt_top]
cxt_top [in cxt_top]
cxt_top [in cxt_top]


D

DirectedColimit [in DirectedColimit]
DirPreord [in DirPreord]
DirSys [in DirSys]
Distributive.Distributive [in Distributive]


E

eapp [in eapp]
eapp [in eapp]
eapp1 [in eapp1]
eapp1 [in eapp1]
eapp2 [in eapp2]
eapp2 [in eapp2]
ebool [in ebool]
ebool [in ebool]
ebool [in ebool]
ebool [in ebool]
EffectiveOrder [in EffectiveOrder]
efix [in efix]
eI [in eI]
eI [in eI]
eIF [in eIF]
eIF [in eIF]
eif [in eif]
eif [in eif]
einh [in einh]
eK [in eK]
eK [in eK]
elam [in elam]
elam [in elam]
Embedding [in Embedding]
enumtype.Enumtype [in Enumtype]
Epimorphism [in Epimorphism]
EpPair [in EpPair]
EqDec [in EqDec]
Eq.Mixin [in Mixin]
Eq.Pack [in Pack]
eS [in eS]
eS [in eS]
eY [in eY]


F

finprod.internals.codom_avoid [in codom_avoid]
finprod.internals.codom_elem [in codom_elem]
finprod.TermModel [in TermModel]
fintype.Fintype [in Fintype]
Functor.Functor [in Functor]


G

Groupoid.Axioms [in Axioms]
Groupoid.Groupoid [in Groupoid]
Groupoid.Mixin [in Mixin]


I

inert_IF1 [in inert_IF1]
inert_IF2 [in inert_IF2]
inert_S1 [in inert_S1]
inert_S2 [in inert_S2]
inert_K [in inert_K]
inert_Y [in inert_Y]
Initialized.Initialized [in Initialized]
Initialized.Mixin [in Mixin]
IsEP [in IsEP]
Isomorphism [in Isomorphism]


L

LimSet [in LimSet]
Lower [in Lower]


M

Monomorphism [in Monomorphism]


N

NomColim [in NomColim]
NomExp [in NomExp]
Nominal.Hom [in Hom]
Nominal.Mixin [in Mixin]
Nominal.Ob [in Ob]
NT.NT [in NT]


O

OrdDec [in OrdDec]


P

Perm.Perm [in Perm]
PlotkinOrder [in PlotkinOrder]
PLT.Class [in Class]
PLT.Hom [in Hom]
PLT.Ob [in Ob]
PolynomialCategory.PolynomialCategory [in PolynomialCategory]
powerdom.PdomElem [in PdomElem]
Preord.Hom [in Hom]
Preord.Mixin [in Mixin]
Preord.Pack [in Pack]
PROD.Hom [in Hom]
PROD.Ob [in Ob]
Pseudofunctor.Pseudofunctor [in Pseudofunctor]
Pullback.Pullback [in Pullback]
Pullback.Square [in Square]


R

redex_I [in redex_I]
redex_I [in redex_I]
redex_K [in redex_K]
redex_K [in redex_K]
redex_S [in redex_S]
redex_S [in redex_S]
redex_Y [in redex_Y]
redex_IFtrue [in redex_IFtrue]
redex_IFtrue [in redex_IFtrue]
redex_IFfalse [in redex_IFfalse]
redex_IFfalse [in redex_IFfalse]


S

Semidec [in Semidec]
Setdec [in Setdec]
SET.Hom [in Hom]
set.Mixin [in Mixin]
SET.Ob [in Ob]
set.Theory [in Theory]
smash_some [in smash_some]
smash_none [in smash_none]
Support.Supported [in Supported]


T

tapp [in tapp]
tapp [in tapp]
tapp [in tapp]
tapp [in tapp]
tbool [in tbool]
tbool [in tbool]
tbool [in tbool]
tbool [in tbool]
Terminated.Mixin [in Mixin]
Terminated.Terminated [in Terminated]
tfix [in tfix]
tI [in tI]
tI [in tI]
tif [in tif]
tif [in tif]
tIF [in tIF]
tIF [in tIF]
tK [in tK]
tK [in tK]
tlam [in tlam]
tlam [in tlam]
tS [in tS]
tS [in tS]
tvar [in tvar]
tvar [in tvar]
tY [in tY]
ty_arrow [in ty_arrow]
ty_arrow [in ty_arrow]
ty_arrow [in ty_arrow]
ty_arrow [in ty_arrow]
ty_bool [in ty_bool]
ty_bool [in ty_bool]
ty_bool [in ty_bool]
ty_bool [in ty_bool]


U

Upper [in Upper]


V

vcong_here [in vcong_here]
vcong_here [in vcong_here]
vcong_there [in vcong_there]
vcong_there [in vcong_there]



Abbreviation Index

A

adjunction [in adjunction]
Adjunction [in Adjunction]
Alg [in Alg]
alg [in alg]
ALG [in ALG]
apply [in apply]
apply [in apply]


B

Bicategory [in Bicategory]
bicategory [in bicategory]
bind [in bind]
bind [in bind]


C

Cartesian [in Cartesian]
cartesian [in cartesian]
CartesianClosed [in CartesianClosed]
cartesian_closed [in cartesian_closed]
castty [in castty]
castty [in castty]
category [in category]
Category [in Category]
cl_finset [in cl_finset]
cl_eset [in cl_eset]
cocartesian [in cocartesian]
Cocartesian [in Cocartesian]
cpo [in cpo]
CPO [in CPO]
cppo [in cppo]
cxt [in cxt]
cxt [in cxt]


D

dcpo [in dcpo]
dirset [in dirset]
Distributive [in Distributive]
distributive [in distributive]
distrib_law [in distrib_law]


E

either [in either]
Enumtype [in Enumtype]
enumtype [in enumtype]
env [in env]
env [in env]
eset [in eset]


F

finprod.castty [in castty]
finprod.cxt [in cxt]
finset [in finset]
fintype [in fintype]
Fintype [in Fintype]
functor [in functor]
Functor [in Functor]


G

groupoid [in groupoid]
Groupoid [in Groupoid]


H

hom [in hom]
hom [in hom]
homl [in homl]
homr [in homr]
hom2 [in hom2]


I

inenv [in inenv]
inenv [in inenv]
Initialized [in Initialized]
initialized [in initialized]
initiate [in initiate]


L

L [in L]
Le [in Le]


N

nominal [in nominal]
NOMINAL [in NOMINAL]
NT [in NT]
nt [in nt]


O

ob [in ob]
ob [in ob]
obl [in obl]
obr [in obr]


P

perm [in perm]
PERM [in PERM]
PLT [in PLT]
PLT [in PLT]
PolynomialCategory [in PolynomialCategory]
polynomial_category [in polynomial_category]
powerdomain [in powerdomain]
preord [in preord]
PROD [in PROD]
proj [in proj]
proj [in proj]
pseudofunctor [in pseudofunctor]
Pseudofunctor [in Pseudofunctor]
Pullback [in Pullback]
pullback [in pullback]


S

set [in set]
subst [in subst]
subst [in subst]
Supported [in Supported]
supported [in supported]


T

Terminated [in Terminated]
terminated [in terminated]
term_subst [in term_subst]
term_subst [in term_subst]
term_wk [in term_wk]
term_wk [in term_wk]
TYPE [in TYPE]


U

U [in U]
Ue [in Ue]


other

Ψ [in Ψ]
γ [in γ]
ε [in ε]
η [in η]



Inductive Index

A

alpha_cong [in alpha_cong]
alpha_cong [in alpha_cong]


B

binding_ty [in binding_ty]


C

context [in context]
context [in context]
context [in context]
context [in context]


E

einhabited [in einhabited]
eval [in eval]
eval [in eval]
eval [in eval]
eval [in eval]


F

finprod.internals.finprod_codom [in finprod_codom]


I

inert [in inert]


P

pdom_sort [in pdom_sort]


R

redex [in redex]
redex [in redex]


S

smash_prod_spec [in smash_prod_spec]


T

term [in term]
term [in term]
term [in term]
term [in term]
ty [in ty]
ty [in ty]
ty [in ty]
ty [in ty]


V

var_cong [in var_cong]
var_cong [in var_cong]



Definition Index

A

adjoin_char [in adjoin_char]
adj_counit_inv_hom [in adj_counit_inv_hom]
adj_unit [in adj_unit]
adj_unit_hom [in adj_unit_hom]
adj_unit_rel [in adj_unit_rel]
adj_counit_hom [in adj_counit_hom]
adj_counit [in adj_counit]
adj_counit_rel [in adj_counit_rel]
admissible [in admissible]
AG_cocone' [in AG_cocone']
AG_cocone [in AG_cocone]
Alg.ALG [in ALG]
Alg.compose [in compose]
Alg.forget [in forget]
Alg.free [in free]
Alg.ident [in ident]
Alg.lift_alg [in lift_alg]
Alg.out [in out]
allowable_chars [in allowable_chars]
all_finset_semidec [in all_finset_semidec]
all_finset_setdec [in all_finset_setdec]
all_jrels [in all_jrels]
antistrict [in antistrict]
apply_acceptable [in apply_acceptable]
apply_rel [in apply_rel]
atom [in atom]
atom_dec [in atom_dec]
atom_supp [in atom_supp]


B

Bicategory.HOM [in HOM]
BICAT_EQ [in BICAT_EQ]
bicat_assoc [in bicat_assoc]
bicat_unit1 [in bicat_unit1]
bicat_unit2 [in bicat_unit2]
BICAT_COMP [in BICAT_COMP]
bilimit [in bilimit]
bilimit_construction [in bilimit_construction]
bilimit_cocone [in bilimit_cocone]
binding [in binding]
bindingF [in bindingF]
binding_equiv [in binding_equiv]
binding_support [in binding_support]
binding_fmap_defn [in binding_fmap_defn]
binding_fmap [in binding_fmap]
binding_eq [in binding_eq]
binding_nominal_mixin [in binding_nominal_mixin]
binding_eq_mixin [in binding_eq_mixin]
binding_papp [in binding_papp]
boolset [in boolset]


C

CartesianClosed.apply_op [in apply_op]
CartesianClosed.cartesian [in cartesian]
CartesianClosed.cartesian' [in cartesian']
CartesianClosed.category [in category]
CartesianClosed.comp [in comp]
CartesianClosed.comp' [in comp']
CartesianClosed.curry_op [in curry_op]
CartesianClosed.eq [in eq]
CartesianClosed.eq' [in eq']
CartesianClosed.exp_op [in exp_op]
CartesianClosed.terminated [in terminated]
Cartesian.category [in category]
Cartesian.comp [in comp]
Cartesian.comp' [in comp']
Cartesian.eq [in eq]
Cartesian.eq' [in eq']
Cartesian.pairing_op [in pairing_op]
Cartesian.product_op [in product_op]
Cartesian.proj1_op [in proj1_op]
Cartesian.proj2_op [in proj2_op]
Cartesian.terminated [in terminated]
cast [in cast]
cast_rel [in cast_rel]
CAT [in CAT]
cata_alg_hom [in cata_alg_hom]
cata_hom' [in cata_hom']
cata_hom [in cata_hom]
Category.cat_EQ [in cat_EQ]
Category.cat_COMP [in cat_COMP]
cat_bicategory_mixin [in cat_bicategory_mixin]
CAT_EQ [in CAT_EQ]
CAT_COMP [in CAT_COMP]
cat_assoc [in cat_assoc]
cat_respects [in cat_respects]
cat_ident1 [in cat_ident1]
cat_ident2 [in cat_ident2]
CAT_axioms [in CAT_axioms]
cbnLamF [in cbnLamF]
cbvLamF [in cbvLamF]
chain_sup [in chain_sup]
char_ord [in char_ord]
choose [in choose]
choose_finset [in choose_finset]
choose' [in choose']
cl_eset_theory [in cl_eset_theory]
cl_finset_theory [in cl_finset_theory]
Cocartesian.category [in category]
Cocartesian.comp [in comp]
Cocartesian.comp' [in comp']
Cocartesian.either_op [in either_op]
Cocartesian.eq [in eq]
Cocartesian.eq' [in eq']
Cocartesian.initalized [in initalized]
Cocartesian.inl_op [in inl_op]
Cocartesian.inr_op [in inr_op]
Cocartesian.sum_op [in sum_op]
cocone_fstF [in cocone_fstF]
cocone_minus1 [in cocone_minus1]
cocone_plus1 [in cocone_plus1]
cocone_plus1 [in cocone_plus1]
cocone_app [in cocone_app]
cocone_sndF [in cocone_sndF]
colift [in colift]
colored_sets.forget_color [in forget_color]
colored_sets.mixin [in mixin]
colored_sets.cset [in cset]
colored_sets.cmember [in cmember]
colored_sets.csingle [in csingle]
colored_sets.cunion [in cunion]
colored_sets.cimage [in cimage]
color_and [in color_and]
compose_rel [in compose_rel]
comp_horiz [in comp_horiz]
comp_op [in comp_op]
concat [in concat]
concat [in concat]
CONCRETE_EQ [in CONCRETE_EQ]
Cone.CONE [in CONE]
Cone.cone_ident [in cone_ident]
Cone.cone_compose [in cone_compose]
Cone.diagram [in diagram]
const [in const]
continuous [in continuous]
continuous_functor [in continuous_functor]
CPO.app [in app]
CPO.app_to [in app_to]
CPO.build_hom [in build_hom]
CPO.comp [in comp]
CPO.compose [in compose]
CPO.comp_mixin [in comp_mixin]
CPO.CPO [in CPO]
CPO.cpo_eq_mixin [in cpo_eq_mixin]
CPO.cpo_eq [in cpo_eq]
CPO.hom_ord [in hom_ord]
CPO.hom_ord_mixin [in hom_ord_mixin]
CPO.hom_order [in hom_order]
CPO.hom_sup [in hom_sup]
CPO.hom_cpo [in hom_cpo]
CPO.hom_mixin [in hom_mixin]
CPO.ident [in ident]
CPO.ord_hom [in ord_hom]
CPO.pair [in pair]
CPO.pi1 [in pi1]
CPO.pi2 [in pi2]
CPO.prod_mixin [in prod_mixin]
CPO.prod_sup [in prod_sup]
CPO.prod_cpo [in prod_cpo]
CPO.sup_op [in sup_op]
cppo_bot [in cppo_bot]
cset_theory [in cset_theory]
curry_rel [in curry_rel]
curry_acceptable [in curry_acceptable]
cxt_eq [in cxt_eq]
cxt_eq [in cxt_eq]
cxt_eq [in cxt_eq]
cxt_eq [in cxt_eq]


D

decompose_is_colimit [in decompose_is_colimit]
decompose_univ [in decompose_univ]
decompose_univ_func [in decompose_univ_func]
dec_semidec [in dec_semidec]
deflate [in deflate]
deflate' [in deflate']
denote [in denote]
denote [in denote]
denote [in denote]
denote [in denote]
directed [in directed]
directed_cl [in directed_cl]
directed_hf_cl [in directed_hf_cl]
directed_rel [in directed_rel]
dir_sys_app [in dir_sys_app]
disc [in disc]
disc_cases [in disc_cases]
disc_elem [in disc_elem]
Distributive.cartesian [in cartesian]
Distributive.cartesian' [in cartesian']
Distributive.category [in category]
Distributive.cocartesian [in cocartesian]
Distributive.cocartesian' [in cocartesian']
Distributive.comp [in comp]
Distributive.comp' [in comp']
Distributive.distrib_law_op [in distrib_law_op]
Distributive.eq [in eq]
Distributive.eq' [in eq']
Distributive.initialized [in initialized]
Distributive.terminated [in terminated]
dom [in dom]
dom [in dom]


E

effective_Nord [in effective_Nord]
effective_empty [in effective_empty]
effective_sum [in effective_sum]
effective_unit [in effective_unit]
effective_prod [in effective_prod]
effective_lift [in effective_lift]
eff_to_ord_dec [in eff_to_ord_dec]
eimage' [in eimage']
elem [in elem]
elist [in elist]
EMBED [in EMBED]
embedForget [in embedForget]
embed_comp [in embed_comp]
embed_ord [in embed_ord]
embed_compose [in embed_compose]
embed_eq_mixin [in embed_eq_mixin]
embed_comp_mixin [in embed_comp_mixin]
embed_hom [in embed_hom]
embed_order_mixin [in embed_order_mixin]
embed_func [in embed_func]
embed_rel [in embed_rel]
embed_order [in embed_order]
embed_ep_pair [in embed_ep_pair]
embed_ident [in embed_ident]
embed_image [in embed_image]
embed_initiate [in embed_initiate]
empty [in empty]
emptypo [in emptypo]
empty_plotkin [in empty_plotkin]
empty_dir [in empty_dir]
enumbool [in enumbool]
enumtype.enumtype_plotkin [in enumtype_plotkin]
enumtype.enumtype_effective [in enumtype_effective]
enumtype.eq_mixin [in eq_mixin]
enumtype.ord [in ord]
enumtype.preord_mixin [in preord_mixin]
enumtype.setoid [in setoid]
enum_lift [in enum_lift]
env_input.A [in A]
env_input.A [in A]
env_input.F [in F]
env_input.F [in F]
env_input.Adec [in Adec]
env_input.Adec [in Adec]
epi_comp_mixin [in epi_comp_mixin]
EPI_COMP [in EPI_COMP]
epi_compose [in epi_compose]
epi_eq [in epi_eq]
epi_id [in epi_id]
EPI_EQ [in EPI_EQ]
epi_cat_axioms [in epi_cat_axioms]
EPI_CAT [in EPI_CAT]
eprod [in eprod]
ep_pair_eq [in ep_pair_eq]
ep_embed [in ep_embed]
ep_id [in ep_id]
ep_pair_comp_mixin [in ep_pair_comp_mixin]
ep_embedding [in ep_embedding]
ep_pair_eq_mixin [in ep_pair_eq_mixin]
ep_set [in ep_set]
ep_pair_comp [in ep_pair_comp]
ep_compose [in ep_compose]
eq_op [in eq_op]
erel [in erel]
erel_inv_image [in erel_inv_image]
erel_image [in erel_image]
eset_theory [in eset_theory]
eset.eimage [in eimage]
eset.emember [in emember]
eset.eset [in eset]
eset.esingle [in esingle]
eset.eunion [in eunion]
esubset [in esubset]
esubset_dec [in esubset_dec]
esum [in esum]
expF [in expF]
exp_papp [in exp_papp]
exp_fmap_func [in exp_fmap_func]
exp_fmap [in exp_fmap]
ex_finset_semidec [in ex_finset_semidec]
ex_finset_setdec [in ex_finset_setdec]


F

fconst [in fconst]
finbool [in finbool]
find_inhabitant' [in find_inhabitant']
find_inhabitant [in find_inhabitant]
finprod [in finprod]
finprod.bind [in bind]
FINPROD.bind [in bind]
finprod.empty_cxt_inh [in empty_cxt_inh]
finprod.env [in env]
finprod.env_incl [in env_incl]
finprod.env_supp [in env_supp]
finprod.env_supported [in env_supported]
finprod.extend_map [in extend_map]
finprod.finprod [in finprod]
finprod.inenv [in inenv]
finprod.internals.codom [in codom]
finprod.internals.codom_eff [in codom_eff]
finprod.internals.codom_enum [in codom_enum]
finprod.internals.codom_out [in codom_out]
finprod.internals.codom_in' [in codom_in']
finprod.internals.codom_out' [in codom_out']
finprod.internals.codom_plotkin [in codom_plotkin]
finprod.internals.empty_cxt_rel [in empty_cxt_rel]
finprod.internals.empty_ctx [in empty_ctx]
finprod.internals.enum_finprod [in enum_finprod]
finprod.internals.finprod [in finprod]
finprod.internals.finprod_codom_ord_mixin [in finprod_codom_ord_mixin]
finprod.internals.finprod_codom_ord [in finprod_codom_ord]
finprod.internals.finprod_dec [in finprod_dec]
finprod.internals.finprod_plotkin [in finprod_plotkin]
finprod.internals.finprod_ord_mixin [in finprod_ord_mixin]
finprod.internals.finprod_univ_rel [in finprod_univ_rel]
finprod.internals.finprod_elem [in finprod_elem]
finprod.internals.finprod_codom_weaken [in finprod_codom_weaken]
finprod.internals.finprod_ord [in finprod_ord]
finprod.internals.finprod_effective [in finprod_effective]
finprod.internals.finprod_univ [in finprod_univ]
finprod.internals.f_cons [in f_cons]
finprod.internals.f_hd' [in f_hd']
finprod.internals.f_hd [in f_hd]
finprod.internals.f_cons' [in f_cons']
finprod.internals.f_tl [in f_tl]
finprod.internals.f_tl' [in f_tl']
finprod.internals.ord [in ord]
finprod.internals.ord_weaken [in ord_weaken]
finprod.internals.proj [in proj]
finprod.internals.proj_rel [in proj_rel]
finprod.lookup [in lookup]
FINPROD.lookup [in lookup]
finprod.mk_finprod [in mk_finprod]
finprod.newestvar [in newestvar]
finprod.proj [in proj]
finprod.shift_vars [in shift_vars]
finprod.subst [in subst]
finprod.subst_denote [in subst_denote]
finprod.tm_wk [in tm_wk]
finprod.tm_subst [in tm_subst]
finprod.ty [in ty]
FINPROD.ty [in ty]
finprod.unbind [in unbind]
FINPROD.unbind [in unbind]
finprod.varmap [in varmap]
finprod.varmap_denote [in varmap_denote]
finprod.varmap_compose [in varmap_compose]
finprod.weaken_map [in weaken_map]
finprod.weaken_denote [in weaken_denote]
finset_theory [in finset_theory]
finset_remove [in finset_remove]
finset_dec [in finset_dec]
finset.fimage [in fimage]
finset.fmember [in fmember]
finset.fset [in fset]
finset.fsingle [in fsingle]
finset.funion [in funion]
finset.mixin [in mixin]
finsubset [in finsubset]
finsubsets [in finsubsets]
finsum [in finsum]
fintype.eq_mixin [in eq_mixin]
fintype.fintype_effective [in fintype_effective]
fintype.fintype_plotkin [in fintype_plotkin]
fintype.fintype_has_normals [in fintype_has_normals]
fintype.ord [in ord]
fintype.preord_mixin [in preord_mixin]
fintype.setoid [in setoid]
fin_intersect [in fin_intersect]
fin_list_intersect [in fin_list_intersect]
fixes [in fixes]
fixes_step [in fixes_step]
fixes_step' [in fixes_step']
fixpoint [in fixpoint]
fixpoint [in fixpoint]
fixpoint [in fixpoint]
fixpoint_alt_iso [in fixpoint_alt_iso]
fixpoint_iso [in fixpoint_iso]
fixpoint_iso [in fixpoint_iso]
fixpoint_iso [in fixpoint_iso]
fixpoint_alg [in fixpoint_alg]
fixpoint_alt [in fixpoint_alt]
fixpoint_embed [in fixpoint_embed]
fixpoint_initial [in fixpoint_initial]
fixpoint_initial [in fixpoint_initial]
fixpoint_initial [in fixpoint_initial]
fixpoint_alt_in [in fixpoint_alt_in]
fixpoint_alt_out [in fixpoint_alt_out]
flat [in flat]
flat_cases [in flat_cases]
flat_cases' [in flat_cases']
flat_cases_rel [in flat_cases_rel]
flat_elem' [in flat_elem']
flat_elem [in flat_elem]
forgetEMBED [in forgetEMBED]
forgetEMBED_map [in forgetEMBED_map]
forgetPLT [in forgetPLT]
forgetPLT_ob [in forgetPLT_ob]
forgetPLT_map [in forgetPLT_map]
fresh_atom [in fresh_atom]
fresh_idents [in fresh_idents]
fstF [in fstF]
fstF_cocone [in fstF_cocone]
fstF_univ [in fstF_univ]
FUNC [in FUNC]
FuncComp [in FuncComp]
FunctorCompose [in FunctorCompose]
FunctorIdent [in FunctorIdent]


G

greatest_lower_bound [in greatest_lower_bound]
Groupoid.category [in category]
Groupoid.comp [in comp]
Groupoid.comp' [in comp']
Groupoid.eq [in eq]
Groupoid.eq' [in eq']
Groupoid.inv_op [in inv_op]


H

has_normals [in has_normals]
HOM [in HOM]
hom_eq [in hom_eq]
hom_order [in hom_order]
hom1_ident [in hom1_ident]
hom1_compose [in hom1_compose]


I

idents_wf [in idents_wf]
idents_out [in idents_out]
idents_step [in idents_step]
idents_inv [in idents_inv]
idents_set [in idents_set]
ident_op [in ident_op]
ident_rel [in ident_rel]
image [in image]
incl [in incl]
inflate [in inflate]
inflate' [in inflate']
inh [in inh]
inhabited [in inhabited]
initialized_mixin [in initialized_mixin]
initialized_nominal [in initialized_nominal]
Initialized.category [in category]
Initialized.comp [in comp]
Initialized.eq [in eq]
Initialized.eq' [in eq']
Initialized.initiate_op [in initiate_op]
Initialized.initium_op [in initium_op]
initiate [in initiate]
initius [in initius]
initius_mixin [in initius_mixin]
initius_eq_mixin [in initius_eq_mixin]
injectA [in injectA]
insert_index [in insert_index]
insert_index [in insert_index]
inset_decset [in inset_decset]
intersection [in intersection]
iota1_rel [in iota1_rel]
iota2_rel [in iota2_rel]
Iset [in Iset]
iso_groupoid_mixin [in iso_groupoid_mixin]
iso_cat_axioms [in iso_cat_axioms]
iso_hom'' [in iso_hom'']
iso_comp_mixin [in iso_comp_mixin]
iso_eq [in iso_eq]
iso_id [in iso_id]
iso_hom' [in iso_hom']
iso_compose [in iso_compose]
iso_inverse [in iso_inverse]
ISO_GROUPOID [in ISO_GROUPOID]
is_joinable_relation [in is_joinable_relation]
is_mub_complete [in is_mub_complete]
iterF [in iterF]
iterF [in iterF]
iter_chain [in iter_chain]
iter_hom [in iter_hom]
iter_hom [in iter_hom]
iter_chain_set [in iter_chain_set]


J

joinable_rel_ord_mixin [in joinable_rel_ord_mixin]
joinable_relation [in joinable_relation]
joinable_rel_order [in joinable_rel_order]
joinable_rel_effective [in joinable_rel_effective]
joinable_rel_ord [in joinable_rel_ord]
joinable_rel_plt [in joinable_rel_plt]


K

kleene_chain [in kleene_chain]
kleene_chain_alt [in kleene_chain_alt]


L

lamModelCBN [in lamModelCBN]
lamModelCBV [in lamModelCBV]
lam_termmodel [in lam_termmodel]
lam_termmodel [in lam_termmodel]
least_upper_bound [in least_upper_bound]
left_whisker [in left_whisker]
left_finset [in left_finset]
lfp [in lfp]
lib_eq [in lib_eq]
lift [in lift]
lift [in lift]
liftEMBED [in liftEMBED]
liftEMBED_map [in liftEMBED_map]
liftF [in liftF]
liftPPLT [in liftPPLT]
liftPPLT_ob [in liftPPLT_ob]
liftPPLT_rel [in liftPPLT_rel]
liftPPLT_map [in liftPPLT_map]
liftup [in liftup]
lift_unit [in lift_unit]
lift_map [in lift_map]
lift_unit' [in lift_unit']
lift_mub_closure [in lift_mub_closure]
lift_plotkin [in lift_plotkin]
lift_mixin [in lift_mixin]
lift_ord [in lift_ord]
lift_prod [in lift_prod]
lift_prod' [in lift_prod']
limord [in limord]
limord_univ [in limord_univ]
limord_effective [in limord_effective]
limord_mixin [in limord_mixin]
limord_plotkin [in limord_plotkin]
limset_enum [in limset_enum]
limset_spoke [in limset_spoke]
limset_order [in limset_order]
list_finsubsets [in list_finsubsets]
lower_bound [in lower_bound]
lower_set [in lower_set]
LR [in LR]
LR [in LR]
LR [in LR]
LR [in LR]
lrapp [in lrapp]
lrapp [in lrapp]
lrhyps [in lrhyps]
lrhyps [in lrhyps]
lrsem [in lrsem]
lrsem [in lrsem]
lrsemapp [in lrsemapp]
lrsemapp [in lrsemapp]
lrsyn [in lrsyn]
lrsyn [in lrsyn]
lrtys [in lrtys]
lrtys [in lrtys]


M

map_rel [in map_rel]
map_indexes [in map_indexes]
maximal_lower_bound [in maximal_lower_bound]
max_len [in max_len]
maybe [in maybe]
minimal_upper_bound [in minimal_upper_bound]
mkrel [in mkrel]
mk_pair [in mk_pair]
mk_disc_cases_rel [in mk_disc_cases_rel]
mono_cat_axioms [in mono_cat_axioms]
MONO_COMP [in MONO_COMP]
mono_compose [in mono_compose]
mono_comp_mixin [in mono_comp_mixin]
MONO_EQ [in MONO_EQ]
MONO_CAT [in MONO_CAT]
mono_eq [in mono_eq]
mono_id [in mono_id]
mub_closed [in mub_closed]


N

nat_dirord [in nat_dirord]
nat_ord [in nat_ord]
nat_eff [in nat_eff]
Ndisc_ord [in Ndisc_ord]
ne_finsubsets [in ne_finsubsets]
Nominal.comp [in comp]
Nominal.compose [in compose]
Nominal.comp_mixin [in comp_mixin]
Nominal.eq [in eq]
Nominal.hom_eq [in hom_eq]
Nominal.hom_eq_mixin [in hom_eq_mixin]
Nominal.ident [in ident]
Nominal.NOMINAL [in NOMINAL]
Nominal.nom_support [in nom_support]
Nominal.ob_eq [in ob_eq]
Nominal.papp_op [in papp_op]
Nominal.support_op [in support_op]
nom_sum_papp [in nom_sum_papp]
nom_terminated_mixin [in nom_terminated_mixin]
nom_terminated [in nom_terminated]
nom_has_colimits [in nom_has_colimits]
nom_colimit_papp [in nom_colimit_papp]
nom_sum [in nom_sum]
nom_cartesian_mixin [in nom_cartesian_mixin]
nom_ccc [in nom_ccc]
nom_colimit_cocone [in nom_colimit_cocone]
nom_sum_support [in nom_sum_support]
nom_prod_eq_mixin [in nom_prod_eq_mixin]
nom_terminus [in nom_terminus]
nom_colimit_eq_mixin [in nom_colimit_eq_mixin]
nom_colimit_equiv [in nom_colimit_equiv]
nom_apply [in nom_apply]
nom_colimit_univ_defn [in nom_colimit_univ_defn]
nom_prod [in nom_prod]
nom_terminate [in nom_terminate]
nom_ccc_mixin [in nom_ccc_mixin]
nom_colimit_spoke [in nom_colimit_spoke]
nom_cartesian [in nom_cartesian]
nom_exp_eq [in nom_exp_eq]
nom_pairing [in nom_pairing]
nom_sum_eq_mixin [in nom_sum_eq_mixin]
nom_terminus_mixin [in nom_terminus_mixin]
nom_colimit_univ [in nom_colimit_univ]
nom_sum_equiv [in nom_sum_equiv]
nom_exp [in nom_exp]
nom_curry [in nom_curry]
nom_colimit_mixin [in nom_colimit_mixin]
nom_pi1 [in nom_pi1]
nom_pi2 [in nom_pi2]
nom_terminus_eq_mixin [in nom_terminus_eq_mixin]
nom_prod_mixin [in nom_prod_mixin]
nom_exp_eq_mixin [in nom_exp_eq_mixin]
nom_colimit [in nom_colimit]
nom_exp_mixin [in nom_exp_mixin]
nom_sum_mixin [in nom_sum_mixin]
nonbottom [in nonbottom]
normal_set [in normal_set]
norm_plt [in norm_plt]
norm_closure [in norm_closure]
NTCAT [in NTCAT]
NTComp [in NTComp]
NTCompHoriz [in NTCompHoriz]
NTEQ [in NTEQ]
nt_assoc [in nt_assoc]
nt_unit1 [in nt_unit1]
nt_unit2 [in nt_unit2]
NT.compose [in compose]
NT.ident [in ident]
NT.NTComp_mixin [in NTComp_mixin]
NT.NTEQ_mixin [in NTEQ_mixin]
NT.pushnt [in pushnt]
NT.stacknt [in stacknt]


O

ONE [in ONE]


P

pairF [in pairF]
pairing [in pairing]
pair_rel [in pair_rel]
pair_map [in pair_map]
pair_right [in pair_right]
pair_left [in pair_left]
pair_rel' [in pair_rel']
pdom_fmap [in pdom_fmap]
pdom_map [in pdom_map]
perms [in perms]
Perm.comp [in comp]
Perm.compose [in compose]
Perm.comp_mixin [in comp_mixin]
Perm.eq [in eq]
Perm.eq_mixin [in eq_mixin]
Perm.groupoid [in groupoid]
Perm.groupoid_mixin [in groupoid_mixin]
Perm.ident [in ident]
Perm.inv [in inv]
Perm.PERM [in PERM]
Perm.perm_support [in perm_support]
Perm.swap [in swap]
pi1 [in pi1]
pi1_rel [in pi1_rel]
pi2 [in pi2]
pi2_rel [in pi2_rel]
plotkin_sum [in plotkin_sum]
plotkin_prod [in plotkin_prod]
plotkin_forget [in plotkin_forget]
plt_hom_adj [in plt_hom_adj]
plt_const_rel [in plt_const_rel]
plt_hom_adj' [in plt_hom_adj']
plt_const [in plt_const]
PLT_adjoint [in PLT_adjoint]
PLT_EP [in PLT_EP]
PLT.app [in app]
PLT.cartesian [in cartesian]
PLT.cartesian_mixin [in cartesian_mixin]
PLT.cartesian_closed_mixin [in cartesian_closed_mixin]
PLT.cartesian_closed [in cartesian_closed]
PLT.cocartesian [in cocartesian]
PLT.cocartesian_mixin [in cocartesian_mixin]
PLT.comp [in comp]
PLT.compose [in compose]
PLT.comp_mixin [in comp_mixin]
PLT.curry [in curry]
PLT.dec [in dec]
PLT.effective [in effective]
PLT.empty [in empty]
PLT.exp [in exp]
PLT.homset_cpo_mixin [in homset_cpo_mixin]
PLT.homset_sup [in homset_sup]
PLT.homset_cpo [in homset_cpo]
PLT.hom_eq [in hom_eq]
PLT.hom_ord [in hom_ord]
PLT.hom_ord_mixin [in hom_ord_mixin]
PLT.hom_eq_mixin [in hom_eq_mixin]
PLT.hom_rel' [in hom_rel']
PLT.ident [in ident]
PLT.initialized_mixin [in initialized_mixin]
PLT.initiate [in initiate]
PLT.iota1 [in iota1]
PLT.iota2 [in iota2]
PLT.ord [in ord]
PLT.pair [in pair]
PLT.pair_map [in pair_map]
PLT.pair_map' [in pair_map']
PLT.pi1 [in pi1]
PLT.pi2 [in pi2]
PLT.plotkin [in plotkin]
PLT.PLT [in PLT]
PLT.prod [in prod]
PLT.sum [in sum]
PLT.sum_cases [in sum_cases]
PLT.terminate [in terminate]
PLT.terminated [in terminated]
PLT.terminated_mixin [in terminated_mixin]
PLT.unit [in unit]
plug [in plug]
plug [in plug]
plug [in plug]
plug [in plug]
PolynomialCategory.cartesian [in cartesian]
PolynomialCategory.cartesian_closed [in cartesian_closed]
PolynomialCategory.category [in category]
PolynomialCategory.cocartesian [in cocartesian]
PolynomialCategory.comp [in comp]
PolynomialCategory.distributive [in distributive]
PolynomialCategory.eq [in eq]
PolynomialCategory.initialized [in initialized]
PolynomialCategory.terminated [in terminated]
postcompose [in postcompose]
powerdomainF [in powerdomainF]
powerdom.all_tokens [in all_tokens]
powerdom.concat_elem [in concat_elem]
powerdom.convex_preord_mixin [in convex_preord_mixin]
powerdom.convex_ord [in convex_ord]
powerdom.empty [in empty]
powerdom.empty_elem [in empty_elem]
powerdom.empty_rel [in empty_rel]
powerdom.enum_elems [in enum_elems]
powerdom.fmap [in fmap]
powerdom.fmap_convex [in fmap_convex]
powerdom.fmap_convex_rel [in fmap_convex_rel]
powerdom.fmap_lower [in fmap_lower]
powerdom.fmap_lower_rel [in fmap_lower_rel]
powerdom.fmap_upper_rel [in fmap_upper_rel]
powerdom.fmap_spec [in fmap_spec]
powerdom.fmap_rel [in fmap_rel]
powerdom.fmap_upper [in fmap_upper]
powerdom.join [in join]
powerdom.joinNT [in joinNT]
powerdom.join_rel [in join_rel]
powerdom.lower_ord [in lower_ord]
powerdom.lower_preord_mixin [in lower_preord_mixin]
powerdom.normal_pdoms [in normal_pdoms]
powerdom.pdomain [in pdomain]
powerdom.pdom_plt [in pdom_plt]
powerdom.pdom_effective [in pdom_effective]
powerdom.pdom_ord [in pdom_ord]
powerdom.powerdomain [in powerdomain]
powerdom.select_pdom_elems [in select_pdom_elems]
powerdom.single [in single]
powerdom.singleNT [in singleNT]
powerdom.single_elem [in single_elem]
powerdom.single_rel [in single_rel]
powerdom.union [in union]
powerdom.union_rel [in union_rel]
powerdom.union_elem [in union_elem]
powerdom.upper_preord_mixin [in upper_preord_mixin]
powerdom.upper_ord [in upper_ord]
PPLT_EMBED_initialized [in PPLT_EMBED_initialized]
PPLT_EMBED_initialized_mixin [in PPLT_EMBED_initialized_mixin]
precompose [in precompose]
PREORD [in PREORD]
preord_initialized_mixin [in preord_initialized_mixin]
Preord_Eq [in Preord_Eq]
preord_hom_eq [in preord_hom_eq]
preord_terminated [in preord_terminated]
preord_apply [in preord_apply]
preord_cartesian_mixin [in preord_cartesian_mixin]
preord_terminated_mixin [in preord_terminated_mixin]
preord_initiate [in preord_initiate]
preord_initialized [in preord_initialized]
PREORD_concrete [in PREORD_concrete]
preord_curry [in preord_curry]
preord_terminate [in preord_terminate]
preord_ccc_mixin [in preord_ccc_mixin]
preord_cartesian [in preord_cartesian]
PREORD_EQ_DEC [in PREORD_EQ_DEC]
preord_comp [in preord_comp]
preord_ccc [in preord_ccc]
Preord.compose [in compose]
Preord.comp_mixin [in comp_mixin]
Preord.eq [in eq]
Preord.eq_mixin [in eq_mixin]
Preord.hom_eq [in hom_eq]
Preord.hom_ord [in hom_ord]
Preord.ident [in ident]
Preord.ord_mixin [in ord_mixin]
Preord.ord_eq [in ord_eq]
Preord.ord_op [in ord_op]
prodF [in prodF]
prod_fmap [in prod_fmap]
prod_preord [in prod_preord]
prod_ord [in prod_ord]
PROD.comp_mixin [in comp_mixin]
PROD.hom_eq [in hom_eq]
PROD.hom_comp [in hom_comp]
PROD.hom_eq_mixin [in hom_eq_mixin]
PROD.hom_equiv [in hom_equiv]
PROD.PROD [in PROD]
PROD.prod_compose [in prod_compose]
PROD.prod_ident [in prod_ident]
project_rel [in project_rel]
project_hom [in project_hom]
Pullback.commuting_square [in commuting_square]
Pullback.pullback_lemma1 [in pullback_lemma1]
Pullback.pullback_lemma_map2 [in pullback_lemma_map2]
Pullback.pullback_lemma1_map1 [in pullback_lemma1_map1]


R

repack [in repack]
right_finset [in right_finset]
right_whisker [in right_whisker]


S

select_jrels [in select_jrels]
semidec_disj [in semidec_disj]
semidec_true [in semidec_true]
semidec_conj [in semidec_conj]
semidec_false [in semidec_false]
semidirected_cl [in semidirected_cl]
semvalue [in semvalue]
SET [in SET]
SET_terminate [in SET_terminate]
SET_terminus [in SET_terminus]
set_preord [in set_preord]
SET_COMP [in SET_COMP]
SET_terminated [in SET_terminated]
SET_EQ [in SET_EQ]
SET_concrete [in SET_concrete]
SET.compose [in compose]
SET.ident [in ident]
SET.set_ob_Eq [in set_ob_Eq]
set.set_preord [in set_preord]
SET.set_hom_comp [in set_hom_comp]
SET.set_hom_eq [in set_hom_eq]
single [in single]
smash_prod [in smash_prod]
sndF [in sndF]
sndF_cocone [in sndF_cocone]
sndF_univ [in sndF_univ]
strict_app' [in strict_app']
strict_app [in strict_app]
strict_curry' [in strict_curry']
strict_curry [in strict_curry]
string_ord [in string_ord]
string_ord_mixin [in string_ord_mixin]
sumF [in sumF]
sum_preord [in sum_preord]
sum_fmap_func [in sum_fmap_func]
sum_map [in sum_map]
sum_fmap [in sum_fmap]
sum_cases [in sum_cases]
sum_ord [in sum_ord]
Support.disjoint [in disjoint]


T

Terminated.category [in category]
Terminated.comp [in comp]
Terminated.eq [in eq]
Terminated.eq' [in eq']
Terminated.terminate_op [in terminate_op]
Terminated.terminus_op [in terminus_op]
tmsize [in tmsize]
traverse [in traverse]
traverse [in traverse]
tydom [in tydom]
tydom [in tydom]
tydom [in tydom]
tydom [in tydom]
TYPE.compose [in compose]
TYPE.ident [in ident]
TYPE.thom [in thom]
TYPE.tob [in tob]
TYPE.TYPE [in TYPE]


U

unenumerate [in unenumerate]
unenumerate_set [in unenumerate_set]
unfold_stream [in unfold_stream]
unimage_jrel [in unimage_jrel]
union [in union]
union2 [in union2]
unitpo [in unitpo]
unit_plotkin [in unit_plotkin]
unlift_list [in unlift_list]
unpairing [in unpairing]
unsmash_prod [in unsmash_prod]
upper_set [in upper_set]
upper_bound [in upper_bound]


V

value [in value]
value [in value]


Y

Ybody [in Ybody]
Ysem [in Ysem]



Module Index

A

Adjunction [in Adjunction]
Alg [in Alg]


B

Bicategory [in Bicategory]


C

Cartesian [in Cartesian]
CartesianClosed [in CartesianClosed]
Category [in Category]
Cocartesian [in Cocartesian]
colored_sets [in colored_sets]
Comp [in Comp]
Cone [in Cone]
CPO [in CPO]


D

Distributive [in Distributive]


E

enumtype [in enumtype]
ENV [in ENV]
ENV [in ENV]
env_input [in env_input]
env_input [in env_input]
Eq [in Eq]
eset [in eset]


F

FINPROD [in FINPROD]
finprod [in finprod]
FINPROD_INPUT [in FINPROD_INPUT]
finprod.internals [in finprod.internals]
finset [in finset]
fintype [in fintype]
Functor [in Functor]


G

Groupoid [in Groupoid]


I

Initialized [in Initialized]


N

Nominal [in Nominal]
NT [in NT]


P

Perm [in Perm]
PLT [in PLT]
PolynomialCategory [in PolynomialCategory]
powerdom [in powerdom]
Preord [in Preord]
PROD [in PROD]
Pseudofunctor [in Pseudofunctor]
Pullback [in Pullback]


S

SET [in SET]
set [in set]
Support [in Support]


T

Terminated [in Terminated]
TYPE [in TYPE]



Axiom Index

F

FINPROD_INPUT.A [in A]
FINPROD_INPUT.F [in F]
FINPROD_INPUT.Adec [in Adec]
FINPROD.A [in A]
FINPROD.Adec [in Adec]
FINPROD.bind_unbind [in bind_unbind]
FINPROD.F [in F]
FINPROD.finprod [in finprod]
FINPROD.finprod_proj_commute [in finprod_proj_commute]
FINPROD.finprod_universal [in finprod_universal]
FINPROD.mk_finprod [in mk_finprod]
FINPROD.mk_finprod_compose_commute [in mk_finprod_compose_commute]
FINPROD.proj [in proj]
FINPROD.proj_bind_neq [in proj_bind_neq]
FINPROD.proj_bind [in proj_bind]
FINPROD.proj_bind_eq [in proj_bind_eq]



Variable Index

A

Adjunction.adjunction.C [in C]
Adjunction.adjunction.D [in D]
Adjunction.adjunction.L [in L]
Adjunction.adjunction.R [in R]
Alg.alg.C [in C]
Alg.alg.F [in F]
Alg.forget.C [in C]
Alg.forget.F [in F]


B

Bicategory.bicategory.cat_axioms [in cat_axioms]
Bicategory.bicategory.comp [in comp]
Bicategory.bicategory.CompHom [in CompHom]
Bicategory.bicategory.CompHoriz [in CompHoriz]
Bicategory.bicategory.eq [in eq]
Bicategory.bicategory.hom [in hom]
Bicategory.bicategory.hom2 [in hom2]
Bicategory.bicategory.Ident [in Ident]
Bicategory.bicategory.ob [in ob]
bilimit.bilimit_univ.YC [in YC]
bilimit.DS [in DS]
bilimit.hf [in hf]
bilimit.I [in I]
bottom.X [in X]
bottom.Y [in Y]


C

CartesianClosed.cartesian_closed.comp [in comp]
CartesianClosed.cartesian_closed.axioms.curry [in curry]
CartesianClosed.cartesian_closed.cat_axioms [in cat_axioms]
CartesianClosed.cartesian_closed.axioms.exp [in exp]
CartesianClosed.cartesian_closed.cartesian [in cartesian]
CartesianClosed.cartesian_closed.eq [in eq]
CartesianClosed.cartesian_closed.hom [in hom]
CartesianClosed.cartesian_closed.terminated [in terminated]
CartesianClosed.cartesian_closed.ob [in ob]
CartesianClosed.cartesian_closed.axioms.apply [in apply]
Cartesian.cartesian.axioms.pairing [in pairing]
Cartesian.cartesian.axioms.product [in product]
Cartesian.cartesian.axioms.proj1 [in proj1]
Cartesian.cartesian.axioms.proj2 [in proj2]
Cartesian.cartesian.comp [in comp]
Cartesian.cartesian.eq [in eq]
Cartesian.cartesian.hom [in hom]
Cartesian.cartesian.ob [in ob]
cast.A [in A]
cast.Adec [in Adec]
cast.F [in F]
cast.hf [in hf]
category_axioms.C [in C]
Category.category.COMP [in COMP]
Category.category.EQ [in EQ]
Category.category.hom [in hom]
Category.category.ob [in ob]
Cocartesian.cocartesian.axioms.either [in either]
Cocartesian.cocartesian.axioms.inl [in inl]
Cocartesian.cocartesian.axioms.inr [in inr]
Cocartesian.cocartesian.axioms.sum [in sum]
Cocartesian.cocartesian.comp [in comp]
Cocartesian.cocartesian.eq [in eq]
Cocartesian.cocartesian.hom [in hom]
Cocartesian.cocartesian.ob [in ob]
colimit_decompose2.I [in I]
colimit_decompose.I [in I]
colimit_decompose2.CC [in CC]
colimit_decompose.CC [in CC]
colimit_decompose2.DS [in DS]
colimit_decompose.DS [in DS]
colimit_decompose2.hf [in hf]
colimit_decompose.hf [in hf]
colimit_decompose2.decompose [in decompose]
colimit_decompose.Hcolimit [in Hcolimit]
colored_sets.colored_sets.cunion.A [in A]
colored_sets.colored_sets.C [in C]
colored_sets.colored_sets.T [in T]
colored_sets.colored_sets.cunion.XS [in XS]
Cone.cone.C [in C]
Cone.cone.F [in F]
Cone.cone.J [in J]
countable_ID.A [in A]
CPO.prod.A [in A]
CPO.prod.B [in B]
CPO.prod.CL [in CL]
curry.A [in A]
curry.B [in B]
curry.C [in C]
curry.HAeff [in HAeff]
curry.HAplt [in HAplt]
curry.HBeff [in HBeff]
curry.HBplt [in HBplt]
curry.HCeff [in HCeff]
curry.hf [in hf]
curry.HR [in HR]
curry.HRdir [in HRdir]
curry.R [in R]
curry.Reff [in Reff]
curry.R' [in R']


D

dec_lemmas.A [in A]
dec_lemmas.Hplt [in Hplt]
dec_lemmas.hf [in hf]
dec_lemmas.Heff [in Heff]
directed_joinables.HBplt [in HBplt]
directed_joinables.A [in A]
directed_joinables.B [in B]
directed_joinables.swell.swell_relation.G [in G]
directed_joinables.M [in M]
directed_joinables.R [in R]
directed_joinables.swell.swell_relation.z [in z]
directed_joinables.swell.swell_relation.ODAB [in ODAB]
directed_joinables.swell.RSinh [in RSinh]
directed_joinables.swell.swell_relation.noub [in noub]
directed_joinables.Minh [in Minh]
directed_joinables.swell.swell_relation.G0inh [in G0inh]
directed_joinables.swell.swell_relation.G0 [in G0]
directed_joinables.swell.swell_relation.HG [in HG]
directed_joinables.HM [in HM]
directed_joinables.HR [in HR]
directed_joinables.swell.swell_relation.Hz [in Hz]
directed_joinables.OD [in OD]
directed_joinables.HAeff [in HAeff]
directed_joinables.RS [in RS]
directed_joinables.swell.RS [in RS]
directed_joinables.swell.swell_relation.XS [in XS]
directed_joinables.HRdir [in HRdir]
directed_joinables.hf [in hf]
directed_joinables.HBeff [in HBeff]
directed_joinables.swell.swell_relation.HG' [in HG']
directed_joinables.swell.swell_relation.HG0 [in HG0]
directed_joinables.swell.HRS [in HRS]
directed_joinables.HAplt [in HAplt]
directed_joinables.swell.swell_relation.HXS [in HXS]
directed_joinables.swell.RS' [in RS']
disc_cases.A [in A]
disc_cases.B [in B]
disc_cases.X [in X]
disc_cases.f [in f]
Distributive.distributive.cartesian [in cartesian]
Distributive.distributive.cat_axioms [in cat_axioms]
Distributive.distributive.cocartesian [in cocartesian]
Distributive.distributive.comp [in comp]
Distributive.distributive.eq [in eq]
Distributive.distributive.hom [in hom]
Distributive.distributive.initialized [in initialized]
Distributive.distributive.ob [in ob]
Distributive.distributive.terminated [in terminated]


E

epic.C [in C]
ep_pairs.embed_func_ep_pair.X [in X]
ep_pairs.ep_pair_embed_func.X [in X]
ep_pairs.embed_func_ep_pair.Y [in Y]
ep_pairs.ep_pair_embed_func.Y [in Y]
ep_pairs.ep_pair_embed_func.e [in e]
ep_pairs.ep_pair_embed_func.p [in p]
ep_pairs.ep_pair_embed_func.embed_func.x [in x]
ep_pairs.ep_pair_embed_func.ep [in ep]
ep_pairs.hf [in hf]
ep_pairs.ep_pair_embed_func.Hep [in Hep]
ep_pairs.embed_func_ep_pair.embed [in embed]
expF_decompose.I [in I]
expF_decompose.CC1 [in CC1]
expF_decompose.CC2 [in CC2]
expF_decompose.DS1 [in DS1]
expF_decompose.DS2 [in DS2]
expF_decompose.decompose1 [in decompose1]
expF_decompose.decompose2 [in decompose2]
expF_decompose.hf [in hf]
exp_functor.A [in A]
exp_functor.B [in B]
exp_functor.C [in C]
exp_functor.D [in D]
exp_functor.f [in f]
exp_functor.g [in g]
exp_functor.hf [in hf]


F

finprod.internals.finprod_univ_rel.X [in X]
finprod.internals.finprod_univ_rel.f [in f]
finprod.internals.finprod_univ_rel.finprod_univ_rel [in finprod_univ_rel]
finprod.internals.finprod_univ_rel.Hf [in Hf]
finprod.internals.finprod_univ_rel.ls [in ls]
finprod.internals.finprod_univ_rel.avd [in avd]
finprod.termmodel.tm [in tm]
finprod.termmodel.varmap_compose.f [in f]
finprod.termmodel.varmap_compose.g [in g]
finprod.termmodel.varmap_compose.Γ₁ [in Γ₁]
finprod.termmodel.varmap_compose.Γ₂ [in Γ₂]
finprod.termmodel.varmap_compose.Γ₃ [in Γ₃]
finprod.varmap.tm [in tm]
finprod.varmap.tm_weaken [in tm_weaken]
finprod.varmap.tm_var [in tm_var]
finsubset.A [in A]
finsubset.Hdec [in Hdec]
finsubset.HP [in HP]
finsubset.P [in P]
fixes.A [in A]
fixes.f [in f]
fixes.Γ [in Γ]
fixpoint.BL [in BL]
fixpoint.C [in C]
fixpoint.cata.AG [in AG]
fixpoint.colimit_cocone [in colimit_cocone]
fixpoint.F [in F]
fixpoint.F [in F]
fixpoint.Fcontinuous [in Fcontinuous]
fixpoint.Fcontinuous [in Fcontinuous]
fixpoint.has_colimits [in has_colimits]
flat_cases.A [in A]
flat_cases.B [in B]
flat_cases.X [in X]
flat_cases.f [in f]
fresh.atoms [in atoms]
fstF_continuous.C [in C]
fstF_continuous.D [in D]
fstF_continuous.I [in I]
fstF_continuous.CC [in CC]
fstF_continuous.DS [in DS]
fstF_continuous.Hcolim [in Hcolim]
functor_compose.C [in C]
functor_compose.D [in D]
functor_compose.E [in E]
Functor.functor.C [in C]
Functor.functor.D [in D]


G

Groupoid.groupoid.axioms.inv [in inv]
Groupoid.groupoid.cat_axioms [in cat_axioms]
Groupoid.groupoid.comp [in comp]
Groupoid.groupoid.eq [in eq]
Groupoid.groupoid.hom [in hom]
Groupoid.groupoid.ob [in ob]


I

idents_length.len [in len]
idents_length.len0 [in len0]
image_compose.A [in A]
image_compose.B [in B]
image_compose.C [in C]
image_compose.T [in T]
image_compose.f [in f]
image_compose.g [in g]
image_compose.XS [in XS]
Initialized.initialized.eq [in eq]
Initialized.initialized.hom [in hom]
Initialized.initialized.ob [in ob]
iso.C [in C]
iter_chain.X [in X]
iter_chain.base [in base]
iter_chain.step_base [in step_base]
iter_chain.step [in step]
iter_chain.hf [in hf]
iter_chain.step_mono [in step_mono]


J

joinable_plt.HBplt [in HBplt]
joinable_plt.A [in A]
joinable_plt.B [in B]
joinable_plt.join_rel_normal.P [in P]
joinable_plt.join_rel_normal.Q [in Q]
joinable_plt.join_rel_normal.HP [in HP]
joinable_plt.join_rel_normal.HQ [in HQ]
joinable_plt.HAeff [in HAeff]
joinable_plt.hf [in hf]
joinable_plt.HBeff [in HBeff]
joinable_plt.HAplt [in HAplt]


L

lfp.f [in f]
lfp.Hpointed [in Hpointed]
lfp.X [in X]


M

map_rel.f [in f]
map_rel.g [in g]
mono.C [in C]


N

nominal_fixpoint.F [in F]
nominal_directed_colimits.I [in I]
nominal_directed_colimits.DS [in DS]
nominal_fixpoint.HF [in HF]
nominal_directed_colimits.nom_colimit_univ.YC [in YC]
nom_sum.A [in A]
nom_sum.B [in B]
normal_sets.A [in A]
normal_sets.normal_mubs.H [in H]
normal_sets.normal_mubs.P [in P]
normal_sets.normal_mubs.Q [in Q]
normal_sets.normal_mubs.X [in X]
normal_sets.normal_mubs.Y [in Y]
normal_sets.plt_normal.Hplt [in Hplt]
normal_sets.Hnorm [in Hnorm]
normal_sets.normal_mubs.Hinh [in Hinh]
normal_sets.normal_mubs.H0 [in H0]
normal_sets.normal_mubs.H1 [in H1]
normal_sets.normal_mubs.H2 [in H2]
normal_sets.OD [in OD]
normal_sets.hf [in hf]
normal_sets.Heff [in Heff]
NT.NT_mixins.C [in C]
NT.nt_compose.C [in C]
NT.NT_mixins.D [in D]
NT.nt_compose.D [in D]
NT.nt_compose.E [in E]
NT.nt.C [in C]
NT.nt.D [in D]
NT.nt.F [in F]
NT.nt.G [in G]


P

pairF_continuous.C [in C]
pairF_continuous.D [in D]
pairF_continuous.E [in E]
pairF_continuous.F [in F]
pairF_continuous.G [in G]
pairF_continuous.cocones.I [in I]
pairF_continuous.cocones.DS [in DS]
pairF_continuous.HcontF [in HcontF]
pairF_continuous.HcontG [in HcontG]
pairF.C [in C]
pairF.D [in D]
pairF.E [in E]
pairF.F [in F]
pairF.G [in G]
plt_const.A [in A]
plt_const.B [in B]
plt_const.b [in b]
plt_const.hf [in hf]
PLT.PLT.hf [in hf]
PLT.PLT.homset_cpo.A [in A]
PLT.PLT.homset_cpo.B [in B]
powerdom_decompose.I [in I]
powerdom_functor.X [in X]
powerdom_functor.Y [in Y]
powerdom_functor.sort [in sort]
powerdom_decompose.CC [in CC]
powerdom_decompose.DS [in DS]
powerdom_decompose.hf [in hf]
powerdom_functor.hf [in hf]
powerdom_decompose.decompose [in decompose]
powerdom.powerdom.hf [in hf]
powerdom.powerdom.orders.X [in X]
powerdom.powerdom.orders.Xeff [in Xeff]
powerdom.powerdom.orders.Xplt [in Xplt]
powerdom.powerdom.powerdomain_fmap.X [in X]
powerdom.powerdom.powerdomain_fmap.Y [in Y]
powerdom.powerdom.powerdomain_fmap.f [in f]
prod_functor.A [in A]
prod_functor.B [in B]
prod_functor.C [in C]
prod_functor.D [in D]
prod_functor.f [in f]
prod_functor.g [in g]
prod_functor.hf [in hf]
PROD.product_category.C [in C]
PROD.product_category.D [in D]
projF.C [in C]
projF.D [in D]
Pullback.pullback_lemma.C [in C]
Pullback.pullback_lemma.pullback_lemma1.pb_map.H [in H]
Pullback.pullback_lemma.pullback_lemma1.pb_map.Q [in Q]
Pullback.pullback_lemma.R [in R]
Pullback.pullback_lemma.S [in S]
Pullback.pullback_lemma.W [in W]
Pullback.pullback_lemma.X [in X]
Pullback.pullback_lemma.Y [in Y]
Pullback.pullback_lemma.Z [in Z]
Pullback.pullback_lemma.pullback_lemma1.pb_map.p [in p]
Pullback.pullback_lemma.pullback_lemma1.pb_map.q [in q]
Pullback.pullback_lemma.pullback_lemma1.PB1 [in PB1]
Pullback.pullback_lemma.pullback_lemma1.PB2 [in PB2]
Pullback.pullback_lemma.f1 [in f1]
Pullback.pullback_lemma.f2 [in f2]
Pullback.pullback_lemma.f3 [in f3]
Pullback.pullback_lemma.g1 [in g1]
Pullback.pullback_lemma.g2 [in g2]
Pullback.pullback_lemma.h1 [in h1]
Pullback.pullback_lemma.h2 [in h2]
Pullback.pullback.C [in C]


S

set.mixin_def.incl [in incl]
set.mixin_def.union [in union]
set.mixin_def.image [in image]
set.mixin_def.member [in member]
set.mixin_def.single [in single]
set.mixin_def.set [in set]
sndF_continuous.C [in C]
sndF_continuous.D [in D]
sndF_continuous.I [in I]
sndF_continuous.CC [in CC]
sndF_continuous.DS [in DS]
sndF_continuous.Hcolim [in Hcolim]
strictify.f [in f]
strictify.strictify [in strictify]
strictify.X [in X]
strictify.Y [in Y]
sum_functor.A [in A]
sum_functor.B [in B]
sum_functor.C [in C]
sum_functor.D [in D]
sum_functor.f [in f]
sum_functor.g [in g]
sum_functor.hf [in hf]


T

Terminated.terminated.eq [in eq]
Terminated.terminated.hom [in hom]
Terminated.terminated.ob [in ob]
test_functor_assocative_convertability.C [in C]
test_functor_assocative_convertability.D [in D]
test_functor_assocative_convertability.E [in E]
test_functor_assocative_convertability.F [in F]
test_functor_assocative_convertability.G [in G]
test_functor_assocative_convertability.H [in H]
test_functor_assocative_convertability.I [in I]
total_fixpoint.A [in A]
total_fixpoint.F [in F]
total_fixpoint.h [in h]
total_fixpoint.BL [in BL]
total_fixpoint.Fcontinuous [in Fcontinuous]
traverse.rename_var [in rename_var]
traverse.rename_var [in rename_var]
traverse.thingy [in thingy]
traverse.thingy [in thingy]
traverse.thingy_term [in thingy_term]
traverse.thingy_term [in thingy_term]
traverse.varmap_denote_proj [in varmap_denote_proj]
traverse.varmap_denote_proj [in varmap_denote_proj]
traverse.weaken_vars [in weaken_vars]
traverse.weaken_vars [in weaken_vars]
traverse.weaken_sem_bind [in weaken_sem_bind]
traverse.weaken_sem_bind [in weaken_sem_bind]


U

unfold.A [in A]
unfold.ind_step [in ind_step]
unfold.invariant [in invariant]
unfold.out_prop [in out_prop]
unfold.step [in step]
unfold.wf [in wf]
unfold.wf_rel [in wf_rel]
unfold.X [in X]


Y

Ydefn.σ₁ [in σ₁]
Ydefn.σ₂ [in σ₂]



Library Index

A

approx_rels
atoms


B

basics
bicategories
bilimit


C

categories
cont_adj
cont_functors
cpo


D

directed
discrete


E

effective
embed
esets
exp_functor


F

finprod
finsets
fixes
flat


J

joinable


L

lam_models


N

nominal
notations


P

pairing
permutations
plotkin
powerdom
preord
profinite
profinite_adj


S

sets
ski
skiy
strict_utils
st_lam_fix
st_lam
sumprod_functor



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 _ other (3088 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 _ other (2 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 _ other (316 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 _ other (84 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 _ other (768 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 _ other (105 entries)
Notation 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 _ other (97 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 _ other (196 entries)
Abbreviation 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 _ other (101 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 _ other (28 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 _ other (878 entries)
Module 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 _ other (43 entries)
Axiom 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 _ other (16 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 _ other (417 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 _ other (37 entries)

This page has been generated by coqdoc