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 (2527 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 (101 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 (207 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 (70 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 (395 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 (273 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 (116 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 (106 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 (41 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 (30 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 (571 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 (33 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 (19 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 (406 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 (159 entries)

Global Index

A

ACommutes [projection, in Adjoint]
ACommutes_Inverse [lemma, in Adjoint]
AComponentsOf [projection, in Adjoint]
action_respectful [projection, in Monoid]
Add [constructor, in Exercise_4_2_3_12]
AddEdge [constructor, in Path]
addedge_equivalent [lemma, in Schema]
Adjoint [library]
AdjointComposition [library]
AdjointUnit [library]
Adjunction [record, in Adjoint]
Adjunction [section, in Adjoint]
AdjunctionCounit [definition, in AdjointUnit]
AdjunctionEquivalences [section, in Adjoint]
AdjunctionEquivalences' [section, in Adjoint]
AdjunctionEquivalences'.F [variable, in Adjoint]
AdjunctionEquivalences'.G [variable, in Adjoint]
AdjunctionEquivalences.F [variable, in Adjoint]
AdjunctionEquivalences.G [variable, in Adjoint]
AdjunctionEquivalences.typeof [section, in Adjoint]
AdjunctionEquivalences.typeof.adjunction_naturality'T' [variable, in Adjoint]
AdjunctionEquivalences.typeof.adjunction_naturalityT' [variable, in Adjoint]
AdjunctionEquivalences.typeof.adjunction_naturality'T [variable, in Adjoint]
AdjunctionEquivalences.typeof.adjunction_naturalityT [variable, in Adjoint]
AdjunctionEquivalences.typeof.typeof [variable, in Adjoint]
AdjunctionUnit [definition, in AdjointUnit]
AdjunctionUnit [section, in AdjointUnit]
AdjunctionUnitCounit [record, in AdjointUnit]
AdjunctionUnit.F [variable, in AdjointUnit]
AdjunctionUnit.G [variable, in AdjointUnit]
adjunction_naturality' [definition, in Adjoint]
adjunction_naturality [definition, in Adjoint]
adjunction_naturality'_pre [lemma, in Adjoint]
adjunction_naturality_pre [lemma, in Adjoint]
Adjunction_UnitCounitEquation2 [projection, in AdjointUnit]
Adjunction_UnitCounitEquation1 [projection, in AdjointUnit]
Adjunction_Counit [projection, in AdjointUnit]
Adjunction_Unit [projection, in AdjointUnit]
Adjunction.COp [variable, in Adjoint]
Adjunction.DOp [variable, in Adjoint]
Adjunction.F [variable, in Adjoint]
Adjunction.FOp [variable, in Adjoint]
Adjunction.G [variable, in Adjoint]
Adjunction.HomCPreFunctor [variable, in Adjoint]
Adjunction.HomDPreFunctor [variable, in Adjoint]
Adjunction2HomAdjunction [definition, in Adjoint]
AIsomorphism [projection, in Adjoint]
AMateOf [projection, in Adjoint]
apply_to_classOf [lemma, in EquivalenceClass]
apply_to_class_f_surj [lemma, in EquivalenceClass]
apply_to_class_f_inj [lemma, in EquivalenceClass]
apply_to_class [definition, in EquivalenceClass]
apply1 [section, in EquivalenceClass]
apply1.equiv' [variable, in EquivalenceClass]
apply1.equiv'_Equivalence [variable, in EquivalenceClass]
apply1.equiv0 [variable, in EquivalenceClass]
apply1.E0 [variable, in EquivalenceClass]
apply1.f [variable, in EquivalenceClass]
apply1.f_mor [variable, in EquivalenceClass]
apply1.value' [variable, in EquivalenceClass]
apply1.value0 [variable, in EquivalenceClass]
apply2 [section, in EquivalenceClass]
apply2_to_classOf [lemma, in EquivalenceClass]
apply2_to_class_f_surj [lemma, in EquivalenceClass]
apply2_to_class_f_inj [lemma, in EquivalenceClass]
apply2_to_class [definition, in EquivalenceClass]
apply2.equiv' [variable, in EquivalenceClass]
apply2.equiv'_Equivalence [variable, in EquivalenceClass]
apply2.equiv0 [variable, in EquivalenceClass]
apply2.equiv1 [variable, in EquivalenceClass]
apply2.E0 [variable, in EquivalenceClass]
apply2.E1 [variable, in EquivalenceClass]
apply2.f [variable, in EquivalenceClass]
apply2.f_mor [variable, in EquivalenceClass]
apply2.value' [variable, in EquivalenceClass]
apply2.value0 [variable, in EquivalenceClass]
apply2.value1 [variable, in EquivalenceClass]
ArbitraryIntersection [definition, in Topology]
ArbitraryUnion [inductive, in Topology]
ArbitraryUnionOpen [projection, in Topology]
ArbitraryUnion_inJ [constructor, in Topology]
ArithmeticCategory [definition, in Exercise_4_2_3_12]
ArithmeticGroupoid [definition, in Exercise_4_2_3_12]
ArrowCategory [definition, in CommaCategory]
ArrowCategory [section, in CommaCategory]
Arrow' [projection, in Graph]
assoc [projection, in Monoid]
Associativity [projection, in Category]
AssociativityComposition [section, in CategoryMorphisms]
AssociativityComposition.o0 [variable, in CategoryMorphisms]
AssociativityComposition.o1 [variable, in CategoryMorphisms]
AssociativityComposition.o2 [variable, in CategoryMorphisms]
AssociativityComposition.o3 [variable, in CategoryMorphisms]
AssociativityComposition.o4 [variable, in CategoryMorphisms]
AssociativityNoEvar [lemma, in Category]


B

Base [constructor, in Common]
Build_CommaCategory_Morphism' [definition, in CommaCategory]
Build_CommaCategory_Object' [definition, in CommaCategory]
Build_Equivalence [constructor, in Isomorphism]


C

C [definition, in Exercise_4_3_1_10]
CategoriesIsomorphic [definition, in FunctorIsomorphisms]
CategoriesIsomorphic_trans [lemma, in FunctorIsomorphisms]
CategoriesIsomorphic_sym [lemma, in FunctorIsomorphisms]
CategoriesIsomorphic_refl [lemma, in FunctorIsomorphisms]
CategoriesIsomorphic_IsomorphismOfCategories [lemma, in FunctorIsomorphisms]
CategoriesNaturallyEquivalent [definition, in NaturalEquivalence]
Category [record, in Category]
Category [library]
CategoryConnected [record, in Exercise_4_2_1_16]
CategoryInCategoryOfCategories [definition, in ComputableCategory]
CategoryInCategoryOfCategories' [definition, in ComputableCategory]
CategoryIsomorphisms [library]
CategoryMorphisms [library]
CategoryObjects [library]
CategoryObjects1 [section, in CategoryObjects]
CategoryObjects1.initial [section, in CategoryObjects]
CategoryObjects1.terminal [section, in CategoryObjects]
CategoryObjects2 [section, in CategoryObjects]
CategoryOf [abbreviation, in SetCategory]
CategoryOfCategories [definition, in ComputableCategory]
CategoryOfCategoriesOn [abbreviation, in ComputableCategory]
CategoryOfCategories_product [instance, in ProductCategory]
CategoryOfElements [definition, in Grothendieck]
CategoryOfGraphs [definition, in GraphCategory]
CategoryOfGraphs [section, in GraphCategory]
CategoryOfGraph's [definition, in GraphCategory]
CategoryOfGroupoids [definition, in Groupoid]
CategoryOfGroups [definition, in GroupCategory]
CategoryOfGroups [section, in GroupCategory]
CategoryOfMonoids [definition, in MonoidCategory]
CategoryOfMonoids [section, in MonoidCategory]
CategoryOfPreOrders [definition, in PreOrderCategory]
CategoryOfProps [definition, in SetCategory]
CategoryOfPropsFalseInitial [definition, in SetCategoryFacts]
CategoryOfPropsTrueTerminal [definition, in SetCategoryFacts]
CategoryOfSets [definition, in SetCategory]
CategoryOfSetsEmptyInitial [definition, in SetCategoryFacts]
CategoryOfSetsFalseInitial [definition, in SetCategoryFacts]
CategoryOfSetsSingletonTerminal [definition, in SetCategoryFacts]
CategoryOfSetsTrueTerminal [definition, in SetCategoryFacts]
CategoryOfSetsUnitTerminal [definition, in SetCategoryFacts]
CategoryOfTopologies [definition, in TopologyCategory]
CategoryOfTopologies [section, in TopologyCategory]
CategoryOfTypes [definition, in SetCategory]
CategoryOfTypesEmptyInitial [definition, in SetCategoryFacts]
CategoryOfTypesFalseInitial [definition, in SetCategoryFacts]
CategoryOfTypesSingletonTerminal [definition, in SetCategoryFacts]
CategoryOfTypesTrueTerminal [definition, in SetCategoryFacts]
CategoryOfTypesUnitTerminal [definition, in SetCategoryFacts]
_ ≅ _ (type_scope) [notation, in CategoryIsomorphisms]
_ ≅ _ [notation, in CategoryIsomorphisms]
category_isomorphisms.Isomorphic [section, in CategoryIsomorphisms]
category_isomorphisms.IsIsomorphism [section, in CategoryIsomorphisms]
_ ≅ _ (type_scope) [notation, in CategoryIsomorphisms]
_ ≅ _ (category_scope) [notation, in CategoryIsomorphisms]
category_isomorphisms.Isomorphism [section, in CategoryIsomorphisms]
category_isomorphisms.IsomorphismOf [section, in CategoryIsomorphisms]
category_isomorphisms [section, in CategoryIsomorphisms]
category_product.Y [variable, in Product]
category_product.X [variable, in Product]
category_product [section, in Product]
category_coproduct.Y [variable, in Coproduct]
category_coproduct.X [variable, in Coproduct]
category_coproduct [section, in Coproduct]
category_morphisms.properties [section, in CategoryMorphisms]
category_morphisms [section, in CategoryMorphisms]
category_connected [projection, in Exercise_4_2_1_16]
Category_sig_mor_as_sig [definition, in Subcategory]
Category_sig_mor [definition, in Subcategory]
Category_sig_obj_as_sig [definition, in Subcategory]
Category_sig_obj [definition, in Subcategory]
Category_sig [definition, in Subcategory]
cat_has_products [section, in ProductCategory]
cgroup [projection, in Group]
ChainCat [section, in ChainCategory]
ChainCategory [definition, in ChainCategory]
ChainCategory [library]
ChainCategory' [definition, in ChainCategory]
ClassContainsEquivalent [projection, in EquivalenceClass]
ClassElementsEquivalent [projection, in EquivalenceClass]
ClassEquivalent_trans [projection, in EquivalenceClass]
ClassEquivalent_sym [projection, in EquivalenceClass]
ClassEquivalent_refl [projection, in EquivalenceClass]
ClassInhabited [projection, in EquivalenceClass]
classOf [definition, in EquivalenceClass]
classOf_eq [lemma, in EquivalenceClass]
classOf_refl [lemma, in EquivalenceClass]
Closed [definition, in Topology]
closure [definition, in Closure]
closure [section, in Closure]
Closure [library]
closure_respect_subset [lemma, in Closure]
closure_closed_same [lemma, in Closure]
closure_superset [lemma, in Closure]
closure_closed [lemma, in Closure]
cmonoid [projection, in Monoid]
CoercedEmptySetInitialOf [abbreviation, in SetCategoryFacts]
CoercedFalseInitialOf [abbreviation, in SetCategoryFacts]
CoercedTrueTerminalOf [abbreviation, in SetCategoryFacts]
CoercedUnitTerminalOf [abbreviation, in SetCategoryFacts]
Coercions [section, in NaturalEquivalence]
Coercions.F [variable, in NaturalEquivalence]
Coercions.F' [variable, in NaturalEquivalence]
Coercions.G [variable, in NaturalEquivalence]
Coercions.G' [variable, in NaturalEquivalence]
CommaCategory [definition, in CommaCategory]
CommaCategory [section, in CommaCategory]
CommaCategory [library]
CommaCategory_RightIdentity [lemma, in CommaCategory]
CommaCategory_LeftIdentity [lemma, in CommaCategory]
CommaCategory_Associativity [lemma, in CommaCategory]
CommaCategory_Identity [definition, in CommaCategory]
CommaCategory_Compose [definition, in CommaCategory]
CommaCategory_Morphism_Eq [lemma, in CommaCategory]
CommaCategory_MorphismT [definition, in CommaCategory]
CommaCategory_Morphism_Member [projection, in CommaCategory]
CommaCategory_Morphism [record, in CommaCategory]
CommaCategory_ObjectT [definition, in CommaCategory]
CommaCategory_Object_Member [projection, in CommaCategory]
CommaCategory_Object [record, in CommaCategory]
CommaCategory.S [variable, in CommaCategory]
CommaCategory.SortPolymorphic_Helper [variable, in CommaCategory]
CommaCategory.T [variable, in CommaCategory]
Common [library]
Common_projT2 [definition, in Common]
Common_projT1 [definition, in Common]
Common_existT [constructor, in Common]
Common_sigT [inductive, in Common]
Commutes [projection, in NaturalTransformation]
comp [projection, in Monoid]
compact [definition, in Compact]
compact [section, in Compact]
Compact [library]
compact.T [variable, in Compact]
compact.X [variable, in Compact]
comparability [projection, in Orders]
comparability [constructor, in Orders]
Comparable [record, in Orders]
Comparable [inductive, in Orders]
complement_intersection [lemma, in Topology]
complement_union [lemma, in Topology]
complement_idempotent [lemma, in Topology]
complement_idempotent [section, in Topology]
CompleteGraph [definition, in Exercise_3_3_1_5]
ComponentsOf [projection, in NaturalTransformation]
compose [definition, in Morphism]
Compose [projection, in Category]
compose [section, in AdjointComposition]
ComposeAdjunctions [definition, in AdjointComposition]
ComposeAdjunctionsUnitMorphism [definition, in AdjointComposition]
ComposeFunctorIsmorphismOf [definition, in FunctorIsomorphisms]
ComposeFunctors [definition, in Functor]
ComposeFunctorsAssociativity [lemma, in Functor]
ComposeFunctorsAssociativityNE [lemma, in NaturalEquivalence]
ComposeFunctorsAssociator1 [definition, in NaturalTransformation]
ComposeFunctorsAssociator2 [definition, in NaturalTransformation]
ComposeIsomorphismOf [instance, in CategoryIsomorphisms]
ComposeSchemaMorphisms [definition, in SchemaMorphism]
ComposeSchemaMorphismsAssociativity [lemma, in SchemaMorphism]
compose_transferPath [lemma, in SchemaMorphism]
compose_relation_homomorphisms [definition, in Orders]
compose_graph'_homomorphisms [definition, in Graph]
compose_graph_homomorphisms [definition, in Graph]
compose_monoid_homomorphisms [definition, in Monoid]
compose_group_homomorphisms [definition, in Group]
compose_continuous [definition, in TopologicalContinuity]
compose_path_prepend [lemma, in Path]
compose_path_addedge [lemma, in Path]
compose_path [definition, in Path]
compose.A [variable, in AdjointComposition]
compose.A' [variable, in AdjointComposition]
compose.F [variable, in AdjointComposition]
compose.F' [variable, in AdjointComposition]
compose.G [variable, in AdjointComposition]
compose.G' [variable, in AdjointComposition]
compose4associativity_helper [lemma, in CategoryMorphisms]
ComputableCategory [definition, in ComputableCategory]
ComputableCategory [section, in ComputableCategory]
ComputableCategory [library]
ComputableCategory.I [variable, in ComputableCategory]
ComputableCategory.Index2Cat [variable, in ComputableCategory]
ComputableCategory.Index2Object [variable, in ComputableCategory]
ComputationalGroup [record, in Group]
ComputationalGroupOfAutomorphisms [definition, in Exercise_3_2_1_7]
ComputationalGroupOfAutomorphismsAction [definition, in Exercise_3_2_1_11]
ComputationalMonoid [record, in Monoid]
ComputationalMonoidOfAutomorphisms [definition, in Exercise_3_2_1_7]
concatenate [definition, in Path]
concatenate_TransferPath [lemma, in SchemaMorphism]
concatenate_transferPath [lemma, in SchemaMorphism]
concatenate_equivalent [lemma, in Schema]
concatenate_associative [lemma, in Path]
concatenate_prepend_p [lemma, in Path]
concatenate_p_addedge [lemma, in Path]
concatenate_concatenate'_equivalent [lemma, in Path]
concatenate_addedge_concatenate'_prepend [lemma, in Path]
concatenate_p_noedges [lemma, in Path]
concatenate_noedges_p [lemma, in Path]
concatenate' [definition, in Path]
concatenate'_noedges_p [lemma, in Path]
concatenate'_p_noedges [lemma, in Path]
concatenate'_p_addedge [lemma, in Path]
Cone [library]
conj_is_product [instance, in SetCategoryFacts]
ConnectedComponents [definition, in Exercise_5_1_1_9]
ConnectedComponentsInjectionFunction [definition, in Exercise_5_1_1_9]
ConnectedComponentsProjectionFunctor [definition, in Exercise_5_1_1_9]
Constant [constructor, in Exercise_4_2_3_12]
ConstantGraph [definition, in Exercise_3_3_1_5]
ContainsEmpty [projection, in Topology]
ContainsSpace [projection, in Topology]
continuous [definition, in TopologicalContinuity]
continuous [section, in TopologicalContinuity]
continuous_induced_functor [definition, in Exercise_4_2_3_2]
continuous_induced_functor_morphism_of [definition, in Exercise_4_2_3_2]
continuous_induced_functor_object_of [definition, in Exercise_4_2_3_2]
continuous.continuous_composition [section, in TopologicalContinuity]
continuous.continuous_identity.Tx [variable, in TopologicalContinuity]
continuous.continuous_identity.X [variable, in TopologicalContinuity]
continuous.continuous_identity [section, in TopologicalContinuity]
continuous.continuous_definition.Ty [variable, in TopologicalContinuity]
continuous.continuous_definition.Tx [variable, in TopologicalContinuity]
continuous.continuous_definition.Y [variable, in TopologicalContinuity]
continuous.continuous_definition.X [variable, in TopologicalContinuity]
continuous.continuous_definition [section, in TopologicalContinuity]
ContravariantHomFunctor [definition, in Hom]
conversion [section, in Graph]
coproduct [record, in Coproduct]
Coproduct [library]
coproduct_is_coproduct [projection, in Coproduct]
coproduct_element [projection, in Coproduct]
coproduct_map_unique [projection, in Coproduct]
coproduct_inr_commutes [projection, in Coproduct]
coproduct_inl_commutes [projection, in Coproduct]
coproduct_map [projection, in Coproduct]
coproduct_inr [projection, in Coproduct]
coproduct_inl [projection, in Coproduct]
coproduct_decidable [instance, in OrderCoproduct]
Corollaries [section, in EqdepFacts_one_variable]
Corollaries.p [variable, in EqdepFacts_one_variable]
Corollaries.U [variable, in EqdepFacts_one_variable]
CosliceCategory [definition, in CommaCategory]
CosliceCategoryOver [definition, in CommaCategory]
CounitOf [definition, in Adjoint]
CovariantHomFunctor [definition, in Hom]
Cover [record, in OpenCover]
CoveringSpace [record, in CoveringSpace]
CoveringSpace [library]
CoveringSpaceHomeomorphism [projection, in CoveringSpace]
CoveringSpaceMap [projection, in CoveringSpace]
CoveringSpaceMap_continuous [projection, in CoveringSpace]
CoveringSpace_IsCoveringSpace [projection, in CoveringSpace]
CoveringSpace_InverseImageSets_DisjointUnion [projection, in CoveringSpace]
CoveringSpace_InverseImageSets [projection, in CoveringSpace]
CoveringSpace_CoverOpen [projection, in CoveringSpace]
CoveringSpace_Cover [projection, in CoveringSpace]
covering_space_inverse_image_open [lemma, in CoveringSpace]
covering_space_open_to_open [lemma, in CoveringSpace]
covering_space_subset_open [lemma, in CoveringSpace]
_ ⁻¹ [notation, in CoveringSpace]
covering_space.T [variable, in CoveringSpace]
covering_space.X [variable, in CoveringSpace]
covering_space [section, in CoveringSpace]
Covers [projection, in OpenCover]
covers [section, in OpenCover]
CoverSets [projection, in OpenCover]
covers.T [variable, in OpenCover]
covers.X [variable, in OpenCover]
cover_open [definition, in OpenCover]


D

DecidableEqDep [module, in Eqdep_dec_one_variable]
DecidableEqDepSet [module, in Eqdep_dec_one_variable]
DecidableEqDepSet.eq_dep_eq [lemma, in Eqdep_dec_one_variable]
DecidableEqDepSet.eq_rect_eq [lemma, in Eqdep_dec_one_variable]
DecidableEqDepSet.inj_pairT2 [abbreviation, in Eqdep_dec_one_variable]
DecidableEqDepSet.inj_pair2 [lemma, in Eqdep_dec_one_variable]
DecidableEqDepSet.inj_pairP2 [lemma, in Eqdep_dec_one_variable]
DecidableEqDepSet.N [module, in Eqdep_dec_one_variable]
DecidableEqDepSet.Streicher_K [lemma, in Eqdep_dec_one_variable]
DecidableEqDepSet.UIP [lemma, in Eqdep_dec_one_variable]
DecidableEqDepSet.UIP_refl [lemma, in Eqdep_dec_one_variable]
DecidableEqDep.eq_dep_eq [lemma, in Eqdep_dec_one_variable]
DecidableEqDep.eq_rect_eq [lemma, in Eqdep_dec_one_variable]
DecidableEqDep.inj_pairP2 [lemma, in Eqdep_dec_one_variable]
DecidableEqDep.inj_pairT2 [lemma, in Eqdep_dec_one_variable]
DecidableEqDep.Streicher_K [lemma, in Eqdep_dec_one_variable]
DecidableEqDep.UIP [lemma, in Eqdep_dec_one_variable]
DecidableEqDep.UIP_refl [lemma, in Eqdep_dec_one_variable]
DecidableSet [module, in Eqdep_dec_one_variable]
DecidableSet.eq_dec [axiom, in Eqdep_dec_one_variable]
DecidableSet.U [axiom, in Eqdep_dec_one_variable]
DecidableSet.x [axiom, in Eqdep_dec_one_variable]
DecidableType [module, in Eqdep_dec_one_variable]
DecidableType.eq_dec [axiom, in Eqdep_dec_one_variable]
DecidableType.U [axiom, in Eqdep_dec_one_variable]
DecidableType.x [axiom, in Eqdep_dec_one_variable]
dec_rel [definition, in Orders]
DenoteExpression [definition, in Exercise_4_2_3_12]
Dependent_Equality.P [variable, in EqdepFacts_one_variable]
Dependent_Equality.U [variable, in EqdepFacts_one_variable]
Dependent_Equality [section, in EqdepFacts_one_variable]
description [section, in EquivalenceSet]
description [section, in EquivalenceClass]
description.constructive_definite_description [variable, in EquivalenceSet]
description.constructive_definite_description [variable, in EquivalenceClass]
description.eq_dec [variable, in EquivalenceSet]
description.T [variable, in EquivalenceSet]
description.T [variable, in EquivalenceClass]
destruct_path [lemma, in Exercise_4_1_2_28]
diagonal_functor_morphism_of [definition, in Exercise_4_3_1_10]
diagonal_functor_object_of [definition, in Exercise_4_3_1_10]
differentClasses [definition, in EquivalenceClass]
differentSets [definition, in EquivalenceSet]
disc [section, in DiscreteCategoryFunctors]
DiscreteAdjoints [section, in DiscreteCategoryFunctors]
DiscreteCategory [definition, in DiscreteCategory]
DiscreteCategory [section, in DiscreteCategory]
DiscreteCategory [library]
DiscreteCategoryFunctors [library]
DiscreteCategory_Identity [definition, in DiscreteCategory]
DiscreteCategory_Compose [definition, in DiscreteCategory]
DiscreteCategory.DiscreteCategory_Morphism [variable, in DiscreteCategory]
DiscreteCategory.O [variable, in DiscreteCategory]
DiscreteFunctor [definition, in DiscreteCategoryFunctors]
DiscreteGraph [definition, in Exercise_3_3_1_5]
DiscreteGraph [definition, in Exercise_5_1_1_6]
DiscreteGraphAdjunction [definition, in Exercise_5_1_1_6]
DiscreteGraphFunctor [definition, in Exercise_5_1_1_6]
DiscreteGraphInjection [definition, in Exercise_5_1_1_6]
DiscreteObjectIdentity [lemma, in DiscreteCategoryFunctors]
DiscreteSetFunctor [definition, in DiscreteCategoryFunctors]
DiscreteTopology [definition, in DiscreteTopology]
DiscreteTopology [library]
discrete_topology.X [variable, in DiscreteTopology]
discrete_topology [section, in DiscreteTopology]
disjointClasses [definition, in EquivalenceClass]
disjointClasses_differentClasses [lemma, in EquivalenceClass]
disjointSets [definition, in EquivalenceSet]
disjointSets_differentSets [lemma, in EquivalenceSet]
DisjointUnionIsUnion [projection, in Topology]
DisjointUnionSets [projection, in Topology]
DisjointUnionSetsDisjoint [projection, in Topology]
disjoint_union_in [lemma, in Topology]
disjoint_union.X [variable, in Topology]
disjoint_union [section, in Topology]
divides [definition, in NatOrders]
divides_dec [instance, in NatOrders]
divides_partial_order [instance, in NatOrders]
divides_antisym [instance, in NatOrders]
divides_pre_order [instance, in NatOrders]
divides_trans [instance, in NatOrders]
divides_refl [instance, in NatOrders]
Duals [library]


E

Edge [projection, in Graph]
EmptySetInitialOf [abbreviation, in SetCategoryFacts]
Empty_set_JMeqr [lemma, in Common]
Empty_set_JMeql [lemma, in Common]
Empty_set_eq [lemma, in Common]
EnsembleHasEnsembleJoins [instance, in EnsemblePreOrder]
EnsembleHasEnsembleMeets [instance, in EnsemblePreOrder]
EnsembleHasIndexedJoins [instance, in EnsemblePreOrder]
EnsembleHasIndexedMeets [instance, in EnsemblePreOrder]
EnsembleHasJoins [instance, in EnsemblePreOrder]
EnsembleHasMeets [instance, in EnsemblePreOrder]
EnsembleJoinElement [projection, in Orders]
EnsembleJoinOf [record, in Orders]
EnsembleMeetElement [projection, in Orders]
EnsembleMeetOf [record, in Orders]
EnsemblePreOrder [section, in EnsemblePreOrder]
EnsemblePreOrder [library]
EnsemblePreOrder.T [variable, in EnsemblePreOrder]
EnsemblesMeetsAndJoins [section, in Orders]
EnsemblesMeetsAndJoins.leq [variable, in Orders]
EnsemblesMeetsAndJoins.T [variable, in Orders]
EnsemblesMeetsAndJoins.U [variable, in Orders]
_ <= _ [notation, in Orders]
ensemble_join_is_join [projection, in Orders]
ensemble_meet_is_meet [projection, in Orders]
Ensemble_PreOrder [instance, in EnsemblePreOrder]
ensemble2sig [definition, in Topology]
EOpenSet [record, in Exercise_4_2_3_2]
EpiMono [section, in SetCategoryFacts]
EpiMono.S [variable, in SetCategoryFacts]
EpimorphismComposition [lemma, in CategoryMorphisms]
EpiSurj [lemma, in SetCategoryFacts]
EqdepDec [section, in Eqdep_dec_one_variable]
EqdepDec.A [variable, in Eqdep_dec_one_variable]
EqdepDec.comp [variable, in Eqdep_dec_one_variable]
EqdepDec.eq_dec [variable, in Eqdep_dec_one_variable]
EqdepDec.nu [variable, in Eqdep_dec_one_variable]
EqdepDec.nu_inv [variable, in Eqdep_dec_one_variable]
EqdepDec.nu_constant [variable, in Eqdep_dec_one_variable]
EqdepDec.proj [variable, in Eqdep_dec_one_variable]
EqdepDec.x [variable, in Eqdep_dec_one_variable]
EqdepElimination [module, in EqdepFacts_one_variable]
EqdepElimination.eq_rect_eq [axiom, in EqdepFacts_one_variable]
EqdepFacts_one_variable [library]
EqdepTheory [module, in EqdepFacts_one_variable]
EqdepTheory.Axioms [section, in EqdepFacts_one_variable]
EqdepTheory.Axioms.U [variable, in EqdepFacts_one_variable]
EqdepTheory.eq_dep_eq [lemma, in EqdepFacts_one_variable]
EqdepTheory.eq_rec_eq [lemma, in EqdepFacts_one_variable]
EqdepTheory.eq_rect_eq [lemma, in EqdepFacts_one_variable]
EqdepTheory.inj_pairT2 [abbreviation, in EqdepFacts_one_variable]
EqdepTheory.inj_pair2 [lemma, in EqdepFacts_one_variable]
EqdepTheory.Streicher_K [lemma, in EqdepFacts_one_variable]
EqdepTheory.UIP [lemma, in EqdepFacts_one_variable]
EqdepTheory.UIP_refl [lemma, in EqdepFacts_one_variable]
Eqdep_dec_one_variable [library]
equiv [section, in EquivalenceSet]
equiv [section, in EquivalenceClass]
Equivalence [record, in Isomorphism]
EquivalenceClass [record, in EquivalenceClass]
EquivalenceClass [section, in EquivalenceClass]
EquivalenceClass [library]
EquivalenceClass_eq_iso2 [lemma, in EquivalenceClass]
EquivalenceClass_eq_iso1 [lemma, in EquivalenceClass]
EquivalenceClass_eq_proj [definition, in EquivalenceClass]
EquivalenceClass_eq_lift [definition, in EquivalenceClass]
EquivalenceClass_forall__eq [lemma, in EquivalenceClass]
EquivalenceClass_forall_equiv__eq [lemma, in EquivalenceClass]
EquivalenceClass.equiv [variable, in EquivalenceClass]
EquivalenceClass.value [variable, in EquivalenceClass]
EquivalenceOf [inductive, in EquivalenceRelationGenerator]
EquivalenceOf_Equivalence [lemma, in EquivalenceRelationGenerator]
EquivalenceRelationGenerator [library]
Equivalences [section, in EqdepFacts_one_variable]
EquivalenceSet [record, in EquivalenceSet]
EquivalenceSet [section, in EquivalenceSet]
EquivalenceSet [library]
EquivalenceSet_eq_iso2 [lemma, in EquivalenceSet]
EquivalenceSet_eq_iso1 [lemma, in EquivalenceSet]
EquivalenceSet_eq_proj [definition, in EquivalenceSet]
EquivalenceSet_eq_lift [definition, in EquivalenceSet]
EquivalenceSet_forall__eq [lemma, in EquivalenceSet]
EquivalenceSet_forall_equiv__eq [lemma, in EquivalenceSet]
EquivalenceSet.equiv [variable, in EquivalenceSet]
EquivalenceSet.value [variable, in EquivalenceSet]
Equivalences.p [variable, in EqdepFacts_one_variable]
Equivalences.U [variable, in EqdepFacts_one_variable]
Equivalence_Transitive [projection, in Isomorphism]
Equivalence_Symmetric [projection, in Isomorphism]
Equivalence_Reflexive [projection, in Isomorphism]
equiv_eqex_eqdep [abbreviation, in EqdepFacts_one_variable]
equiv_helper [lemma, in Exercise_5_1_1_9]
equiv.equiv [variable, in EquivalenceSet]
equiv.equiv [variable, in EquivalenceClass]
equiv.equiv_dec [variable, in EquivalenceSet]
equiv.equiv_Equivalence [variable, in EquivalenceSet]
equiv.equiv_Equivalence [variable, in EquivalenceClass]
equiv.value [variable, in EquivalenceSet]
equiv.value [variable, in EquivalenceClass]
_ ~= _ [notation, in EquivalenceSet]
_ ~= _ [notation, in EquivalenceClass]
eq_sameSet [lemma, in EquivalenceSet]
eq_dep_eq_dec [lemma, in Eqdep_dec_one_variable]
eq_rect_eq_dec [lemma, in Eqdep_dec_one_variable]
eq_proofs_unicity [lemma, in Eqdep_dec_one_variable]
eq_dep_eq__inj_pairT2 [abbreviation, in EqdepFacts_one_variable]
eq_dep_eq__inj_pair2 [lemma, in EqdepFacts_one_variable]
eq_dep_eq__UIP [lemma, in EqdepFacts_one_variable]
eq_rect_eq__eq_dep_eq [lemma, in EqdepFacts_one_variable]
eq_rect_eq__eq_dep1_eq [lemma, in EqdepFacts_one_variable]
Eq_dep_eq [definition, in EqdepFacts_one_variable]
Eq_rect_eq [definition, in EqdepFacts_one_variable]
eq_sig_snd [lemma, in EqdepFacts_one_variable]
eq_sig_fst [lemma, in EqdepFacts_one_variable]
eq_sigT_snd [lemma, in EqdepFacts_one_variable]
eq_sigT_fst [lemma, in EqdepFacts_one_variable]
eq_sigT_sig_eq [lemma, in EqdepFacts_one_variable]
eq_sig_iff_eq_dep [lemma, in EqdepFacts_one_variable]
eq_dep_eq_sig [lemma, in EqdepFacts_one_variable]
eq_sig_eq_dep [lemma, in EqdepFacts_one_variable]
eq_sigT_iff_eq_dep [lemma, in EqdepFacts_one_variable]
eq_dep_eq_sigT [lemma, in EqdepFacts_one_variable]
eq_sigS_eq_dep [abbreviation, in EqdepFacts_one_variable]
eq_sigT_eq_dep [lemma, in EqdepFacts_one_variable]
eq_dep_dep1 [lemma, in EqdepFacts_one_variable]
eq_dep1_dep [lemma, in EqdepFacts_one_variable]
eq_dep1_intro [constructor, in EqdepFacts_one_variable]
eq_dep1 [inductive, in EqdepFacts_one_variable]
eq_indd [definition, in EqdepFacts_one_variable]
eq_dep_trans [lemma, in EqdepFacts_one_variable]
eq_dep_sym [lemma, in EqdepFacts_one_variable]
eq_dep_refl [lemma, in EqdepFacts_one_variable]
eq_dep_intro [constructor, in EqdepFacts_one_variable]
eq_dep [inductive, in EqdepFacts_one_variable]
eq_JMeq [lemma, in FEqualDep]
eq_pre_order [instance, in Orders]
eq_trans_id [lemma, in Exercise_4_2_3_12]
eq_sameClass [lemma, in EquivalenceClass]
Exercise_4_1_2_28 [section, in Exercise_4_1_2_28]
Exercise_4_1_2_29 [section, in Exercise_4_1_2_29]
Exercise_4_1_2_30 [section, in Exercise_4_1_2_30]
Exercise_4_1_2_31.Hom_C_v_x_two_elements [lemma, in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom_C_x_v_empty [lemma, in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom [variable, in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom_C_v_x_only_helper [lemma, in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom_C_x_v_empty_helper [lemma, in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom_C_x_v [definition, in Exercise_4_1_2_31]
Exercise_4_1_2_31.hf [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.gf [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom_C_v_x [inductive, in Exercise_4_1_2_31]
Exercise_4_1_2_31.C [definition, in Exercise_4_1_2_31]
Exercise_4_1_2_31.G [definition, in Exercise_4_1_2_31]
Exercise_4_1_2_31.k [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.j [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.i [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.h [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.g [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.f [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.A [inductive, in Exercise_4_1_2_31]
Exercise_4_1_2_31.z [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.y [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.x [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.w [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.v [constructor, in Exercise_4_1_2_31]
Exercise_4_1_2_31.V [inductive, in Exercise_4_1_2_31]
Exercise_4_1_2_31 [module, in Exercise_4_1_2_31]
Exercise_4_1_2_33.D_2 [variable, in Exercise_4_1_2_33]
Exercise_4_1_2_33.D_3 [variable, in Exercise_4_1_2_33]
Exercise_4_1_2_33 [section, in Exercise_4_1_2_33]
Exercise_4_1_2_34.C [variable, in Exercise_4_1_2_34]
Exercise_4_1_2_34.obj [variable, in Exercise_4_1_2_34]
Exercise_4_1_2_34 [section, in Exercise_4_1_2_34]
Exercise_4_1_2_35.Sets [variable, in Exercise_4_1_2_35]
Exercise_4_1_2_35.Cat [variable, in Exercise_4_1_2_35]
Exercise_4_1_2_35 [section, in Exercise_4_1_2_35]
Exercise_4_3_1_3.F [variable, in Exercise_4_3_1_3]
Exercise_4_3_1_3 [section, in Exercise_4_3_1_3]
Exercise_3_2_1_11.X [variable, in Exercise_3_2_1_11]
Exercise_3_2_1_11.Σ [variable, in Exercise_3_2_1_11]
Exercise_3_2_1_11 [section, in Exercise_3_2_1_11]
Exercise_3_2_1_14 [section, in Exercise_3_2_1_14]
Exercise_4_3_1_9 [section, in Exercise_4_3_1_9]
Exercise_3_3_1_5.V [variable, in Exercise_3_3_1_5]
Exercise_3_3_1_5 [section, in Exercise_3_3_1_5]
Exercise_3_3_1_9 [definition, in Exercise_3_3_1_9]
_ = _ (nat_scope) [notation, in Exercise_3_3_1_9]
Exercise_3_3_1_9' [definition, in Exercise_3_3_1_9]
Exercise_3_3_1_9 [section, in Exercise_3_3_1_9]
Exercise_5_3_2_3 [module, in Exercise_5_3_2_3]
Exercise_5_3_2_5.ExceptionMonad [definition, in Exercise_5_3_2_5]
Exercise_5_3_2_5.µ [variable, in Exercise_5_3_2_5]
Exercise_5_3_2_5.η [variable, in Exercise_5_3_2_5]
Exercise_5_3_2_5.T [definition, in Exercise_5_3_2_5]
Exercise_5_3_2_5.E [axiom, in Exercise_5_3_2_5]
Exercise_5_3_2_5 [module, in Exercise_5_3_2_5]
Exercise_3_3_1_10 [section, in Exercise_3_3_1_10]
_ ~~> _ [notation, in Exercise_4_4_1_1]
_ ~> _ [notation, in Exercise_4_4_1_1]
Paths_f _ [notation, in Exercise_4_4_1_1]
Exercise_4_4_1_1.part_b.m [variable, in Exercise_4_4_1_1]
Exercise_4_4_1_1.part_b.n [variable, in Exercise_4_4_1_1]
[] [notation, in Exercise_4_4_1_1]
[ _ , .. , _ ] [notation, in Exercise_4_4_1_1]
Exercise_4_4_1_1.part_b [section, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path5 [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path4 [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path3 [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path2 [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path1 [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path0 [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2 [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Exercise_4_4_1_1_a_edges [lemma, in Exercise_4_4_1_1]
Exercise_4_4_1_1.f' [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.nth_edge_in_loop_injective [lemma, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Exercise_4_4_1_1_a_vert [lemma, in Exercise_4_4_1_1]
Exercise_4_4_1_1.f [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.nth_edge_in_loop [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.LinearOrder2Graph [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1.One_Two [constructor, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Zero_One [constructor, in Exercise_4_4_1_1]
Exercise_4_4_1_1.LinearOrder2Graph_Edge [inductive, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Two [constructor, in Exercise_4_4_1_1]
Exercise_4_4_1_1.One [constructor, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Zero [constructor, in Exercise_4_4_1_1]
Exercise_4_4_1_1.LinearOrder2Graph_Vertex [inductive, in Exercise_4_4_1_1]
Exercise_4_4_1_1.Loop [definition, in Exercise_4_4_1_1]
Exercise_4_4_1_1 [module, in Exercise_4_4_1_1]
Exercise_4_4_1_5.b_schema_morphism_all [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_schema_morphsim_on_paths [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_schema_morphism_all_template' [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_2_0_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_2_1_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_0_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_2_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_2_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_1_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_2_2_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_1_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_0_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism5 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism4 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism3 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism2 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism1 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_2 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_2 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_1 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_2_2 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_1 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices8 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices7 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices6 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices5 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices4 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices3 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices2 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices1 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.part_b [section, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_schema_morphism_all [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_schema_morphsim_on_paths [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_schema_morphism_all_template [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_c_a_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_c_b_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_a_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_c_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_c_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_b_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_c_c_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_b_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_a_only [lemma, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism7 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism6 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism5 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism4 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism3 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism2 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism1 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_c_1 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_c_0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_c_0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_b_0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_c_c_0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_b_0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_a_0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices8 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices7 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices6 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices5 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices4 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices3 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices2 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices1 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices0 [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.part_a [section, in Exercise_4_4_1_5]
Exercise_4_4_1_5.SchemaMorphism_template' [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.SchemaMorphism_template [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.LinearOrder2Schema [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.One_Two [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Zero_One [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.LinearOrder2Schema_Edge [inductive, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Two [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.One [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.Zero [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.LinearOrder2Schema_Vertex [inductive, in Exercise_4_4_1_5]
Exercise_4_4_1_5.C [definition, in Exercise_4_4_1_5]
Exercise_4_4_1_5.i [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.h [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.g [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.C_Edge [inductive, in Exercise_4_4_1_5]
Exercise_4_4_1_5.c [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.b [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.a [constructor, in Exercise_4_4_1_5]
Exercise_4_4_1_5.C_Vertex [inductive, in Exercise_4_4_1_5]
Exercise_4_4_1_5 [module, in Exercise_4_4_1_5]
Exercise_4_4_1_6.L0_to_singleton_to_L0_id [lemma, in Exercise_4_4_1_6]
Exercise_4_4_1_6.singleton_to_L0_to_singleton_id [lemma, in Exercise_4_4_1_6]
Exercise_4_4_1_6.singleton_to_L0 [definition, in Exercise_4_4_1_6]
Exercise_4_4_1_6.L0_to_singleton [definition, in Exercise_4_4_1_6]
Exercise_4_4_1_6.SingletonSchema [definition, in Exercise_4_4_1_6]
Exercise_4_4_1_6.L [definition, in Exercise_4_4_1_6]
_ ≃_ _ _ [notation, in Exercise_4_4_1_6]
Exercise_4_4_1_6.Loop_Equiv [definition, in Exercise_4_4_1_6]
Exercise_4_4_1_6.count_edges_concatenate [lemma, in Exercise_4_4_1_6]
Exercise_4_4_1_6.count_edges_prepend [lemma, in Exercise_4_4_1_6]
Exercise_4_4_1_6.count_edges [definition, in Exercise_4_4_1_6]
Exercise_4_4_1_6.f [constructor, in Exercise_4_4_1_6]
Exercise_4_4_1_6.Loop_Edge [inductive, in Exercise_4_4_1_6]
Exercise_4_4_1_6.s [constructor, in Exercise_4_4_1_6]
Exercise_4_4_1_6.Loop_Vertex [inductive, in Exercise_4_4_1_6]
Exercise_4_4_1_6 [module, in Exercise_4_4_1_6]
Exercise_4_4_1_7 [module, in Exercise_4_4_1_7]
Exercise_4_6_4_3 [lemma, in Exercise_4_6_4_3]
Exercise_4_6_4_3_G [definition, in Exercise_4_6_4_3]
Exercise_4_6_4_3_G_MorphismOf [definition, in Exercise_4_6_4_3]
Exercise_4_6_4_3.G_ObjectOf [variable, in Exercise_4_6_4_3]
Exercise_4_6_4_3_F [definition, in Exercise_4_6_4_3]
Exercise_4_6_4_3_F_MorphismOf [definition, in Exercise_4_6_4_3]
Exercise_4_6_4_3.c' [variable, in Exercise_4_6_4_3]
Exercise_4_6_4_3.c [variable, in Exercise_4_6_4_3]
Exercise_4_6_4_3 [section, in Exercise_4_6_4_3]
Exercise_4_5_1_14_only [lemma, in Exercise_4_5_1_14]
Exercise_4_5_1_14_ex [definition, in Exercise_4_5_1_14]
Exercise_4_5_1_14.X' [variable, in Exercise_4_5_1_14]
Exercise_4_5_1_14.X [variable, in Exercise_4_5_1_14]
Exercise_4_5_1_14 [section, in Exercise_4_5_1_14]
_ ≤ _ [notation, in Exercise_4_5_1_16]
Exercise_4_5_1_16 [section, in Exercise_4_5_1_16]
Exercise_4_5_1_28_only [lemma, in Exercise_4_5_1_28]
Exercise_4_5_1_28_ex [definition, in Exercise_4_5_1_28]
Exercise_4_5_1_28.X' [variable, in Exercise_4_5_1_28]
Exercise_4_5_1_28.X [variable, in Exercise_4_5_1_28]
Exercise_4_5_1_28 [section, in Exercise_4_5_1_28]
Exercise_4_3_2_5.FunCSet [variable, in Exercise_4_3_2_5]
Exercise_4_3_2_5.C [variable, in Exercise_4_3_2_5]
Exercise_4_3_2_5 [section, in Exercise_4_3_2_5]
Exercise_5_1_4_4.CategoryLeafTable [definition, in Exercise_5_1_4_4]
Exercise_5_1_4_4.CategoryLeafTable.Hom [variable, in Exercise_5_1_4_4]
Exercise_5_1_4_4.CategoryLeafTable.Ob [variable, in Exercise_5_1_4_4]
Exercise_5_1_4_4.CategoryLeafTable [section, in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable [definition, in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.tgt [variable, in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.src [variable, in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.A [variable, in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.V [variable, in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.G [variable, in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable [section, in Exercise_5_1_4_4]
Exercise_5_1_4_4 [module, in Exercise_5_1_4_4]
Exercise_5_1_4_5 [module, in Exercise_5_1_4_5]
Exercise_5_1_4_9 [module, in Exercise_5_1_4_9]
Exercise_3_4_1_2_right_relation_not_transitive [definition, in Exercise_3_4_1_2]
Exercise_3_4_1_2_middle_relation_not_reflexive [definition, in Exercise_3_4_1_2]
Exercise_3_4_1_2_left_relation_linear_order [definition, in Exercise_3_4_1_2]
Exercise_3_4_1_2_right_relation [definition, in Exercise_3_4_1_2]
Exercise_3_4_1_2_middle_relation [definition, in Exercise_3_4_1_2]
Exercise_3_4_1_2_left_relation [definition, in Exercise_3_4_1_2]
| _ - _ | [notation, in Exercise_3_4_1_2]
Exercise_3_4_1_2 [section, in Exercise_3_4_1_2]
Exercise_3_4_1_7_R'_not_antisymmetric [definition, in Exercise_3_4_1_7]
Exercise_3_4_1_7_R_not_comparable [definition, in Exercise_3_4_1_7]
Exercise_3_4_1_7_R_partial_order [definition, in Exercise_3_4_1_7]
Exercise_3_4_1_7_R'_preorder [definition, in Exercise_3_4_1_7]
Exercise_3_4_1_7_R_preorder [instance, in Exercise_3_4_1_7]
Exercise_3_4_1_7.R' [variable, in Exercise_3_4_1_7]
Exercise_3_4_1_7.R [variable, in Exercise_3_4_1_7]
Exercise_3_4_1_7.S [variable, in Exercise_3_4_1_7]
Exercise_3_4_1_7 [section, in Exercise_3_4_1_7]
Exercise_3_4_1_8_R4_preorder [definition, in Exercise_3_4_1_8]
Exercise_3_4_1_8_R3_preorder [definition, in Exercise_3_4_1_8]
Exercise_3_4_1_8_R2_preorder [definition, in Exercise_3_4_1_8]
Exercise_3_4_1_8_R1_preorder [definition, in Exercise_3_4_1_8]
Exercise_3_4_1_8_R4 [definition, in Exercise_3_4_1_8]
Exercise_3_4_1_8_R3 [definition, in Exercise_3_4_1_8]
Exercise_3_4_1_8_R2 [definition, in Exercise_3_4_1_8]
Exercise_3_4_1_8_R1 [definition, in Exercise_3_4_1_8]
Exercise_3_4_1_8.finite_set_relation [variable, in Exercise_3_4_1_8]
Exercise_3_4_1_8.finite_set [variable, in Exercise_3_4_1_8]
Exercise_3_4_1_8 [section, in Exercise_3_4_1_8]
Exercise_4_2_3_2_continuity_bad.f_not_preserve_open [lemma, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.continuous_function_continuous [definition, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.f [definition, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.ThreeTopology2 [definition, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.ThreeTopology1 [definition, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.C [constructor, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.B [constructor, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.A [constructor, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.Three [inductive, in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad [module, in Exercise_4_2_3_2]
Exercise_4_2_3_2 [section, in Exercise_4_2_3_2]
_ ≼ _ [notation, in Exercise_4_5_1_4]
_ ≤ _ [notation, in Exercise_4_5_1_4]
Exercise_4_5_1_4 [section, in Exercise_4_5_1_4]
Exercise_3_3_2_4_SingletonGraphIsMonoid [instance, in Exercise_3_3_2_4]
Exercise_3_3_2_4_SingletonGraphCMonoid [definition, in Exercise_3_3_2_4]
Exercise_3_3_2_4 [section, in Exercise_3_3_2_4]
Exercise_5_3_3_6.PowerSetMonadProducts [instance, in Exercise_5_3_3_6]
Exercise_5_3_3_6.PowerSumIsProductPower [instance, in Exercise_5_3_3_6]
Exercise_5_3_3_6.µ [variable, in Exercise_5_3_3_6]
Exercise_5_3_3_6.η [variable, in Exercise_5_3_3_6]
Exercise_5_3_3_6.T [variable, in Exercise_5_3_3_6]
Exercise_5_3_3_6 [module, in Exercise_5_3_3_6]
Exercise_5_3_3_7.PowerSetMonadCoproducts [instance, in Exercise_5_3_3_7]
Exercise_5_3_3_7.µ [variable, in Exercise_5_3_3_7]
Exercise_5_3_3_7.η [variable, in Exercise_5_3_3_7]
Exercise_5_3_3_7.T [variable, in Exercise_5_3_3_7]
Exercise_5_3_3_7 [module, in Exercise_5_3_3_7]
Exercise_4_2_3_12 [section, in Exercise_4_2_3_12]
Exercise_4_6_1_5.Exercise_4_2_4_4.MaximalRespectedLawOfFunctor [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.MaximalRespectedLawOfFunctor_MorphismOf [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.maximal_law [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.maximal_law.SetOfLawsAsProp [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.maximal_law.S [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.maximal_law [section, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOfFunctor [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOfFunctor_MorphismOf [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.SetsPreOrder [instance, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.JurisdictionPreOrder [instance, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOfAll [constructor, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOf [inductive, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOfPerson [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.SetOfLaws [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.LawAsProp [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.Law [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.Jurisdiction [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.Person [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4 [module, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLandFunctor [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.JurisdictionPreOrder [instance, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand_subset_flip [lemma, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand.V_LawsAsProp [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand.V_Laws [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand.V [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand [section, in Exercise_4_6_1_5]
_ ≤ _ [notation, in Exercise_4_6_1_5]
_ <= _ [notation, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawsOf [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.Jurisdiction [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawAsProp [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.Law [variable, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3 [module, in Exercise_4_6_1_5]
Exercise_4_6_1_5.PreOrderedSets [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.continuous_induced_functor [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.continuous_induced_functor_morphism_of [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.continuous_induced_functor_object_of [definition, in Exercise_4_6_1_5]
Exercise_4_6_1_5.opens_ordered_by_inclusion [instance, in Exercise_4_6_1_5]
Exercise_4_6_1_5.OpenSet_eq [lemma, in Exercise_4_6_1_5]
Exercise_4_6_1_5.OpenSetOpen [projection, in Exercise_4_6_1_5]
Exercise_4_6_1_5.OpenSetSet [projection, in Exercise_4_6_1_5]
Exercise_4_6_1_5.EOpenSet [record, in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_3_2 [section, in Exercise_4_6_1_5]
Exercise_4_6_1_5 [module, in Exercise_4_6_1_5]
_ ≤ _ [notation, in Exercise_3_4_2_7]
Exercise_3_4_2_7.le [variable, in Exercise_3_4_2_7]
Exercise_3_4_2_7.S [variable, in Exercise_3_4_2_7]
Exercise_3_4_2_7 [section, in Exercise_3_4_2_7]
Exercise_4_2_4_3.LawOfTheLandFunctor [definition, in Exercise_4_2_4_3]
Exercise_4_2_4_3.JurisdictionPreOrder [instance, in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand_subset_flip [lemma, in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand [definition, in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand.V_LawsAsProp [variable, in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand.V_Laws [variable, in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand.V [variable, in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand [section, in Exercise_4_2_4_3]
_ ≤ _ [notation, in Exercise_4_2_4_3]
_ <= _ [notation, in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawsOf [variable, in Exercise_4_2_4_3]
Exercise_4_2_4_3.Jurisdiction [variable, in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawAsProp [variable, in Exercise_4_2_4_3]
Exercise_4_2_4_3.Law [variable, in Exercise_4_2_4_3]
Exercise_4_2_4_3 [module, in Exercise_4_2_4_3]
Exercise_4_2_4_4.MaximalRespectedLawOfFunctor [definition, in Exercise_4_2_4_4]
Exercise_4_2_4_4.MaximalRespectedLawOfFunctor_MorphismOf [definition, in Exercise_4_2_4_4]
Exercise_4_2_4_4.maximal_law [definition, in Exercise_4_2_4_4]
Exercise_4_2_4_4.maximal_law.SetOfLawsAsProp [variable, in Exercise_4_2_4_4]
Exercise_4_2_4_4.maximal_law.S [variable, in Exercise_4_2_4_4]
Exercise_4_2_4_4.maximal_law [section, in Exercise_4_2_4_4]
Exercise_4_2_4_4.RespectedLawsOfFunctor [definition, in Exercise_4_2_4_4]
Exercise_4_2_4_4.RespectedLawsOfFunctor_MorphismOf [definition, in Exercise_4_2_4_4]
Exercise_4_2_4_4.SetsPreOrder [instance, in Exercise_4_2_4_4]
Exercise_4_2_4_4.JurisdictionPreOrder [instance, in Exercise_4_2_4_4]
Exercise_4_2_4_4.RespectedLawsOfAll [constructor, in Exercise_4_2_4_4]
Exercise_4_2_4_4.RespectedLawsOf [inductive, in Exercise_4_2_4_4]
Exercise_4_2_4_4.RespectedLawsOfPerson [variable, in Exercise_4_2_4_4]
Exercise_4_2_4_4.SetOfLaws [definition, in Exercise_4_2_4_4]
Exercise_4_2_4_4.LawAsProp [variable, in Exercise_4_2_4_4]
Exercise_4_2_4_4.Law [variable, in Exercise_4_2_4_4]
Exercise_4_2_4_4.Jurisdiction [definition, in Exercise_4_2_4_4]
Exercise_4_2_4_4.Person [variable, in Exercise_4_2_4_4]
Exercise_4_2_4_4 [module, in Exercise_4_2_4_4]
Exercise_4_5_2_3.diagram_triangle_iso [definition, in Exercise_4_5_2_3]
Exercise_4_5_2_3.C_obj_trunc [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.CommutativeTriangleOfDiagram [definition, in Exercise_4_5_2_3]
Exercise_4_5_2_3.triangle_commutes [lemma, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.h [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.g [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.f [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.c [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.b [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.a [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.c' [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.b' [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.a' [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_h [lemma, in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_g [lemma, in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_f [lemma, in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_c [lemma, in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_b [lemma, in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_a [lemma, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.CommutativeTriangleDiagram [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle [section, in Exercise_4_5_2_3]
Exercise_4_5_2_3.DiagramOfCommutativeTriangle [definition, in Exercise_4_5_2_3]
Exercise_4_5_2_3.CommutativeTriangleDiagram_MorphismOf [definition, in Exercise_4_5_2_3]
Exercise_4_5_2_3.CommutativeTriangleDiagram_ObjectOf [definition, in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.h [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.g [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.f [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.c [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.b [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.a [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.T [variable, in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram [section, in Exercise_4_5_2_3]
Exercise_4_5_2_3.nat_eq_dec [definition, in Exercise_4_5_2_3]
Exercise_4_5_2_3.TriangleCommutes [projection, in Exercise_4_5_2_3]
Exercise_4_5_2_3.h [projection, in Exercise_4_5_2_3]
Exercise_4_5_2_3.g [projection, in Exercise_4_5_2_3]
Exercise_4_5_2_3.f [projection, in Exercise_4_5_2_3]
Exercise_4_5_2_3.c [projection, in Exercise_4_5_2_3]
Exercise_4_5_2_3.b [projection, in Exercise_4_5_2_3]
Exercise_4_5_2_3.a [projection, in Exercise_4_5_2_3]
Exercise_4_5_2_3.CommutativeTriangle [record, in Exercise_4_5_2_3]
Exercise_4_5_2_3.C [axiom, in Exercise_4_5_2_3]
Exercise_4_5_2_3.objC [axiom, in Exercise_4_5_2_3]
Exercise_4_5_2_3 [module, in Exercise_4_5_2_3]
Exercise_4_5_2_5.FirstDiagram [definition, in Exercise_4_5_2_5]
Exercise_4_5_2_5.FirstDiagram_helper [definition, in Exercise_4_5_2_5]
Exercise_4_5_2_5.SecondDiagram [definition, in Exercise_4_5_2_5]
Exercise_4_5_2_5.SecondDiagram_MorphismOf_commut [lemma, in Exercise_4_5_2_5]
Exercise_4_5_2_5.SecondDiagram_MorphismOf [definition, in Exercise_4_5_2_5]
Exercise_4_5_2_5.SecondIndex [definition, in Exercise_4_5_2_5]
Exercise_4_5_2_5.FirstIndex [definition, in Exercise_4_5_2_5]
Exercise_4_5_2_5.NatGroup [definition, in Exercise_4_5_2_5]
Exercise_4_5_2_5.f [axiom, in Exercise_4_5_2_5]
Exercise_4_5_2_5.A [axiom, in Exercise_4_5_2_5]
Exercise_4_5_2_5.C [axiom, in Exercise_4_5_2_5]
Exercise_4_5_2_5.objC [axiom, in Exercise_4_5_2_5]
Exercise_4_5_2_5 [module, in Exercise_4_5_2_5]
Exercise_4_5_2_9.Exercise_4_5_2_9 [lemma, in Exercise_4_5_2_9]
Exercise_4_5_2_9.chain_to_C_functor [definition, in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_to_chain_functor [definition, in Exercise_4_5_2_9]
Exercise_4_5_2_9.chain_to_C_MorphismOf [lemma, in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_to_chain_MorphismOf [lemma, in Exercise_4_5_2_9]
Exercise_4_5_2_9.chain_to_C [definition, in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_to_chain [definition, in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_morphism_unicity [lemma, in Exercise_4_5_2_9]
Exercise_4_5_2_9.C [definition, in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_obj [definition, in Exercise_4_5_2_9]
Exercise_4_5_2_9 [module, in Exercise_4_5_2_9]
Exercise_5_1_1_3.β [variable, in Exercise_5_1_1_3]
Exercise_5_1_1_3.f [variable, in Exercise_5_1_1_3]
Exercise_5_1_1_3.M [variable, in Exercise_5_1_1_3]
Exercise_5_1_1_3.c [constructor, in Exercise_5_1_1_3]
Exercise_5_1_1_3.b [constructor, in Exercise_5_1_1_3]
Exercise_5_1_1_3.a [constructor, in Exercise_5_1_1_3]
Exercise_5_1_1_3.X [inductive, in Exercise_5_1_1_3]
Exercise_5_1_1_3 [module, in Exercise_5_1_1_3]
Exercise_4_5_2_12.Exercise_4_5_2_12 [lemma, in Exercise_4_5_2_12]
Exercise_4_5_2_12.sq_to_C_functor [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.C_to_sq_functor [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.sq_to_C_MorphismOf [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.C_to_sq_MorphismOf [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.sq_to_C [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.C_to_sq [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.mor_0_1 [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.obj_1 [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.obj_0 [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.pf_0_le_n [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.pf_1_le_1 [lemma, in Exercise_4_5_2_12]
Exercise_4_5_2_12.pf_0_le_1 [lemma, in Exercise_4_5_2_12]
Exercise_4_5_2_12.pf_0_le_0 [lemma, in Exercise_4_5_2_12]
Exercise_4_5_2_12.C [definition, in Exercise_4_5_2_12]
Exercise_4_5_2_12.B [constructor, in Exercise_4_5_2_12]
Exercise_4_5_2_12.A [constructor, in Exercise_4_5_2_12]
Exercise_4_5_2_12.Two [inductive, in Exercise_4_5_2_12]
Exercise_4_5_2_12 [module, in Exercise_4_5_2_12]
Exercise_5_1_1_6.indiscrete_adjunction [section, in Exercise_5_1_1_6]
Exercise_5_1_1_6.discrete_adjunction [section, in Exercise_5_1_1_6]
Exercise_5_1_1_6.uniform_functors [section, in Exercise_5_1_1_6]
Exercise_5_1_1_6.uniform.UniformGraphFunctor_MorphismOf [variable, in Exercise_5_1_1_6]
Exercise_5_1_1_6.uniform.edge_set [variable, in Exercise_5_1_1_6]
Exercise_5_1_1_6.uniform [section, in Exercise_5_1_1_6]
Exercise_5_1_1_6.underlying [section, in Exercise_5_1_1_6]
Exercise_5_1_1_6 [section, in Exercise_5_1_1_6]
Exercise_5_1_1_9 [definition, in Exercise_5_1_1_9]
Exercise_5_1_1_9_Counit [definition, in Exercise_5_1_1_9]
Exercise_5_1_1_9_Unit [definition, in Exercise_5_1_1_9]
Exercise_5_1_1_9.p [variable, in Exercise_5_1_1_9]
Exercise_5_1_1_9.Disc [variable, in Exercise_5_1_1_9]
Exercise_5_1_1_9 [section, in Exercise_5_1_1_9]
Exercise_4_1_1_13 [lemma, in Exercise_4_1_1_13]
Exercise_4_1_1_13.Grph [variable, in Exercise_4_1_1_13]
Exercise_4_1_1_13 [section, in Exercise_4_1_1_13]
Exercise_4_1_1_14 [lemma, in Exercise_4_1_1_14]
Exercise_4_1_1_14.Grph [variable, in Exercise_4_1_1_14]
Exercise_4_1_1_14 [section, in Exercise_4_1_1_14]
Exercise_3_5_2_4.Exercise_3_5_2_4_c [lemma, in Exercise_3_5_2_4]
Exercise_3_5_2_4.Exercise_3_5_2_4_a [lemma, in Exercise_3_5_2_4]
Exercise_3_5_2_4.Associativity [axiom, in Exercise_3_5_2_4]
Exercise_3_5_2_4.RightIdentity [axiom, in Exercise_3_5_2_4]
Exercise_3_5_2_4.LeftIdentity [axiom, in Exercise_3_5_2_4]
Exercise_3_5_2_4.Rule2 [axiom, in Exercise_3_5_2_4]
Exercise_3_5_2_4.Rule1 [axiom, in Exercise_3_5_2_4]
_ o _ [notation, in Exercise_3_5_2_4]
Exercise_3_5_2_4.name [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.secretary [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.worksIn [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.lastName [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.firstName [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.manager [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.compose [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.identity [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.Arrow [inductive, in Exercise_3_5_2_4]
Exercise_3_5_2_4.DepartmentNameString [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.LastNameString [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.FirstNameString [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.Department [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.Employee [constructor, in Exercise_3_5_2_4]
Exercise_3_5_2_4.Node [inductive, in Exercise_3_5_2_4]
_ ≃ _ [notation, in Exercise_3_5_2_4]
Exercise_3_5_2_4 [module, in Exercise_3_5_2_4]
Exercise_2_6_1_6 [definition, in Exercise_2_6_1_6]
Exercise_2_6_1_6.X [variable, in Exercise_2_6_1_6]
Exercise_2_6_1_6.I [variable, in Exercise_2_6_1_6]
Exercise_2_6_1_6 [section, in Exercise_2_6_1_6]
Exercise_4_6_2_4.RDF_bad [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_8 [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_7 [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_6 [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_5 [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_4 [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_3 [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_2 [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_1 [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Year_2013 [variable, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Build_RDF [abbreviation, in Exercise_4_6_2_4]
Exercise_4_6_2_4.P [definition, in Exercise_4_6_2_4]
[ _ ] [notation, in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.I [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Inst_MorphismOf [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Inst_MorphismOf_Gen [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Inst_ObjectOf [definition, in Exercise_4_6_2_4]
Exercise_4_6_2_4.C [definition, in Exercise_4_6_2_4]
_ ~~~> _ [notation, in Exercise_4_6_2_4]
_ ~~> _ [notation, in Exercise_4_6_2_4]
_ ~~> _ [notation, in Exercise_4_6_2_4]
Exercise_4_6_2_4.LastName [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.FirstName [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.hasDay [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.hasMonth [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.hasYear [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.actionDescription [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.performedBy [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.occuredOn [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.morC [inductive, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Month [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Day [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Year [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.String [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.PersonId [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.DateId [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.ActionId [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.objC [inductive, in Exercise_4_6_2_4]
Exercise_4_6_2_4.December [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.November [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.October [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.September [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.August [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.July [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.June [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.May [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.April [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.March [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.February [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.January [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.Months [inductive, in Exercise_4_6_2_4]
Exercise_4_6_2_4.A01 [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.ActionIds [inductive, in Exercise_4_6_2_4]
Exercise_4_6_2_4.P44 [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.PersonIds [inductive, in Exercise_4_6_2_4]
Exercise_4_6_2_4.D13114 [constructor, in Exercise_4_6_2_4]
Exercise_4_6_2_4.DateIds [inductive, in Exercise_4_6_2_4]
Exercise_4_6_2_4 [module, in Exercise_4_6_2_4]
Exercise_4_2_1_10 [module, in Exercise_4_2_1_10]
_ ≤ _ [notation, in Exercise_4_2_1_13]
Exercise_4_2_1_13 [section, in Exercise_4_2_1_13]
Exercise_4_2_1_14 [lemma, in Exercise_4_2_1_14]
_ ≤ _ [notation, in Exercise_4_2_1_14]
Exercise_4_2_1_14.C [variable, in Exercise_4_2_1_14]
Exercise_4_2_1_14 [section, in Exercise_4_2_1_14]
_ ≤ _ [notation, in Exercise_4_2_1_16]
Exercise_4_2_1_16.C [variable, in Exercise_4_2_1_16]
Exercise_4_2_1_16 [section, in Exercise_4_2_1_16]
Exercise_4_5_3_6_b [definition, in Exercise_4_5_3_6]
Exercise_4_5_3_6_a [definition, in Exercise_4_5_3_6]
Exercise_4_5_3_6.ℙX [variable, in Exercise_4_5_3_6]
Exercise_4_5_3_6.X [variable, in Exercise_4_5_3_6]
Exercise_4_5_3_6 [section, in Exercise_4_5_3_6]
Exercise_4_5_3_8_b [definition, in Exercise_4_5_3_8]
Exercise_4_5_3_8_a [definition, in Exercise_4_5_3_8]
Exercise_4_5_3_8.Grp [variable, in Exercise_4_5_3_8]
Exercise_4_5_3_8 [section, in Exercise_4_5_3_8]
Exercise_3_5_2_12 [section, in Exercise_3_5_2_12]
Exercise_3_5_2_13 [section, in Exercise_3_5_2_13]
Exercise_3_5_2_18 [section, in Exercise_3_5_2_18]
Exercise_4_3_1_10_NT [definition, in Exercise_4_3_1_10]
Exercise_4_3_1_10.f [variable, in Exercise_4_3_1_10]
Exercise_4_3_1_10.Y [variable, in Exercise_4_3_1_10]
Exercise_4_3_1_10.X [variable, in Exercise_4_3_1_10]
Exercise_4_3_1_10.DiagonalFunctor_parts [section, in Exercise_4_3_1_10]
Exercise_4_3_1_10 [section, in Exercise_4_3_1_10]
Exercise_3_2_1_7_is_group [instance, in Exercise_3_2_1_7]
Exercise_3_2_1_7_is_monoid [instance, in Exercise_3_2_1_7]
Exercise_3_2_1_7.S [variable, in Exercise_3_2_1_7]
Exercise_3_2_1_7 [section, in Exercise_3_2_1_7]
Exercise_3_2_1_8 [section, in Exercise_3_2_1_8]
Exercise_4_5_3_11_b [definition, in Exercise_4_5_3_11]
Exercise_4_5_3_11_a [definition, in Exercise_4_5_3_11]
Exercise_4_5_3_11.C [variable, in Exercise_4_5_3_11]
Exercise_4_5_3_11 [section, in Exercise_4_5_3_11]
Exercise_4_5_3_13_b [definition, in Exercise_4_5_3_13]
Exercise_4_5_3_13_a [definition, in Exercise_4_5_3_13]
Exercise_4_5_3_13.S [variable, in Exercise_4_5_3_13]
Exercise_4_5_3_13.K [variable, in Exercise_4_5_3_13]
Exercise_4_5_3_13 [section, in Exercise_4_5_3_13]
Exercise_4_1_2_21.F [variable, in Exercise_4_1_2_21]
Exercise_4_1_2_21 [section, in Exercise_4_1_2_21]
Exercise_4_3_2_5 [library]
Exercise_4_5_2_3 [library]
Exercise_4_5_2_5 [library]
Exercise_3_3_1_10 [library]
Exercise_5_3_2_3 [library]
Exercise_4_5_2_9 [library]
Exercise_5_3_2_5 [library]
Exercise_4_5_1_28 [library]
Exercise_4_2_3_2 [library]
Exercise_3_1_1_7 [library]
Exercise_3_3_1_5 [library]
Exercise_3_3_1_9 [library]
Exercise_4_1_1_5 [library]
Exercise_3_2_1_11 [library]
Exercise_4_3_1_3 [library]
Exercise_4_3_1_10 [library]
Exercise_4_1_1_6 [library]
Exercise_4_5_3_11 [library]
Exercise_3_2_1_14 [library]
Exercise_4_5_3_13 [library]
Exercise_4_5_1_4 [library]
Exercise_5_1_1_3 [library]
Exercise_4_3_1_9 [library]
Exercise_5_1_1_6 [library]
Exercise_3_5_2_12 [library]
Exercise_3_5_2_13 [library]
Exercise_5_1_1_9 [library]
Exercise_3_5_2_18 [library]
Exercise_3_4_2_7 [library]
Exercise_4_2_1_10 [library]
Exercise_5_1_4_4 [library]
Exercise_5_1_4_5 [library]
Exercise_4_2_1_13 [library]
Exercise_4_2_1_14 [library]
Exercise_4_2_1_16 [library]
Exercise_5_1_4_9 [library]
Exercise_4_6_2_4 [library]
Exercise_4_5_2_12 [library]
Exercise_4_1_2_21 [library]
Exercise_4_1_2_28 [library]
Exercise_2_6_1_5 [library]
Exercise_4_1_2_29 [library]
Exercise_2_6_1_6 [library]
Exercise_3_4_1_2 [library]
Exercise_4_1_1_13 [library]
Exercise_3_2_1_7 [library]
Exercise_4_1_1_14 [library]
Exercise_3_2_1_8 [library]
Exercise_3_4_1_7 [library]
Exercise_3_4_1_8 [library]
Exercise_4_4_1_1 [library]
Exercise_4_5_3_6 [library]
Exercise_4_1_2_30 [library]
Exercise_4_5_3_8 [library]
Exercise_4_1_2_31 [library]
Exercise_4_4_1_5 [library]
Exercise_4_4_1_6 [library]
Exercise_4_1_2_33 [library]
Exercise_5_3_3_6 [library]
Exercise_4_4_1_7 [library]
Exercise_4_1_2_34 [library]
Exercise_5_3_3_7 [library]
Exercise_4_6_1_5 [library]
Exercise_4_1_2_35 [library]
Exercise_4_5_1_14 [library]
Exercise_4_5_1_16 [library]
Exercise_4_2_4_3 [library]
Exercise_4_2_3_12 [library]
Exercise_3_3_2_4 [library]
Exercise_4_2_4_4 [library]
Exercise_3_5_2_4 [library]
Exercise_4_6_4_3 [library]
Expression [inductive, in Exercise_4_2_3_12]
ExtendedConstantGraph [definition, in Exercise_3_3_1_5]
E_4_1_2_28_Hom_v0_v1 [lemma, in Exercise_4_1_2_28]
E_4_1_2_28_Hom_v1_v0 [lemma, in Exercise_4_1_2_28]
E_4_1_2_28_Hom_v1_v1 [lemma, in Exercise_4_1_2_28]
E_4_1_2_28_Hom_v0_v0 [lemma, in Exercise_4_1_2_28]
E_4_1_2_28_Objects_G [lemma, in Exercise_4_1_2_28]
E_4_1_2_33_Functor_8 [definition, in Exercise_4_1_2_33]
E_4_1_2_33_Functor_7 [definition, in Exercise_4_1_2_33]
E_4_1_2_33_Functor_6 [definition, in Exercise_4_1_2_33]
E_4_1_2_33_Functor_5 [definition, in Exercise_4_1_2_33]
E_4_1_2_33_Functor_4 [definition, in Exercise_4_1_2_33]
E_4_1_2_33_Functor_3 [definition, in Exercise_4_1_2_33]
E_4_1_2_33_Functor_2 [definition, in Exercise_4_1_2_33]
E_4_1_2_33_Functor_1 [definition, in Exercise_4_1_2_33]


F

f [definition, in Exercise_3_1_1_7]
FalseInitialOf [abbreviation, in SetCategoryFacts]
False_JMeqr [lemma, in Common]
False_JMeql [lemma, in Common]
False_eq [lemma, in Common]
FCompositionOf [projection, in Functor]
FEqualDep [library]
fg_equal [lemma, in Common]
fg_equal_JMeq [lemma, in FEqualDep]
fiber_is_relation [lemma, in Exercise_2_6_1_5]
FIdentityOf [projection, in Functor]
FiniteIntersectionOpen [projection, in Topology]
FIsomorphismOf [definition, in Exercise_4_1_2_21]
forall_extensionality_dep_JMeq [lemma, in FEqualDep]
forall_extensionality_dep [lemma, in FEqualDep]
FreeArrowCategory [definition, in Exercise_4_1_2_28]
FreeMonoid [definition, in MonoidAdjunction]
FreeMonoidMorphism [definition, in MonoidAdjunction]
FreeMonoidOn [definition, in MonoidAdjunction]
fst_Functor [definition, in ProductCategory]
FullSubcategory [definition, in Subcategory]
FullSubcategoryInclusionFunctor [definition, in Subcategory]
FunCSet_Hom_Iso_Set [lemma, in Exercise_4_3_2_5]
FunCSet_Iso_Set [lemma, in Exercise_4_3_2_5]
functional_extensionality_dep_JMeq' [lemma, in FEqualDep]
functional_extensionality_dep_JMeq [lemma, in FEqualDep]
FunctionProduct [library]
function_prod [definition, in FunctionProduct]
function_prod [section, in FunctionProduct]
Functor [record, in Functor]
Functor [library]
FunctorCategory [definition, in FunctorCategory]
FunctorCategory [section, in FunctorCategory]
FunctorCategory [library]
FunctorComposition [section, in Functor]
FunctorCompositionLemmas [section, in Functor]
FunctorFromDiscrete [definition, in DiscreteCategoryFunctors]
FunctorFromDiscrete [section, in DiscreteCategoryFunctors]
FunctorFromDiscrete.FunctorFromDiscrete_MorphismOf [variable, in DiscreteCategoryFunctors]
FunctorFromDiscrete.O [variable, in DiscreteCategoryFunctors]
FunctorFromDiscrete.objOf [variable, in DiscreteCategoryFunctors]
FunctorFromInitial [definition, in InitialTerminalCategory]
FunctorFromTerminal [definition, in InitialTerminalCategory]
FunctorIsInverseOf [definition, in FunctorIsomorphisms]
FunctorIsInverseOf_sym [lemma, in FunctorIsomorphisms]
FunctorIsInverseOf1 [definition, in FunctorIsomorphisms]
FunctorIsInverseOf2 [definition, in FunctorIsomorphisms]
FunctorIsIsomorphism [definition, in FunctorIsomorphisms]
FunctorIsIsomorphism_FunctorIsmorphismOf [lemma, in FunctorIsomorphisms]
FunctorIsmorphismOf_FunctorIsIsomorphism [lemma, in FunctorIsomorphisms]
FunctorIsomorphism [section, in FunctorIsomorphisms]
FunctorIsomorphismOf [record, in FunctorIsomorphisms]
FunctorIsomorphismOf_Identity [definition, in FunctorIsomorphisms]
FunctorIsomorphisms [library]
FunctorIsomorphism.CategoriesIsomorphic [section, in FunctorIsomorphisms]
FunctorIsomorphism.FunctorIsInverseOf [section, in FunctorIsomorphisms]
FunctorIsomorphism.FunctorIsIsomorphism [section, in FunctorIsomorphisms]
FunctorIsomorphism.FunctorIsomorphismOf [section, in FunctorIsomorphisms]
FunctorIsomorphism.IsomorphismOfCategories [section, in FunctorIsomorphisms]
FunctorNaturalEquivalenceLemmas [section, in NaturalEquivalence]
FunctorNaturalEquivalenceRelation [section, in NaturalEquivalence]
FunctorProduct [definition, in ProductCategory]
FunctorProduct [section, in ProductCategory]
FunctorProductFunctorial [definition, in ProductCategory]
Functors [section, in Functor]
FunctorsNaturallyEquivalent [definition, in NaturalEquivalence]
functors_naturally_equivalent_trans [lemma, in NaturalEquivalence]
functors_naturally_equivalent_sym [lemma, in NaturalEquivalence]
functors_naturally_equivalent_refl [lemma, in NaturalEquivalence]
Functors_Equal [section, in Functor]
FunctorToIndiscrete [definition, in IndiscreteCategory]
FunctorToIndiscrete [section, in IndiscreteCategory]
FunctorToIndiscrete.O [variable, in IndiscreteCategory]
FunctorToIndiscrete.objOf [variable, in IndiscreteCategory]
FunctorToTerminal [definition, in Exercise_4_1_2_34]
FunctorToTerminal [definition, in InitialTerminalCategory]
FunctorToTerminalUnique [lemma, in Exercise_4_1_2_34]
Functor_Eq_by_JMeq [lemma, in Functor]
Functor_Eq [lemma, in Functor]
Functor_preserves_isomorphism.F [variable, in FunctorIsomorphisms]
Functor_preserves_isomorphism [section, in FunctorIsomorphisms]
f_equal_helper [lemma, in Common]
f_equal5_JMeq [lemma, in FEqualDep]
f_equal4_JMeq [lemma, in FEqualDep]
f_equal3_JMeq [lemma, in FEqualDep]
f_equal2_JMeq [lemma, in FEqualDep]
f_equal1_JMeq [lemma, in FEqualDep]
f_equal_JMeq [lemma, in FEqualDep]
f_type_equal [lemma, in FEqualDep]
f_equal_dep [section, in FEqualDep]


G

G [definition, in Exercise_4_1_2_28]
gcd_9_12 [definition, in Exercise_4_5_1_16]
gcd_is_product [instance, in Exercise_4_5_1_16]
gcd_n_m [instance, in Exercise_4_5_1_16]
gcd_n_m_flip [instance, in Exercise_4_5_1_16]
gcd_n_n [instance, in Exercise_4_5_1_16]
gcd_n_1 [instance, in Exercise_4_5_1_16]
gcd_1_n [instance, in Exercise_4_5_1_16]
gcd_n_0 [instance, in Exercise_4_5_1_16]
gcd_0_n [instance, in Exercise_4_5_1_16]
gcd_maximal [projection, in Exercise_4_5_1_16]
gcd_divides_second [projection, in Exercise_4_5_1_16]
gcd_divides_first [projection, in Exercise_4_5_1_16]
Gen [section, in EquivalenceRelationGenerator]
GeneralizedPathEquivalence [section, in Schema]
GeneralizedPathEquivalence.S [variable, in Schema]
GeneralizedPathsEquivalenceRelation [section, in Schema]
GeneralizedPathsEquivalenceRelation.S [variable, in Schema]
GeneralizedPathsEquivalent [inductive, in Schema]
GeneralizedPathsEquivalent_trans [lemma, in Schema]
GeneralizedPathsEquivalent_sym [lemma, in Schema]
GeneralizedPathsEquivalent_refl [lemma, in Schema]
GeneralizedPathsEquivalent_eq [lemma, in Schema]
GeneralizedPathsEquivalent_PathsEquivalent [lemma, in Schema]
generalized_fg_equal [lemma, in Common]
generateEquivalence [definition, in EquivalenceRelationGenerator]
gen_trans [constructor, in EquivalenceRelationGenerator]
gen_sym [constructor, in EquivalenceRelationGenerator]
gen_refl [constructor, in EquivalenceRelationGenerator]
gen_underlying [constructor, in EquivalenceRelationGenerator]
Gen.A [variable, in EquivalenceRelationGenerator]
Gen.equiv [variable, in EquivalenceRelationGenerator]
GPathsEquivalent [constructor, in Schema]
Graph [record, in Graph]
Graph [library]
GraphCategory [library]
GraphHomomorphism [record, in Graph]
GraphHomomorphismToGraph'Homomorphism [definition, in Graph]
GraphHomomorphism_Eq [lemma, in Graph]
GraphToGraph' [definition, in Graph]
graph_homomorphisms [section, in Graph]
graph_equivalence [section, in Graph]
Graph' [record, in Graph]
Graph'Homomorphism [record, in Graph]
Graph'HomomorphismToGraphHomomorphism [definition, in Graph]
Graph'Homomorphism_Eq [lemma, in Graph]
Graph'Source [projection, in Graph]
Graph'Target [projection, in Graph]
Graph'ToGraph [definition, in Graph]
graph'_homomorphisms [section, in Graph]
Grothendieck [section, in Grothendieck]
Grothendieck [library]
GrothendieckC [projection, in Grothendieck]
GrothendieckCompose [definition, in Grothendieck]
GrothendieckIdentity [definition, in Grothendieck]
GrothendieckPair [record, in Grothendieck]
GrothendieckPair_eta [lemma, in Grothendieck]
GrothendieckProjectionFunctor [definition, in Grothendieck]
GrothendieckX [projection, in Grothendieck]
Grothendieck.F [variable, in Grothendieck]
Group [record, in Group]
Group [library]
GroupCategory [library]
GroupHomomorphism [definition, in Group]
GroupIsMonoid [projection, in Group]
Groupoid [record, in Groupoid]
Groupoid [library]
GroupoidCategory [projection, in Groupoid]
GroupoidIsGroupoid [projection, in Groupoid]
GroupoidType [projection, in Groupoid]
group_inverse_is_inverse [projection, in Group]
group_inverse [projection, in Group]
group_monoid [projection, in Group]
G_e [constructor, in Exercise_4_1_2_28]
G_Edge [inductive, in Exercise_4_1_2_28]
G_v1 [constructor, in Exercise_4_1_2_28]
G_v0 [constructor, in Exercise_4_1_2_28]
G_Vertex [inductive, in Exercise_4_1_2_28]


H

hausdorff [definition, in Hausdorff]
hausdorff [section, in Hausdorff]
Hausdorff [library]
hausdorff.T [variable, in Hausdorff]
hausdorff.X [variable, in Hausdorff]
Hom [library]
HomAdjunction [record, in Adjoint]
HomAdjunctionOfCounit [definition, in Adjoint]
HomAdjunctionOfUnit [definition, in Adjoint]
HomAdjunctionOfUnitCounit [definition, in Adjoint]
HomAdjunction2Adjunction [definition, in Adjoint]
HomAdjunction2Adjunction_AMateOf [definition, in Adjoint]
homemorphism_open_to_open [lemma, in Homeomorphism]
Homeomophic [record, in Homeomorphism]
Homeomophic_Homeomorphism [projection, in Homeomorphism]
HomeomophismContinuous [projection, in Homeomorphism]
HomeomophismInverse [projection, in Homeomorphism]
HomeomophismInverseContinuous [projection, in Homeomorphism]
Homeomophism1 [projection, in Homeomorphism]
homeomorphic [section, in Homeomorphism]
homeomorphic.Tx [variable, in Homeomorphism]
homeomorphic.Ty [variable, in Homeomorphism]
homeomorphic.X [variable, in Homeomorphism]
homeomorphic.Y [variable, in Homeomorphism]
Homeomorphism [record, in Homeomorphism]
Homeomorphism [library]
HomeomorphismInverse1 [projection, in Homeomorphism]
HomeomorphismInverse2 [projection, in Homeomorphism]
HomFunctor [definition, in Hom]
HomFunctor [section, in Hom]
HomFunctor.COp [variable, in Hom]
HomFunctor.covariant_contravariant [section, in Hom]
HomomorphismFromZeroGroup [definition, in ZeroGroup]
HomomorphismFromZeroGroup_unique [lemma, in ZeroGroup]
HomomorphismToZeroGroup [definition, in ZeroGroup]
HomomorphismToZeroGroup_unique [lemma, in ZeroGroup]


I

id [projection, in Monoid]
Identity [projection, in Category]
IdentityFunctor [definition, in Functor]
IdentityFunctor [section, in Functor]
IdentityFunctorLemmas [section, in Functor]
IdentityIsEpimorphism [lemma, in CategoryMorphisms]
IdentityIsMonomorphism [lemma, in CategoryMorphisms]
IdentityNaturalEquivalence [lemma, in NaturalEquivalence]
IdentityNaturalEquivalence [section, in NaturalEquivalence]
IdentityNaturalEquivalence.F [variable, in NaturalEquivalence]
IdentityNaturalTransformation [definition, in NaturalTransformation]
IdentityNaturalTransformation [section, in NaturalTransformation]
IdentityNaturalTransformationF [section, in NaturalTransformation]
IdentityNaturalTransformationF.F [variable, in NaturalTransformation]
IdentityNaturalTransformationF.G [variable, in NaturalTransformation]
IdentityNaturalTransformation' [definition, in Exercise_4_3_1_3]
IdentityNaturalTransformation' [definition, in NaturalTransformation]
IdentityNaturalTransformation.FullIdentity [section, in NaturalTransformation]
IdentityNaturalTransformation.FullIdentity.F [variable, in NaturalTransformation]
IdentityNaturalTransformation.ProofFreeIdentity [section, in NaturalTransformation]
IdentityNaturalTransformation.ProofFreeIdentity.FMO [variable, in NaturalTransformation]
IdentityNaturalTransformation.ProofFreeIdentity.FOO [variable, in NaturalTransformation]
IdentitySchemaMorphism [definition, in SchemaMorphism]
IdentitySchemaMorphsims [section, in SchemaMorphism]
IdentitySchemaMorphsims.C [variable, in SchemaMorphism]
IdentitySchemaMorphsims.D [variable, in SchemaMorphism]
identity_composition_lemmas [section, in CategoryIsomorphisms]
identity_dep_refl [constructor, in FEqualDep]
identity_dep [inductive, in FEqualDep]
identity_relation_homomorphism [definition, in Orders]
identity_graph'_homomorphism [definition, in Graph]
identity_graph_homomorphism [definition, in Graph]
identity_monoid_homomorphism [definition, in Monoid]
identity_group_homomorphism [definition, in Group]
identity_is_continuous [definition, in TopologicalContinuity]
id_action [projection, in Monoid]
image [definition, in Morphism]
InClass [projection, in EquivalenceClass]
InClass_classOf_eq' [definition, in EquivalenceClass]
InClass_classOf.C_Equivalence [variable, in EquivalenceClass]
InClass_classOf_eq [lemma, in EquivalenceClass]
InClass_classOf.C [variable, in EquivalenceClass]
InClass_classOf.equiv [variable, in EquivalenceClass]
InClass_classOf.value [variable, in EquivalenceClass]
InClass_classOf [section, in EquivalenceClass]
Included_trans [instance, in Topology]
Included_refl [instance, in Topology]
include_subset [definition, in Topology]
inclusion [definition, in Topology]
inclusion [section, in Topology]
inclusion.T [variable, in Topology]
inclusion2 [section, in Topology]
inclusion2.E [variable, in Topology]
inclusion2.X [variable, in Topology]
inclusion3 [section, in Topology]
inclusion3.X [variable, in Topology]
IndexedCategoryOf [abbreviation, in SetCategory]
IndexedEmptySetInitialOf [abbreviation, in SetCategoryFacts]
IndexedFalseInitialOf [abbreviation, in SetCategoryFacts]
IndexedJoinElement [projection, in Orders]
IndexedJoinOf [record, in Orders]
IndexedMeetElement [projection, in Orders]
IndexedMeetOf [record, in Orders]
IndexedMeetsAndJoins [section, in Orders]
IndexedMeetsAndJoins.Index [variable, in Orders]
IndexedMeetsAndJoins.IndexToSet [variable, in Orders]
IndexedMeetsAndJoins.leq [variable, in Orders]
IndexedMeetsAndJoins.T [variable, in Orders]
_ <= _ [notation, in Orders]
IndexedTInitialOf [abbreviation, in SetCategoryFacts]
IndexedTrueTerminalOf [abbreviation, in SetCategoryFacts]
IndexedTTerminalOf [abbreviation, in SetCategoryFacts]
IndexedUnitTerminalOf [abbreviation, in SetCategoryFacts]
indexed_join_is_join [projection, in Orders]
indexed_meet_is_meet [projection, in Orders]
IndiscreteCategory [definition, in IndiscreteCategory]
IndiscreteCategory [section, in IndiscreteCategory]
IndiscreteCategory [library]
IndiscreteCategory.O [variable, in IndiscreteCategory]
IndiscreteGraph [definition, in Exercise_5_1_1_6]
IndiscreteGraphAdjunction [definition, in Exercise_5_1_1_6]
IndiscreteGraphFunctor [definition, in Exercise_5_1_1_6]
IndiscreteGraphSurjection [definition, in Exercise_5_1_1_6]
IndiscreteTopology [definition, in IndiscreteTopology]
IndiscreteTopology [library]
indiscrete_topology.X [variable, in IndiscreteTopology]
indiscrete_topology [section, in IndiscreteTopology]
InducedDiscreteFunctor [definition, in DiscreteCategoryFunctors]
InducedFunctor [section, in DiscreteCategoryFunctors]
InducedFunctor.f [variable, in DiscreteCategoryFunctors]
InducedFunctor.O [variable, in DiscreteCategoryFunctors]
InducedProductFstFunctor [definition, in ProductInducedFunctors]
InducedProductFstNaturalTransformation [definition, in ProductInducedFunctors]
InducedProductSndFunctor [definition, in ProductInducedFunctors]
InducedProductSndNaturalTransformation [definition, in ProductInducedFunctors]
InitialCategory [definition, in InitialTerminalCategory]
InitialObject [record, in CategoryObjects]
InitialObjectUnique [lemma, in CategoryObjects]
InitialObject_IsInitialObject [definition, in CategoryObjects]
InitialObject_Object [definition, in CategoryObjects]
InitialObject_Property [projection, in CategoryObjects]
InitialObject_Morphism [projection, in CategoryObjects]
InitialObject_Object' [projection, in CategoryObjects]
InitialTerminal [section, in InitialTerminalCategory]
InitialTerminal [section, in SetCategoryFacts]
InitialTerminalCategory [library]
InitialTerminalFunctors [section, in InitialTerminalCategory]
injective_projections_JMeq [lemma, in Common]
InjMono [lemma, in SetCategoryFacts]
inj_pair2_eq_dec [lemma, in Eqdep_dec_one_variable]
inj_right_pair [lemma, in Eqdep_dec_one_variable]
Inj_dep_pairT [abbreviation, in EqdepFacts_one_variable]
Inj_dep_pairS [abbreviation, in EqdepFacts_one_variable]
Inj_dep_pair [definition, in EqdepFacts_one_variable]
InSet_setOf_eq' [definition, in EquivalenceSet]
InSet_setOf.C_Equivalence [variable, in EquivalenceSet]
InSet_setOf_eq [lemma, in EquivalenceSet]
InSet_setOf.equiv_dec [variable, in EquivalenceSet]
InSet_setOf.C [variable, in EquivalenceSet]
InSet_setOf.equiv [variable, in EquivalenceSet]
InSet_setOf.value [variable, in EquivalenceSet]
InSet_setOf [section, in EquivalenceSet]
InSet' [projection, in EquivalenceSet]
interior [definition, in Interior]
interior [section, in Interior]
Interior [library]
interior_respect_subset [lemma, in Interior]
interior_open_same [lemma, in Interior]
interior_subset [lemma, in Interior]
interior_open [lemma, in Interior]
intersection [section, in Topology]
IntersectionAAA [lemma, in Topology]
IntersectionCover [definition, in CoveringSpace]
IntersectionCover_open [lemma, in CoveringSpace]
intersection_lemmas.X [variable, in Topology]
intersection_lemmas [section, in Topology]
intersection_arbitrary_union_commute [lemma, in Topology]
intersection_union_commute.C' [variable, in Topology]
intersection_union_commute.C [variable, in Topology]
intersection_union_commute.X [variable, in Topology]
intersection_union_commute [section, in Topology]
intersection_cover.C' [variable, in CoveringSpace]
intersection_cover.C [variable, in CoveringSpace]
intersection_cover.T [variable, in CoveringSpace]
intersection_cover.X [variable, in CoveringSpace]
intersection_cover [section, in CoveringSpace]
intersection.C [variable, in Topology]
intersection.C' [variable, in Topology]
intersection.X [variable, in Topology]
Inverse [projection, in CategoryIsomorphisms]
InverseFunctor [projection, in FunctorIsomorphisms]
InverseNaturalIsomorphism [definition, in NaturalEquivalence]
InverseNaturalIsomorphism_NT [definition, in NaturalEquivalence]
InverseOf [instance, in CategoryIsomorphisms]
InverseOfFunctor [definition, in FunctorIsomorphisms]
inverse_compose_commutes [definition, in Morphism]
inverse_image [definition, in Morphism]
inverse_map [definition, in Morphism]
inverse_of [definition, in Group]
IsCoveringSpace [record, in CoveringSpace]
IsDisjointUnion [record, in Topology]
IsEpimorphism [definition, in CategoryMorphisms]
IsGroup [record, in Group]
IsGroupHomomorphism [definition, in Group]
IsGroupoid [record, in Groupoid]
IsInitialObject [definition, in CategoryObjects]
IsInitialObject_InitialObject [definition, in CategoryObjects]
IsInitialObject' [definition, in CategoryObjects]
IsInverseOf [definition, in CategoryIsomorphisms]
IsInverseOf_sym [lemma, in CategoryIsomorphisms]
IsInverseOf1 [definition, in CategoryIsomorphisms]
IsInverseOf2 [definition, in CategoryIsomorphisms]
IsIsomorphism [definition, in CategoryIsomorphisms]
IsIsomorphism_IsomorphismOf [lemma, in CategoryIsomorphisms]
IsMonoid [record, in Monoid]
IsMonoidAction [record, in Monoid]
IsMonomorphism [definition, in CategoryMorphisms]
IsmorphismOfCategories_CategoriesIsomorphic [lemma, in FunctorIsomorphisms]
IsoImpliesId [record, in Exercise_4_2_1_13]
Isomorphic [definition, in CategoryIsomorphisms]
isomorphic [record, in Isomorphism]
Isomorphic_trans [lemma, in CategoryIsomorphisms]
Isomorphic_sym [lemma, in CategoryIsomorphisms]
Isomorphic_refl [lemma, in CategoryIsomorphisms]
Isomorphic_Isomorphism [lemma, in CategoryIsomorphisms]
isomorphic_transitive [definition, in Isomorphism]
isomorphic_symmetric [definition, in Isomorphism]
isomorphic_reflexive [definition, in Isomorphism]
isomorphic_relation [section, in Isomorphism]
isomorphic_eq [lemma, in Isomorphism]
isomorphic_is_isomorphism [projection, in Isomorphism]
isomorphic_morphism [projection, in Isomorphism]
Isomorphism [record, in CategoryIsomorphisms]
Isomorphism [library]
IsomorphismOf [record, in CategoryIsomorphisms]
IsomorphismOfCategories [record, in FunctorIsomorphisms]
IsomorphismOfCategories_Of [projection, in FunctorIsomorphisms]
IsomorphismOfCategories_Functor [projection, in FunctorIsomorphisms]
IsomorphismOf_Identity [instance, in CategoryIsomorphisms]
IsomorphismOf_sig [definition, in CategoryIsomorphisms]
IsomorphismOf_sig2 [definition, in CategoryIsomorphisms]
Isomorphism_Of [projection, in CategoryIsomorphisms]
Isomorphism_Morphism [projection, in CategoryIsomorphisms]
isomorphism_left_inverse [projection, in Isomorphism]
isomorphism_right_inverse [projection, in Isomorphism]
isomorphism_inverse [projection, in Isomorphism]
IsomrphismOf_IsIsomorphism [lemma, in CategoryIsomorphisms]
Isomrphism_Isomorphic [lemma, in CategoryIsomorphisms]
iso_is_mono [lemma, in CategoryIsomorphisms]
iso_is_epi [lemma, in CategoryIsomorphisms]
iso_implies_id [projection, in Exercise_4_2_1_13]
IsTerminalObject [definition, in CategoryObjects]
IsTerminalObject_TerminalObject [definition, in CategoryObjects]
IsTerminalObject' [definition, in CategoryObjects]
is_gcd [record, in Exercise_4_5_1_16]
is_unique [definition, in Common]
is_injective [definition, in Morphism]
is_ensemble_join [definition, in Orders]
is_ensemble_meet [definition, in Orders]
is_indexed_join [definition, in Orders]
is_indexed_meet [definition, in Orders]
is_join [definition, in Orders]
is_meet [definition, in Orders]
is_monoid_action [projection, in Monoid]
is_commutative [definition, in Monoid]
is_monoid [projection, in Monoid]
is_product [record, in Product]
is_coproduct [record, in Coproduct]
is_group [projection, in Group]
is_inverse_of [definition, in Group]
is_isomorphism [record, in Isomorphism]
is_groupoid [projection, in Groupoid]


J

JMeq_eqT [lemma, in FEqualDep]
JoinElement [projection, in Orders]
JoinOf [record, in Orders]
join_is_join [projection, in Orders]


K

Kleisli [section, in KleisliCategory]
KleisliCategory [definition, in KleisliCategory]
KleisliCategory [library]
KleisliCategoryCoproducts [library]
KleisliCategoryProducts [library]
KleisliCategory_has_is_products [instance, in KleisliCategoryProducts]
KleisliCategory_has_is_coproducts [instance, in KleisliCategoryCoproducts]
KleisliCoproducts [section, in KleisliCategoryCoproducts]
KleisliCoproducts.KT [variable, in KleisliCategoryCoproducts]
KleisliProducts [section, in KleisliCategoryProducts]
KleisliProducts.KT [variable, in KleisliCategoryProducts]
Kleisli.µ [variable, in KleisliCategory]
Kleisli.η [variable, in KleisliCategory]
K_dec_set [lemma, in Eqdep_dec_one_variable]
K_dec_type [lemma, in Eqdep_dec_one_variable]
K_dec [lemma, in Eqdep_dec_one_variable]


L

LeftCone [definition, in Cone]
LeftCone_FCompositionOf [lemma, in Cone]
LeftCone_FIdentityOf [lemma, in Cone]
LeftCone_MorphismOf [definition, in Cone]
LeftCone_Compose [definition, in Cone]
LeftCone_Identity [definition, in Cone]
LeftCone_Morphism [definition, in Cone]
LeftIdentity [projection, in Category]
LeftIdentityFunctor [lemma, in Functor]
LeftIdentityFunctorNaturalTransformation1 [definition, in NaturalTransformation]
LeftIdentityFunctorNaturalTransformation2 [definition, in NaturalTransformation]
LeftIdentityFunctorNE [lemma, in NaturalEquivalence]
LeftIdentityFunctorNT_Isomorphism [lemma, in NaturalTransformation]
LeftIdentityNaturalTransformation [lemma, in NaturalTransformation]
LeftIdentityNaturalTransformation' [lemma, in Exercise_4_3_1_3]
LeftIdentitySchemaMorphism [lemma, in SchemaMorphism]
LeftInverse [projection, in CategoryIsomorphisms]
LeftInverseFunctor [projection, in FunctorIsomorphisms]
left_cone_f_composition_of.G [variable, in Cone]
left_cone_f_composition_of.F [variable, in Cone]
left_cone_f_composition_of [section, in Cone]
left_cone_f_identity_of [section, in Cone]
left_cone_morphism_of.F [variable, in Cone]
left_cone_morphism_of [section, in Cone]
left_cone_category.obj [variable, in Cone]
left_cone_category [section, in Cone]
left_id [projection, in Monoid]
le_dec' [instance, in NatOrders]
le_linear_order' [instance, in NatOrders]
le_comp' [instance, in NatOrders]
le_partial_order' [instance, in NatOrders]
le_antisym' [instance, in NatOrders]
le_pre_order' [instance, in NatOrders]
le_trans' [instance, in NatOrders]
le_refl' [instance, in NatOrders]
le_trans [lemma, in NatFacts]
le_refl [lemma, in NatFacts]
le_rel [section, in NatFacts]
LiftConnectedFunctor [definition, in Exercise_5_1_1_9]
LiftConnectedFunctor_Functor [definition, in Exercise_5_1_1_9]
LiftMonoidFunction [definition, in MonoidAdjunction]
LinearOrder [record, in Orders]
LinearOrderCategory_is_LinearOrder [instance, in Exercise_4_2_1_16]
LinearOrder_Comparable [projection, in Orders]
LinearOrder_Transitive [projection, in Orders]
LinearOrder_Reflexive [projection, in Orders]
LinearOrder_op_is_LinearOrder [instance, in Exercise_3_4_2_7]
LinearOrder_is_LinearOrderCategory [instance, in Exercise_4_2_1_16]
ListFunctor [definition, in ListFunctor]
ListFunctor [section, in ListFunctor]
ListFunctor [library]
LocallySmallCategory [definition, in Category]


M

MeetElement [projection, in Orders]
MeetOf [record, in Orders]
meet_is_meet [projection, in Orders]
misc [section, in FEqualDep]
Monad [record, in Monad]
Monad [section, in Monad]
Monad [library]
MonadFunctor [projection, in Monad]
MonadFunctorDiagram1 [projection, in Monad]
MonadFunctorDiagram2 [projection, in Monad]
MonadFunctorDiagram3 [projection, in Monad]
MonadMultiplication [projection, in Monad]
MonadUnit [projection, in Monad]
Monoid [record, in Monoid]
Monoid [library]
MonoidAction [record, in Monoid]
MonoidAdjunction [section, in MonoidAdjunction]
MonoidAdjunction [library]
MonoidAdjunction.adjunction [section, in MonoidAdjunction]
MonoidAdjunction.free [section, in MonoidAdjunction]
MonoidAdjunction.underlying [section, in MonoidAdjunction]
MonoidCategory [library]
MonoidFreeUnderlyingAdjunction [definition, in MonoidAdjunction]
MonoidHomomorphism [record, in Monoid]
MonoidHomomorphism_Eq [lemma, in Monoid]
MonoidHomomorphism_CompositionLaw [projection, in Monoid]
MonoidHomomorphism_IdentityLaw [projection, in Monoid]
MonoidHomomorphism_Function [projection, in Monoid]
monoid_action [projection, in Monoid]
MonoInj [lemma, in SetCategoryFacts]
MonomorphismComposition [lemma, in CategoryMorphisms]
morphism [section, in Morphism]
Morphism [projection, in Category]
Morphism [library]
MorphismOf [projection, in Functor]
MorphismOf_IsomorphismOf [definition, in FunctorIsomorphisms]
morphism.inverse [section, in Morphism]
morphism.inverse_compose.g [variable, in Morphism]
morphism.inverse_compose.f [variable, in Morphism]
morphism.inverse_compose.Z [variable, in Morphism]
morphism.inverse_compose.Y [variable, in Morphism]
morphism.inverse_compose.X [variable, in Morphism]
morphism.inverse_compose [section, in Morphism]
morphism.inverse.X [variable, in Morphism]
morphism.inverse.Y [variable, in Morphism]
_ ⁻¹ (function_scope) [notation, in Morphism]
_ o _ [notation, in Morphism]
Multiply [constructor, in Exercise_4_2_3_12]


N

NatCategory [definition, in NatCategory]
NatCategory [library]
NatFacts [library]
NatOrders [library]
NatualNumbersMonoid [section, in NaturalNumbersMonoid]
NaturalEquivalence [section, in NaturalEquivalence]
NaturalEquivalence [library]
NaturalEquivalenceInverse [definition, in NaturalEquivalence]
NaturalEquivalenceInverse_NaturalEquivalence [lemma, in NaturalEquivalence]
NaturalEquivalenceOf [definition, in NaturalEquivalence]
NaturalEquivalenceOfCategories [definition, in NaturalEquivalence]
NaturalEquivalenceOfCategories [section, in NaturalEquivalence]
NaturalEquivalence_of_NaturalIsomorphism [definition, in NaturalEquivalence]
NaturalEquivalence.F [variable, in NaturalEquivalence]
NaturalEquivalence.G [variable, in NaturalEquivalence]
NaturalIsomorphism [record, in NaturalEquivalence]
NaturalIsomorphism [section, in NaturalEquivalence]
NaturalIsomorphismOfCategories [record, in NaturalEquivalence]
NaturalIsomorphismOfCategories [section, in NaturalEquivalence]
NaturalIsomorphismOfCategories_Isomorphism_D [projection, in NaturalEquivalence]
NaturalIsomorphismOfCategories_Isomorphism_C [projection, in NaturalEquivalence]
NaturalIsomorphismOfCategories_G [projection, in NaturalEquivalence]
NaturalIsomorphismOfCategories_F [projection, in NaturalEquivalence]
NaturalIsomorphism_of_NaturalEquivalence [definition, in NaturalEquivalence]
NaturalIsomorphism_Isomorphism [projection, in NaturalEquivalence]
NaturalIsomorphism_Transformation [projection, in NaturalEquivalence]
NaturalIsomorphism.Composition [section, in NaturalEquivalence]
NaturalIsomorphism.Composition.F [variable, in NaturalEquivalence]
NaturalIsomorphism.Composition.F' [variable, in NaturalEquivalence]
NaturalIsomorphism.Composition.F'' [variable, in NaturalEquivalence]
NaturalIsomorphism.Composition.G [variable, in NaturalEquivalence]
NaturalIsomorphism.Composition.G' [variable, in NaturalEquivalence]
NaturalIsomorphism.Inverse [section, in NaturalEquivalence]
NaturalIsomorphism.Inverse.F [variable, in NaturalEquivalence]
NaturalIsomorphism.Inverse.G [variable, in NaturalEquivalence]
NaturalIsomorphism.NaturalIsomorphism [section, in NaturalEquivalence]
NaturalIsomorphism.NaturalIsomorphism.F [variable, in NaturalEquivalence]
NaturalIsomorphism.NaturalIsomorphism.G [variable, in NaturalEquivalence]
NaturalNumbersMonoid [definition, in NaturalNumbersMonoid]
NaturalNumbersMonoid [library]
NaturalTransformation [record, in NaturalTransformation]
NaturalTransformation [section, in NaturalTransformation]
NaturalTransformation [library]
NaturalTransformationComposition [section, in NaturalTransformation]
NaturalTransformationComposition.F [variable, in NaturalTransformation]
NaturalTransformationComposition.F' [variable, in NaturalTransformation]
NaturalTransformationComposition.F'' [variable, in NaturalTransformation]
NaturalTransformationComposition.G [variable, in NaturalTransformation]
NaturalTransformationComposition.G' [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw [lemma, in NaturalTransformation]
NaturalTransformationExchangeLaw [section, in NaturalTransformation]
NaturalTransformationExchangeLaw.F [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.F' [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.G [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.G' [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.H [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.H' [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.T [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.T' [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.U [variable, in NaturalTransformation]
NaturalTransformationExchangeLaw.U' [variable, in NaturalTransformation]
NaturalTransformationInverse [section, in NaturalEquivalence]
NaturalTransformationInverse.F [variable, in NaturalEquivalence]
NaturalTransformationInverse.G [variable, in NaturalEquivalence]
NaturalTransformationInverse.T [variable, in NaturalEquivalence]
NaturalTransformations_Equal [section, in NaturalTransformation]
NaturalTransformation_Eq [lemma, in NaturalTransformation]
NaturalTransformation.F [variable, in NaturalTransformation]
NaturalTransformation.G [variable, in NaturalTransformation]
nat_le_div [section, in NatOrders]
nat_le_order [section, in NatOrders]
nat_le_proofs_unicity [lemma, in NatFacts]
Negate [constructor, in Exercise_4_2_3_12]
NIComposeF [definition, in NaturalEquivalence]
NIComposeT [definition, in NaturalEquivalence]
NoEdges [constructor, in Path]
NoEvar [definition, in Category]
Notations [library]
notDisjointClasses [definition, in EquivalenceClass]
notDisjointClasses_eq [lemma, in EquivalenceClass]
notDisjointClasses_sameClass [lemma, in EquivalenceClass]
notDisjointClasses' [definition, in EquivalenceClass]
notDisjointSets [definition, in EquivalenceSet]
notDisjointSets_eq [lemma, in EquivalenceSet]
notDisjointSets_sameSet [lemma, in EquivalenceSet]
notDisjointSets' [definition, in EquivalenceSet]
no_path' [lemma, in Exercise_4_1_2_28]
no_smaller_monoid [lemma, in Exercise_3_1_1_7]
NTAssociativity [section, in NaturalTransformation]
NTAssociativity.F [variable, in NaturalTransformation]
NTAssociativity.F0 [variable, in NaturalTransformation]
NTAssociativity.F1 [variable, in NaturalTransformation]
NTAssociativity.G [variable, in NaturalTransformation]
NTAssociativity.H [variable, in NaturalTransformation]
NTComposeF [definition, in NaturalTransformation]
NTComposeFIdentityNaturalTransformation [lemma, in NaturalTransformation]
NTComposeT [definition, in NaturalTransformation]
NTIdentityFunctor [section, in NaturalTransformation]
NTIdentityFunctor.left [section, in NaturalTransformation]
NTIdentityFunctor.left.F [variable, in NaturalTransformation]
NTIdentityFunctor.right [section, in NaturalTransformation]
NTIdentityFunctor.right.F [variable, in NaturalTransformation]
nu_left_inv [lemma, in Eqdep_dec_one_variable]


O

ObFunctor [definition, in Exercise_4_1_2_35]
Obj [section, in DiscreteCategoryFunctors]
ObjectFunctor [definition, in DiscreteCategoryFunctors]
ObjectFunctorTo [abbreviation, in DiscreteCategoryFunctors]
ObjectFunctorToProp [definition, in DiscreteCategoryFunctors]
ObjectFunctorToSet [definition, in DiscreteCategoryFunctors]
ObjectOf [projection, in Functor]
OmegaCategory [definition, in ChainCategory]
OnArrows' [projection, in Graph]
one [constructor, in Exercise_3_1_1_7]
OnEdges [projection, in Graph]
OneLeOne [lemma, in Exercise_4_1_2_28]
OneLtTwo [lemma, in Exercise_4_1_2_33]
one_path' [lemma, in Exercise_4_1_2_28]
OnVertices [projection, in Graph]
OnVertices' [projection, in Graph]
Open [projection, in Topology]
OpenCover [library]
OpenSetOpen [projection, in Exercise_4_2_3_2]
OpenSetSet [projection, in Exercise_4_2_3_2]
OpenSet_eq [lemma, in Exercise_4_2_3_2]
opens_ordered_by_inclusion [instance, in Exercise_4_2_3_2]
open_subcover_open [lemma, in OpenCover]
OppositeCategory [definition, in Duals]
OppositeCategory [section, in Duals]
OppositeFunctor [definition, in Duals]
OppositeFunctor [section, in Duals]
OppositeFunctor.COp [variable, in Duals]
OppositeFunctor.DOp [variable, in Duals]
OppositeFunctor.F [variable, in Duals]
opposite_relation [definition, in Orders]
OrderCoproduct [library]
OrderProduct [library]
Orders [library]
order_product [section, in OrderProduct]
or_is_coproduct [instance, in SetCategoryFacts]


P

PairwiseIntersection [inductive, in Topology]
PairwiseIntersection_intro [constructor, in Topology]
PartialOrderCategory_is_PartialOrder [instance, in Exercise_4_2_1_13]
PartialOrder_op_is_PartialOrder [instance, in Exercise_3_4_2_7]
PartialOrder_is_PartialOrderCategory [instance, in Exercise_4_2_1_13]
path [inductive, in Path]
path [section, in Path]
Path [library]
PathOf [projection, in SchemaMorphism]
PathsCategory [definition, in PathsCategory]
PathsCategory [section, in PathsCategory]
PathsCategory [library]
PathsCategory.E [variable, in PathsCategory]
PathsCategory.V [variable, in PathsCategory]
PathsEquivalent [projection, in Schema]
PathsEquivalent_Equivalence [projection, in Schema]
PathsFunctor [definition, in PathsFunctor]
PathsFunctor [section, in PathsFunctor]
PathsFunctor [library]
PathsFunctor.paths_functor.f [variable, in PathsFunctor]
PathsFunctor.paths_functor.G' [variable, in PathsFunctor]
PathsFunctor.paths_functor.G [variable, in PathsFunctor]
PathsFunctor.paths_functor [section, in PathsFunctor]
PathsHomomorphism [definition, in PathsFunctor]
PathsHomomorphism_on_edges [definition, in PathsFunctor]
PathsOf [definition, in Path]
path_unique [definition, in Schema]
path_Equivalence_Theorems.S [variable, in Schema]
path_Equivalence_Theorems [section, in Schema]
path_Theorems.E [variable, in Path]
path_Theorems.V [variable, in Path]
path_Theorems [section, in Path]
path.E [variable, in Path]
path.functionOf [variable, in Path]
path.typeOf [variable, in Path]
path.V [variable, in Path]
Pos [constructor, in Exercise_4_2_3_12]
PostCompose [projection, in Schema]
PostComposeFunctorsNE [lemma, in NaturalEquivalence]
PostComposeSchemaMorphismsEquivalent [lemma, in SchemaMorphism]
PostCompose' [lemma, in Schema]
post_compose_identity2 [lemma, in CategoryIsomorphisms]
post_compose_identity [lemma, in CategoryIsomorphisms]
post_concatenate_equivalent [lemma, in Schema]
PowerSetFunctor [definition, in PowerSetFunctor]
PowerSetFunctor [section, in PowerSetFunctor]
PowerSetFunctor [library]
PowerSetFunctorOp [definition, in PowerSetFunctor]
PowerSetMonad [definition, in PowerSetMonad]
PowerSetMonad [section, in PowerSetMonad]
PowerSetMonad [library]
PowerSetMonad.µ [variable, in PowerSetMonad]
PowerSetMonad.η [variable, in PowerSetMonad]
PreCompose [projection, in Schema]
PreComposeFunctorsNE [lemma, in NaturalEquivalence]
PreComposeSchemaMorphismsEquivalent [lemma, in SchemaMorphism]
PreCompose' [lemma, in Schema]
PreOrderCategory [definition, in PreOrderCategory]
PreOrderCategory [library]
PreOrderedSet [record, in PreOrderCategory]
PreOrderedSetPreOrder [projection, in PreOrderCategory]
PreOrderedSetRelation [projection, in PreOrderCategory]
PreOrderedSets [definition, in Exercise_4_2_3_2]
PreOrderedSetType [projection, in PreOrderCategory]
PreOrder_op_is_PreOrder [instance, in Exercise_3_4_2_7]
preorder_category.all_preorders [section, in PreOrderCategory]
_ ≤ _ [notation, in PreOrderCategory]
preorder_category.single_preorder [section, in PreOrderCategory]
preorder_category [section, in PreOrderCategory]
prepend [definition, in Path]
prepend_equivalent [lemma, in Schema]
pre_compose_identity2 [lemma, in CategoryIsomorphisms]
pre_compose_identity [lemma, in CategoryIsomorphisms]
pre_concatenate_equivalent [lemma, in Schema]
prodT_is_product [instance, in SetCategoryFacts]
product [definition, in SwapExercise]
product [record, in Product]
Product [library]
ProductCategory [definition, in ProductCategory]
ProductCategory [section, in ProductCategory]
ProductCategory [library]
ProductCategoryFunctors [section, in ProductCategory]
ProductInducedFunctors [section, in ProductInducedFunctors]
ProductInducedFunctors [library]
ProductInducedFunctors.F [variable, in ProductInducedFunctors]
ProductInducedNaturalTransformations [section, in ProductInducedFunctors]
ProductInducedNaturalTransformations.F [variable, in ProductInducedFunctors]
product_of [definition, in SwapExercise]
product_element [definition, in SwapExercise]
product_type [record, in SwapExercise]
product_is_product [projection, in Product]
product_element [projection, in Product]
product_map_unique [projection, in Product]
product_snd_commutes [projection, in Product]
product_fst_commutes [projection, in Product]
product_map [projection, in Product]
product_snd [projection, in Product]
product_fst [projection, in Product]
product_decidable [instance, in OrderProduct]
product_strict_order [instance, in OrderProduct]
product_partial_order [instance, in OrderProduct]
product_antisym [instance, in OrderProduct]
product_equiv [instance, in OrderProduct]
product_PER [instance, in OrderProduct]
product_pre_order [instance, in OrderProduct]
product_trans [instance, in OrderProduct]
product_asym [instance, in OrderProduct]
product_sym [instance, in OrderProduct]
product_irefl [instance, in OrderProduct]
product_refl [instance, in OrderProduct]
prodXY [projection, in SwapExercise]
prod_eta [lemma, in Common]
prod_is_product [instance, in SetCategoryFacts]
prod_map_unique [projection, in SwapExercise]
prod_snd_commutes [projection, in SwapExercise]
prod_fst_commutes [projection, in SwapExercise]
prod_map [projection, in SwapExercise]
prod_snd [projection, in SwapExercise]
prod_fst [projection, in SwapExercise]
projT3 [definition, in Common]
proj1_sig_mor_functor [definition, in Subcategory]
proj1_sig_obj_functor [definition, in Subcategory]
proj1_sig_functor [definition, in Subcategory]
proj3_sig [definition, in Common]
proof_irrelevance_JMeq [lemma, in Exercise_4_1_2_34]
proof_irrelevance_JMeq [lemma, in FEqualDep]
PropHasEnsembleJoins [instance, in PropPreOrder]
PropHasEnsembleMeets [instance, in PropPreOrder]
PropHasIndexedJoins [instance, in PropPreOrder]
PropHasIndexedMeets [instance, in PropPreOrder]
PropHasJoins [instance, in PropPreOrder]
PropHasMeets [instance, in PropPreOrder]
PropPreOrder [section, in PropPreOrder]
PropPreOrder [library]
Prop_PreOrder [instance, in PropPreOrder]


Q

Quant [constructor, in Common]


R

Reflexive [definition, in Isomorphism]
relation [abbreviation, in Isomorphism]
RelationDecidable [record, in Orders]
RelationDecidable [inductive, in Orders]
RelationHomomorphism [record, in Orders]
RelationHomomorphism_Eq [lemma, in Orders]
RelationHomomorphism_Respectful [projection, in Orders]
RelationHomomorphism_Function [projection, in Orders]
Relation_dec [projection, in Orders]
Relation_dec [constructor, in Orders]
relation_product [definition, in OrderProduct]
relation_coproduct [section, in OrderCoproduct]
relation_sum [definition, in OrderCoproduct]
restrict [definition, in Morphism]
restrict_range [definition, in Morphism]
restrict_domain [definition, in Morphism]
RightCone [definition, in Cone]
RightCone_FCompositionOf [lemma, in Cone]
RightCone_FIdentityOf [lemma, in Cone]
RightCone_MorphismOf [definition, in Cone]
RightCone_Compose [definition, in Cone]
RightCone_Identity [definition, in Cone]
RightCone_Morphism [definition, in Cone]
RightIdentity [projection, in Category]
RightIdentityFunctor [lemma, in Functor]
RightIdentityFunctorNaturalTransformation1 [definition, in NaturalTransformation]
RightIdentityFunctorNaturalTransformation2 [definition, in NaturalTransformation]
RightIdentityFunctorNE [lemma, in NaturalEquivalence]
RightIdentityFunctorNT_Isomorphism [lemma, in NaturalTransformation]
RightIdentityNaturalTransformation [lemma, in NaturalTransformation]
RightIdentityNaturalTransformation' [lemma, in Exercise_4_3_1_3]
RightIdentitySchemaMorphism [lemma, in SchemaMorphism]
RightInverse [projection, in CategoryIsomorphisms]
RightInverseFunctor [projection, in FunctorIsomorphisms]
right_cone_f_composition_of.G [variable, in Cone]
right_cone_f_composition_of.F [variable, in Cone]
right_cone_f_composition_of [section, in Cone]
right_cone_f_identity_of [section, in Cone]
right_cone_morphism_of.F [variable, in Cone]
right_cone_morphism_of [section, in Cone]
right_cone_category.obj [variable, in Cone]
right_cone_category [section, in Cone]
right_id [projection, in Monoid]


S

sameClass [definition, in EquivalenceClass]
sameClass_eq [lemma, in EquivalenceClass]
sameClass_trans [lemma, in EquivalenceClass]
sameClass_sym [lemma, in EquivalenceClass]
sameClass_refl [lemma, in EquivalenceClass]
sameSet [definition, in EquivalenceSet]
sameSet_eq [lemma, in EquivalenceSet]
sameSet_trans [lemma, in EquivalenceSet]
sameSet_sym [lemma, in EquivalenceSet]
sameSet_refl [lemma, in EquivalenceSet]
Same_relation [definition, in Orders]
Schema [section, in Schema]
Schema [record, in Schema]
Schema [library]
SchemaIdentityInverse [lemma, in Schema]
SchemaIdentityIsomorphism [lemma, in Schema]
SchemaIsomorphism [definition, in Schema]
SchemaIsomorphismComposition [lemma, in Schema]
SchemaIsomorphismEquivalenceRelation [section, in Schema]
SchemaIsomorphismEquivalenceRelation.C [variable, in Schema]
SchemaIsomorphismEquivalenceRelation.d [variable, in Schema]
SchemaIsomorphismEquivalenceRelation.d' [variable, in Schema]
SchemaIsomorphismEquivalenceRelation.s [variable, in Schema]
SchemaIsomorphism' [definition, in Schema]
SchemaIsomorphism2Isomorphism' [lemma, in Schema]
SchemaMorphism [record, in SchemaMorphism]
SchemaMorphism [library]
SchemaMorphismComposition [section, in SchemaMorphism]
SchemaMorphismCompositionLemmas [section, in SchemaMorphism]
SchemaMorphismCompositionLemmas.B [variable, in SchemaMorphism]
SchemaMorphismCompositionLemmas.C [variable, in SchemaMorphism]
SchemaMorphismCompositionLemmas.D [variable, in SchemaMorphism]
SchemaMorphismCompositionLemmas.E [variable, in SchemaMorphism]
SchemaMorphismComposition.B [variable, in SchemaMorphism]
SchemaMorphismComposition.C [variable, in SchemaMorphism]
SchemaMorphismComposition.D [variable, in SchemaMorphism]
SchemaMorphismComposition.E [variable, in SchemaMorphism]
SchemaMorphismsEquivalent [definition, in SchemaMorphism]
SchemaMorphismsEquivalent [section, in SchemaMorphism]
SchemaMorphismsEquivalent_trans [lemma, in SchemaMorphism]
SchemaMorphismsEquivalent_sym [lemma, in SchemaMorphism]
SchemaMorphismsEquivalent_refl [lemma, in SchemaMorphism]
SchemaMorphismsEquivalent_Relation.E [variable, in SchemaMorphism]
SchemaMorphismsEquivalent_Relation.D [variable, in SchemaMorphism]
SchemaMorphismsEquivalent_Relation.C [variable, in SchemaMorphism]
SchemaMorphismsEquivalent_Relation [section, in SchemaMorphism]
SchemaMorphismsEquivalent.C [variable, in SchemaMorphism]
SchemaMorphismsEquivalent.D [variable, in SchemaMorphism]
SchemaMorphismsEquivalent.F [variable, in SchemaMorphism]
SchemaMorphismsEquivalent.G [variable, in SchemaMorphism]
SchemaMorphisms_equivalent [lemma, in SchemaMorphism]
SchemaMorphisms_Equal [section, in SchemaMorphism]
SchemaMorphism_equal_parts [lemma, in SchemaMorphism]
SchemaMorphism_Eq [lemma, in SchemaMorphism]
Schemas [section, in SchemaMorphism]
Schemas.C [variable, in SchemaMorphism]
Schemas.D [variable, in SchemaMorphism]
Schemas.transferPath [section, in SchemaMorphism]
Schemas.transferPath.pathOf [variable, in SchemaMorphism]
Schemas.transferPath.vertexOf [variable, in SchemaMorphism]
Schema.C [variable, in Schema]
SEdge [projection, in Schema]
SEpimorphism [definition, in Schema]
SetCategory [library]
SetCategoryFacts [library]
SetContainsEquivalent [projection, in EquivalenceSet]
SetElementsEquivalent [projection, in EquivalenceSet]
SetEquivalent_trans [projection, in EquivalenceSet]
SetEquivalent_sym [projection, in EquivalenceSet]
SetEquivalent_refl [projection, in EquivalenceSet]
SetInhabited [projection, in EquivalenceSet]
setOf [definition, in EquivalenceSet]
setOf_eq [lemma, in EquivalenceSet]
setOf_refl [lemma, in EquivalenceSet]
SetUnderlyingGraphFunctor [definition, in Exercise_5_1_1_6]
set_cat_has_coprod [section, in SetCategoryFacts]
set_cat_has_prod [section, in SetCategoryFacts]
sig [section, in Common]
sigT_eta [lemma, in Common]
sigT_eq [lemma, in Common]
sigT_of_sigT2 [definition, in Common]
sigT2_eta [lemma, in Common]
sigT2_eq [lemma, in Common]
sig_eta [lemma, in Common]
sig_eq [lemma, in Common]
sig_of_sig2 [definition, in Common]
sig_JMeq [lemma, in FEqualDep]
sig_mor_compat [lemma, in Subcategory]
sig_mor_eq [lemma, in Subcategory]
sig_functor_mor_inv [definition, in Subcategory]
sig_functor_mor [definition, in Subcategory]
sig_mor.Pcompose [variable, in Subcategory]
sig_mor.Pidentity [variable, in Subcategory]
sig_mor.Pmor [variable, in Subcategory]
sig_mor [section, in Subcategory]
sig_obj_compat [lemma, in Subcategory]
sig_obj_eq [lemma, in Subcategory]
sig_functor_obj_inv [definition, in Subcategory]
sig_functor_obj [definition, in Subcategory]
sig_obj.Pobj [variable, in Subcategory]
sig_obj [section, in Subcategory]
sig_obj_mor.Pcompose [variable, in Subcategory]
sig_obj_mor.Pidentity [variable, in Subcategory]
sig_obj_mor.Pmor [variable, in Subcategory]
sig_obj_mor.Pobj [variable, in Subcategory]
sig_obj_mor [section, in Subcategory]
sig2_IsomorphismOf [instance, in CategoryIsomorphisms]
sig2_eta [lemma, in Common]
sig2_eq [lemma, in Common]
SingletonList [definition, in Exercise_4_3_1_9]
SingletonNaturalTransformation [definition, in Exercise_4_3_1_9]
SInverseOf [definition, in Schema]
SInverseOf_sym [lemma, in Schema]
SInverseOf1 [lemma, in Schema]
SInverseOf1' [lemma, in Schema]
SInverseOf2 [lemma, in Schema]
SliceCategory [definition, in CommaCategory]
SliceCategory [section, in CommaCategory]
SliceCategoryOver [definition, in CommaCategory]
SliceCategoryOver [section, in CommaCategory]
SliceCategoryOver.a [variable, in CommaCategory]
SliceCategory_Functor [definition, in CommaCategory]
SliceCategory.a [variable, in CommaCategory]
SliceCategory.B [variable, in CommaCategory]
SliceCategory.S [variable, in CommaCategory]
SmallCategory [definition, in Category]
smallest_monoid [definition, in Exercise_3_1_1_7]
SMonomorphism [definition, in Schema]
snd_Functor [definition, in ProductCategory]
SourceCommutes' [projection, in Graph]
SplitHom [lemma, in Hom]
SplitHomFunctor [section, in Hom]
SplitHomFunctor.COp [variable, in Hom]
SplitHom' [lemma, in Hom]
Streicher_K__eq_rect_eq [lemma, in EqdepFacts_one_variable]
Streicher_K_ [definition, in EqdepFacts_one_variable]
Subcategory [definition, in Subcategory]
Subcategory [library]
SubcategoryInclusionFunctor [definition, in Subcategory]
subcover [definition, in OpenCover]
subset_ensemble_union [lemma, in Topology]
subset_ensemble_intersection [lemma, in Topology]
subset_ensemble_union_intersection.U [variable, in Topology]
subset_ensemble_union_intersection.X [variable, in Topology]
subset_ensemble_union_intersection [section, in Topology]
subset_ensemble_iff2 [lemma, in Topology]
subset_ensemble_iff1 [lemma, in Topology]
subset_ensemble_included [lemma, in Topology]
subset_ensemble [definition, in Topology]
SubspaceTopology [instance, in SubspaceTopology]
SubspaceTopology [library]
subspace_topology.P [variable, in SubspaceTopology]
subspace_topology.T [variable, in SubspaceTopology]
subspace_topology.X [variable, in SubspaceTopology]
subspace_topology [section, in SubspaceTopology]
Subtract [constructor, in Exercise_4_2_3_12]
sumbool_to_bool [definition, in Common]
sumT_is_coproduct [instance, in SetCategoryFacts]
sum_is_coproduct [instance, in SetCategoryFacts]
sum_function [definition, in Morphism]
sum_strict_order [instance, in OrderCoproduct]
sum_partial_order [instance, in OrderCoproduct]
sum_antisym [instance, in OrderCoproduct]
sum_equiv [instance, in OrderCoproduct]
sum_PER [instance, in OrderCoproduct]
sum_pre_order [instance, in OrderCoproduct]
sum_trans [instance, in OrderCoproduct]
sum_asym [instance, in OrderCoproduct]
sum_sym [instance, in OrderCoproduct]
sum_irefl [instance, in OrderCoproduct]
sum_refl [instance, in OrderCoproduct]
SurjEpi [lemma, in SetCategoryFacts]
SVertex [projection, in Schema]
swap [definition, in SwapExercise]
swap [section, in SwapExercise]
SwapExercise [library]
swap_iso [definition, in SwapExercise]
swap_types_iso [definition, in SwapExercise]
swap_types [definition, in SwapExercise]
swap_product [definition, in Product]
swap_product [section, in Product]
swap_coproduct [definition, in Coproduct]
swap_coproduct [section, in Coproduct]
Symmetric [definition, in Isomorphism]
sym_iff [lemma, in EqdepFacts_one_variable]
sym_iff0 [lemma, in EqdepFacts_one_variable]
s_iso_is_mono [lemma, in Schema]
s_iso_is_epi [lemma, in Schema]


T

TargetCommutes' [projection, in Graph]
telescope [inductive, in Common]
telescope [section, in Common]
telescopeOut [definition, in Common]
telescopeOut' [definition, in Common]
TEquivalenceOf [projection, in SchemaMorphism]
TerminalCategory [definition, in InitialTerminalCategory]
TerminalObject [record, in CategoryObjects]
TerminalObjectUnique [lemma, in CategoryObjects]
TerminalObject_IsTerminalObject [definition, in CategoryObjects]
TerminalObject_Object [definition, in CategoryObjects]
TerminalObject_Property [projection, in CategoryObjects]
TerminalObject_Morphism [projection, in CategoryObjects]
TerminalObject_Object' [projection, in CategoryObjects]
three [inductive, in Exercise_3_1_1_7]
ThreeNotLtThree [lemma, in Exercise_4_1_2_33]
three_monoid [definition, in Exercise_3_1_1_7]
TopologicalContinuity [library]
Topology [record, in Topology]
topology [section, in Topology]
Topology [library]
TopologyCategory [library]
TopologyOfTotalTopology [projection, in TopologyCategory]
topology.X [variable, in Topology]
TotalTopology [record, in TopologyCategory]
transferPath [definition, in SchemaMorphism]
TransferPath_NoEdges [lemma, in SchemaMorphism]
Transitive [definition, in Isomorphism]
trans_sym_eq [lemma, in Eqdep_dec_one_variable]
True [section, in Common]
TrueTerminalOf [abbreviation, in SetCategoryFacts]
True_JMeq [lemma, in Common]
True_eq_eq [lemma, in Common]
True_eq_singleton [lemma, in Common]
True_eq [lemma, in Common]
True_singleton [lemma, in Common]
two [inductive, in Exercise_3_1_1_7]
twoa [constructor, in Exercise_3_1_1_7]
twob [constructor, in Exercise_3_1_1_7]
TwoNotLeOne [lemma, in Exercise_4_1_2_28]
two_monoid_is_commutative [lemma, in Exercise_3_1_1_7]
TypeOfTotalTopology [projection, in TopologyCategory]


U

UIP_refl_nat [lemma, in Eqdep_dec_one_variable]
UIP_refl_bool [lemma, in Eqdep_dec_one_variable]
UIP_refl_unit [lemma, in Eqdep_dec_one_variable]
UIP_dec [lemma, in Eqdep_dec_one_variable]
UIP_shift [lemma, in EqdepFacts_one_variable]
UIP_refl__Streicher_K [lemma, in EqdepFacts_one_variable]
UIP__UIP_refl [lemma, in EqdepFacts_one_variable]
UIP_refl_ [definition, in EqdepFacts_one_variable]
UIP_ [definition, in EqdepFacts_one_variable]
UnderlyingGraph [definition, in UnderlyingGraph]
UnderlyingGraph [library]
UnderlyingGraph' [definition, in UnderlyingGraph]
UnderlyingPoints [definition, in Exercise_4_2_3_2]
UnderlyingSetOfMonoid [definition, in MonoidAdjunction]
underlying_graph [section, in UnderlyingGraph]
UniformGraph [definition, in Exercise_5_1_1_6]
UniformGraphFunctor [definition, in Exercise_5_1_1_6]
UniformGraphInjection [definition, in Exercise_5_1_1_6]
UniformGraphSurjection [definition, in Exercise_5_1_1_6]
UniqueUpToUniqueIsomorphism [definition, in CategoryObjects]
UniqueUpToUniqueIsomorphism' [definition, in CategoryObjects]
unit [section, in Common]
UnitCounitOf [definition, in Adjoint]
UnitCounitOf_Helper2 [lemma, in Adjoint]
UnitCounitOf_Helper1 [lemma, in Adjoint]
UnitOf [definition, in Adjoint]
UnitTerminalOf [abbreviation, in SetCategoryFacts]
unit_JMeq [lemma, in Common]
unit_eq_eq [lemma, in Common]
unit_eq_singleton [lemma, in Common]
unit_eq [lemma, in Common]
unit_singleton [lemma, in Common]
univ_prod.Y [variable, in SwapExercise]
univ_prod.X [variable, in SwapExercise]
univ_prod [section, in SwapExercise]


V

Vertex [projection, in Graph]
VertexOf [projection, in SchemaMorphism]
Vertex' [projection, in Graph]


W

WideSubcategory [definition, in Subcategory]
WideSubcategoryInclusionFunctor [definition, in Subcategory]


Z

zeroa [constructor, in Exercise_3_1_1_7]
zerob [constructor, in Exercise_3_1_1_7]
ZeroComputationalGroup [definition, in ZeroGroup]
ZeroGroup [definition, in ZeroGroup]
ZeroGroup [library]
ZeroIsGroup [instance, in ZeroGroup]
ZeroIsMonoid [instance, in ZeroGroup]
ZeroLeOne [lemma, in Exercise_4_1_2_28]
ZeroLtTwo [lemma, in Exercise_4_1_2_33]
zero_group [section, in ZeroGroup]


other

_ ≅ _ (category_scope) [notation, in CategoryIsomorphisms]
_ ▻ (category_scope) [notation, in Cone]
_ ◅ (category_scope) [notation, in Cone]
_ ^ _ (category_scope) [notation, in FunctorCategory]
[ ω ] (category_scope) [notation, in ChainCategory]
[ ∞ ] (category_scope) [notation, in ChainCategory]
[ _ ] (category_scope) [notation, in ChainCategory]
_ ~> _ (category_scope) [notation, in Category]
_ * _ (category_scope) [notation, in ProductCategory]
_ ↓ _ (category_scope) [notation, in CommaCategory]
_ ⁻¹ (function_scope) [notation, in Morphism]
_ ⟨ - , _ ⟩ (functor_scope) [notation, in ProductInducedFunctors]
_ ⟨ _ , - ⟩ (functor_scope) [notation, in ProductInducedFunctors]
_ ▻ (functor_scope) [notation, in Cone]
_ ◅ (functor_scope) [notation, in Cone]
_ o _ (functor_scope) [notation, in Functor]
_ * _ (functor_scope) [notation, in ProductCategory]
π₂ (functor_scope) [notation, in ProductCategory]
π₁ (functor_scope) [notation, in ProductCategory]
_ ⁻¹ (morphism_scope) [notation, in CategoryIsomorphisms]
π₂ (morphism_scope) [notation, in Product]
π₁ (morphism_scope) [notation, in Product]
i₂ (morphism_scope) [notation, in Coproduct]
i₁ (morphism_scope) [notation, in Coproduct]
_ o _ (morphism_scope) [notation, in Category]
_ ⟨ - , _ ⟩ (natural_transformation_scope) [notation, in ProductInducedFunctors]
_ ⟨ _ , - ⟩ (natural_transformation_scope) [notation, in ProductInducedFunctors]
_ o _ (natural_transformation_scope) [notation, in NaturalTransformation]
_ ◇ _ (natural_transformation_scope) [notation, in NaturalTransformation]
( _ | _ ) (nat_scope) [notation, in NatOrders]
π₂ (object_scope) [notation, in Product]
π₁ (object_scope) [notation, in Product]
_ × _ (object_type_scope) [notation, in Product]
_ × _ (object_scope) [notation, in Product]
i₂ (object_scope) [notation, in Coproduct]
i₁ (object_scope) [notation, in Coproduct]
_ ⊔ _ (object_type_scope) [notation, in Coproduct]
_ ⊔ _ (object_scope) [notation, in Coproduct]
_ × _ (old_type_scope) [notation, in SwapExercise]
_ × _ (product_scope) [notation, in SwapExercise]
_ × _ (product_type_scope) [notation, in SwapExercise]
_ * _ (relation_scope) [notation, in OrderProduct]
_ + _ (relation_scope) [notation, in OrderCoproduct]
_ ⁻¹ (topology_scope) [notation, in Topology]
⋂ _ (topology_scope) [notation, in Topology]
⋃ _ (topology_scope) [notation, in Topology]
_ ⊔ _ (type_scope) [notation, in Notations]
_ × _ (type_scope) [notation, in Notations]
_ ↷ _ (type_scope) [notation, in Monoid]
_ × _ (type_scope) [notation, in SwapExercise]
_ ~> _ (type_scope) [notation, in Category]
_ ⁻¹ (type_scope) [notation, in Group]
_ ≅ _ (type_scope) [notation, in Isomorphism]
_ ⊆ _ [notation, in Notations]
_ ∪ _ [notation, in Notations]
_ ∩ _ [notation, in Notations]
_ ∈ _ [notation, in Notations]
_ == _ [notation, in Notations]
_ ⊔ _ [notation, in Morphism]
_ o _ [notation, in Morphism]
_ ↷ _ [notation, in Monoid]
_ ★ _ [notation, in Monoid]
_ -| _ [notation, in Adjoint]
_ ⊣ _ [notation, in Adjoint]
_ ⁻¹ [notation, in Isomorphism]
[notation, in Notations]
∫ _ [notation, in Grothendieck]
π₁ [notation, in SwapExercise]
π₂ [notation, in SwapExercise]
[abbreviation, in Notations]
[abbreviation, in Exercise_4_5_3_6]
[abbreviation, in Exercise_4_2_3_12]



Instance Index

C

CategoryOfCategories_product [in ProductCategory]
ComposeIsomorphismOf [in CategoryIsomorphisms]
conj_is_product [in SetCategoryFacts]
coproduct_decidable [in OrderCoproduct]


D

divides_dec [in NatOrders]
divides_partial_order [in NatOrders]
divides_antisym [in NatOrders]
divides_pre_order [in NatOrders]
divides_trans [in NatOrders]
divides_refl [in NatOrders]


E

EnsembleHasEnsembleJoins [in EnsemblePreOrder]
EnsembleHasEnsembleMeets [in EnsemblePreOrder]
EnsembleHasIndexedJoins [in EnsemblePreOrder]
EnsembleHasIndexedMeets [in EnsemblePreOrder]
EnsembleHasJoins [in EnsemblePreOrder]
EnsembleHasMeets [in EnsemblePreOrder]
Ensemble_PreOrder [in EnsemblePreOrder]
eq_pre_order [in Orders]
Exercise_3_4_1_7_R_preorder [in Exercise_3_4_1_7]
Exercise_3_3_2_4_SingletonGraphIsMonoid [in Exercise_3_3_2_4]
Exercise_5_3_3_6.PowerSetMonadProducts [in Exercise_5_3_3_6]
Exercise_5_3_3_6.PowerSumIsProductPower [in Exercise_5_3_3_6]
Exercise_5_3_3_7.PowerSetMonadCoproducts [in Exercise_5_3_3_7]
Exercise_4_6_1_5.Exercise_4_2_4_4.SetsPreOrder [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.JurisdictionPreOrder [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.JurisdictionPreOrder [in Exercise_4_6_1_5]
Exercise_4_6_1_5.opens_ordered_by_inclusion [in Exercise_4_6_1_5]
Exercise_4_2_4_3.JurisdictionPreOrder [in Exercise_4_2_4_3]
Exercise_4_2_4_4.SetsPreOrder [in Exercise_4_2_4_4]
Exercise_4_2_4_4.JurisdictionPreOrder [in Exercise_4_2_4_4]
Exercise_3_2_1_7_is_group [in Exercise_3_2_1_7]
Exercise_3_2_1_7_is_monoid [in Exercise_3_2_1_7]


G

gcd_is_product [in Exercise_4_5_1_16]
gcd_n_m [in Exercise_4_5_1_16]
gcd_n_m_flip [in Exercise_4_5_1_16]
gcd_n_n [in Exercise_4_5_1_16]
gcd_n_1 [in Exercise_4_5_1_16]
gcd_1_n [in Exercise_4_5_1_16]
gcd_n_0 [in Exercise_4_5_1_16]
gcd_0_n [in Exercise_4_5_1_16]


I

Included_trans [in Topology]
Included_refl [in Topology]
InverseOf [in CategoryIsomorphisms]
IsomorphismOf_Identity [in CategoryIsomorphisms]


K

KleisliCategory_has_is_products [in KleisliCategoryProducts]
KleisliCategory_has_is_coproducts [in KleisliCategoryCoproducts]


L

le_dec' [in NatOrders]
le_linear_order' [in NatOrders]
le_comp' [in NatOrders]
le_partial_order' [in NatOrders]
le_antisym' [in NatOrders]
le_pre_order' [in NatOrders]
le_trans' [in NatOrders]
le_refl' [in NatOrders]
LinearOrderCategory_is_LinearOrder [in Exercise_4_2_1_16]
LinearOrder_op_is_LinearOrder [in Exercise_3_4_2_7]
LinearOrder_is_LinearOrderCategory [in Exercise_4_2_1_16]


O

opens_ordered_by_inclusion [in Exercise_4_2_3_2]
or_is_coproduct [in SetCategoryFacts]


P

PartialOrderCategory_is_PartialOrder [in Exercise_4_2_1_13]
PartialOrder_op_is_PartialOrder [in Exercise_3_4_2_7]
PartialOrder_is_PartialOrderCategory [in Exercise_4_2_1_13]
PreOrder_op_is_PreOrder [in Exercise_3_4_2_7]
prodT_is_product [in SetCategoryFacts]
product_decidable [in OrderProduct]
product_strict_order [in OrderProduct]
product_partial_order [in OrderProduct]
product_antisym [in OrderProduct]
product_equiv [in OrderProduct]
product_PER [in OrderProduct]
product_pre_order [in OrderProduct]
product_trans [in OrderProduct]
product_asym [in OrderProduct]
product_sym [in OrderProduct]
product_irefl [in OrderProduct]
product_refl [in OrderProduct]
prod_is_product [in SetCategoryFacts]
PropHasEnsembleJoins [in PropPreOrder]
PropHasEnsembleMeets [in PropPreOrder]
PropHasIndexedJoins [in PropPreOrder]
PropHasIndexedMeets [in PropPreOrder]
PropHasJoins [in PropPreOrder]
PropHasMeets [in PropPreOrder]
Prop_PreOrder [in PropPreOrder]


S

sig2_IsomorphismOf [in CategoryIsomorphisms]
SubspaceTopology [in SubspaceTopology]
sumT_is_coproduct [in SetCategoryFacts]
sum_is_coproduct [in SetCategoryFacts]
sum_strict_order [in OrderCoproduct]
sum_partial_order [in OrderCoproduct]
sum_antisym [in OrderCoproduct]
sum_equiv [in OrderCoproduct]
sum_PER [in OrderCoproduct]
sum_pre_order [in OrderCoproduct]
sum_trans [in OrderCoproduct]
sum_asym [in OrderCoproduct]
sum_sym [in OrderCoproduct]
sum_irefl [in OrderCoproduct]
sum_refl [in OrderCoproduct]


Z

ZeroIsGroup [in ZeroGroup]
ZeroIsMonoid [in ZeroGroup]



Projection Index

A

ACommutes [in Adjoint]
AComponentsOf [in Adjoint]
action_respectful [in Monoid]
Adjunction_UnitCounitEquation2 [in AdjointUnit]
Adjunction_UnitCounitEquation1 [in AdjointUnit]
Adjunction_Counit [in AdjointUnit]
Adjunction_Unit [in AdjointUnit]
AIsomorphism [in Adjoint]
AMateOf [in Adjoint]
ArbitraryUnionOpen [in Topology]
Arrow' [in Graph]
assoc [in Monoid]
Associativity [in Category]


C

category_connected [in Exercise_4_2_1_16]
cgroup [in Group]
ClassContainsEquivalent [in EquivalenceClass]
ClassElementsEquivalent [in EquivalenceClass]
ClassEquivalent_trans [in EquivalenceClass]
ClassEquivalent_sym [in EquivalenceClass]
ClassEquivalent_refl [in EquivalenceClass]
ClassInhabited [in EquivalenceClass]
cmonoid [in Monoid]
CommaCategory_Morphism_Member [in CommaCategory]
CommaCategory_Object_Member [in CommaCategory]
Commutes [in NaturalTransformation]
comp [in Monoid]
comparability [in Orders]
ComponentsOf [in NaturalTransformation]
Compose [in Category]
ContainsEmpty [in Topology]
ContainsSpace [in Topology]
coproduct_is_coproduct [in Coproduct]
coproduct_element [in Coproduct]
coproduct_map_unique [in Coproduct]
coproduct_inr_commutes [in Coproduct]
coproduct_inl_commutes [in Coproduct]
coproduct_map [in Coproduct]
coproduct_inr [in Coproduct]
coproduct_inl [in Coproduct]
CoveringSpaceHomeomorphism [in CoveringSpace]
CoveringSpaceMap [in CoveringSpace]
CoveringSpaceMap_continuous [in CoveringSpace]
CoveringSpace_IsCoveringSpace [in CoveringSpace]
CoveringSpace_InverseImageSets_DisjointUnion [in CoveringSpace]
CoveringSpace_InverseImageSets [in CoveringSpace]
CoveringSpace_CoverOpen [in CoveringSpace]
CoveringSpace_Cover [in CoveringSpace]
Covers [in OpenCover]
CoverSets [in OpenCover]


D

DisjointUnionIsUnion [in Topology]
DisjointUnionSets [in Topology]
DisjointUnionSetsDisjoint [in Topology]


E

Edge [in Graph]
EnsembleJoinElement [in Orders]
EnsembleMeetElement [in Orders]
ensemble_join_is_join [in Orders]
ensemble_meet_is_meet [in Orders]
Equivalence_Transitive [in Isomorphism]
Equivalence_Symmetric [in Isomorphism]
Equivalence_Reflexive [in Isomorphism]
Exercise_4_6_1_5.OpenSetOpen [in Exercise_4_6_1_5]
Exercise_4_6_1_5.OpenSetSet [in Exercise_4_6_1_5]
Exercise_4_5_2_3.TriangleCommutes [in Exercise_4_5_2_3]
Exercise_4_5_2_3.h [in Exercise_4_5_2_3]
Exercise_4_5_2_3.g [in Exercise_4_5_2_3]
Exercise_4_5_2_3.f [in Exercise_4_5_2_3]
Exercise_4_5_2_3.c [in Exercise_4_5_2_3]
Exercise_4_5_2_3.b [in Exercise_4_5_2_3]
Exercise_4_5_2_3.a [in Exercise_4_5_2_3]


F

FCompositionOf [in Functor]
FIdentityOf [in Functor]
FiniteIntersectionOpen [in Topology]


G

gcd_maximal [in Exercise_4_5_1_16]
gcd_divides_second [in Exercise_4_5_1_16]
gcd_divides_first [in Exercise_4_5_1_16]
Graph'Source [in Graph]
Graph'Target [in Graph]
GrothendieckC [in Grothendieck]
GrothendieckX [in Grothendieck]
GroupIsMonoid [in Group]
GroupoidCategory [in Groupoid]
GroupoidIsGroupoid [in Groupoid]
GroupoidType [in Groupoid]
group_inverse_is_inverse [in Group]
group_inverse [in Group]
group_monoid [in Group]


H

Homeomophic_Homeomorphism [in Homeomorphism]
HomeomophismContinuous [in Homeomorphism]
HomeomophismInverse [in Homeomorphism]
HomeomophismInverseContinuous [in Homeomorphism]
Homeomophism1 [in Homeomorphism]
HomeomorphismInverse1 [in Homeomorphism]
HomeomorphismInverse2 [in Homeomorphism]


I

id [in Monoid]
Identity [in Category]
id_action [in Monoid]
InClass [in EquivalenceClass]
IndexedJoinElement [in Orders]
IndexedMeetElement [in Orders]
indexed_join_is_join [in Orders]
indexed_meet_is_meet [in Orders]
InitialObject_Property [in CategoryObjects]
InitialObject_Morphism [in CategoryObjects]
InitialObject_Object' [in CategoryObjects]
InSet' [in EquivalenceSet]
Inverse [in CategoryIsomorphisms]
InverseFunctor [in FunctorIsomorphisms]
isomorphic_is_isomorphism [in Isomorphism]
isomorphic_morphism [in Isomorphism]
IsomorphismOfCategories_Of [in FunctorIsomorphisms]
IsomorphismOfCategories_Functor [in FunctorIsomorphisms]
Isomorphism_Of [in CategoryIsomorphisms]
Isomorphism_Morphism [in CategoryIsomorphisms]
isomorphism_left_inverse [in Isomorphism]
isomorphism_right_inverse [in Isomorphism]
isomorphism_inverse [in Isomorphism]
iso_implies_id [in Exercise_4_2_1_13]
is_monoid_action [in Monoid]
is_monoid [in Monoid]
is_group [in Group]
is_groupoid [in Groupoid]


J

JoinElement [in Orders]
join_is_join [in Orders]


L

LeftIdentity [in Category]
LeftInverse [in CategoryIsomorphisms]
LeftInverseFunctor [in FunctorIsomorphisms]
left_id [in Monoid]
LinearOrder_Comparable [in Orders]
LinearOrder_Transitive [in Orders]
LinearOrder_Reflexive [in Orders]


M

MeetElement [in Orders]
meet_is_meet [in Orders]
MonadFunctor [in Monad]
MonadFunctorDiagram1 [in Monad]
MonadFunctorDiagram2 [in Monad]
MonadFunctorDiagram3 [in Monad]
MonadMultiplication [in Monad]
MonadUnit [in Monad]
MonoidHomomorphism_CompositionLaw [in Monoid]
MonoidHomomorphism_IdentityLaw [in Monoid]
MonoidHomomorphism_Function [in Monoid]
monoid_action [in Monoid]
Morphism [in Category]
MorphismOf [in Functor]


N

NaturalIsomorphismOfCategories_Isomorphism_D [in NaturalEquivalence]
NaturalIsomorphismOfCategories_Isomorphism_C [in NaturalEquivalence]
NaturalIsomorphismOfCategories_G [in NaturalEquivalence]
NaturalIsomorphismOfCategories_F [in NaturalEquivalence]
NaturalIsomorphism_Isomorphism [in NaturalEquivalence]
NaturalIsomorphism_Transformation [in NaturalEquivalence]


O

ObjectOf [in Functor]
OnArrows' [in Graph]
OnEdges [in Graph]
OnVertices [in Graph]
OnVertices' [in Graph]
Open [in Topology]
OpenSetOpen [in Exercise_4_2_3_2]
OpenSetSet [in Exercise_4_2_3_2]


P

PathOf [in SchemaMorphism]
PathsEquivalent [in Schema]
PathsEquivalent_Equivalence [in Schema]
PostCompose [in Schema]
PreCompose [in Schema]
PreOrderedSetPreOrder [in PreOrderCategory]
PreOrderedSetRelation [in PreOrderCategory]
PreOrderedSetType [in PreOrderCategory]
product_is_product [in Product]
product_element [in Product]
product_map_unique [in Product]
product_snd_commutes [in Product]
product_fst_commutes [in Product]
product_map [in Product]
product_snd [in Product]
product_fst [in Product]
prodXY [in SwapExercise]
prod_map_unique [in SwapExercise]
prod_snd_commutes [in SwapExercise]
prod_fst_commutes [in SwapExercise]
prod_map [in SwapExercise]
prod_snd [in SwapExercise]
prod_fst [in SwapExercise]


R

RelationHomomorphism_Respectful [in Orders]
RelationHomomorphism_Function [in Orders]
Relation_dec [in Orders]
RightIdentity [in Category]
RightInverse [in CategoryIsomorphisms]
RightInverseFunctor [in FunctorIsomorphisms]
right_id [in Monoid]


S

SEdge [in Schema]
SetContainsEquivalent [in EquivalenceSet]
SetElementsEquivalent [in EquivalenceSet]
SetEquivalent_trans [in EquivalenceSet]
SetEquivalent_sym [in EquivalenceSet]
SetEquivalent_refl [in EquivalenceSet]
SetInhabited [in EquivalenceSet]
SourceCommutes' [in Graph]
SVertex [in Schema]


T

TargetCommutes' [in Graph]
TEquivalenceOf [in SchemaMorphism]
TerminalObject_Property [in CategoryObjects]
TerminalObject_Morphism [in CategoryObjects]
TerminalObject_Object' [in CategoryObjects]
TopologyOfTotalTopology [in TopologyCategory]
TypeOfTotalTopology [in TopologyCategory]


V

Vertex [in Graph]
VertexOf [in SchemaMorphism]
Vertex' [in Graph]



Record Index

A

Adjunction [in Adjoint]
AdjunctionUnitCounit [in AdjointUnit]


C

Category [in Category]
CategoryConnected [in Exercise_4_2_1_16]
CommaCategory_Morphism [in CommaCategory]
CommaCategory_Object [in CommaCategory]
Comparable [in Orders]
ComputationalGroup [in Group]
ComputationalMonoid [in Monoid]
coproduct [in Coproduct]
Cover [in OpenCover]
CoveringSpace [in CoveringSpace]


E

EnsembleJoinOf [in Orders]
EnsembleMeetOf [in Orders]
EOpenSet [in Exercise_4_2_3_2]
Equivalence [in Isomorphism]
EquivalenceClass [in EquivalenceClass]
EquivalenceSet [in EquivalenceSet]
Exercise_4_6_1_5.EOpenSet [in Exercise_4_6_1_5]
Exercise_4_5_2_3.CommutativeTriangle [in Exercise_4_5_2_3]


F

Functor [in Functor]
FunctorIsomorphismOf [in FunctorIsomorphisms]


G

Graph [in Graph]
GraphHomomorphism [in Graph]
Graph' [in Graph]
Graph'Homomorphism [in Graph]
GrothendieckPair [in Grothendieck]
Group [in Group]
Groupoid [in Groupoid]


H

HomAdjunction [in Adjoint]
Homeomophic [in Homeomorphism]
Homeomorphism [in Homeomorphism]


I

IndexedJoinOf [in Orders]
IndexedMeetOf [in Orders]
InitialObject [in CategoryObjects]
IsCoveringSpace [in CoveringSpace]
IsDisjointUnion [in Topology]
IsGroup [in Group]
IsGroupoid [in Groupoid]
IsMonoid [in Monoid]
IsMonoidAction [in Monoid]
IsoImpliesId [in Exercise_4_2_1_13]
isomorphic [in Isomorphism]
Isomorphism [in CategoryIsomorphisms]
IsomorphismOf [in CategoryIsomorphisms]
IsomorphismOfCategories [in FunctorIsomorphisms]
is_gcd [in Exercise_4_5_1_16]
is_product [in Product]
is_coproduct [in Coproduct]
is_isomorphism [in Isomorphism]


J

JoinOf [in Orders]


L

LinearOrder [in Orders]


M

MeetOf [in Orders]
Monad [in Monad]
Monoid [in Monoid]
MonoidAction [in Monoid]
MonoidHomomorphism [in Monoid]


N

NaturalIsomorphism [in NaturalEquivalence]
NaturalIsomorphismOfCategories [in NaturalEquivalence]
NaturalTransformation [in NaturalTransformation]


P

PreOrderedSet [in PreOrderCategory]
product [in Product]
product_type [in SwapExercise]


R

RelationDecidable [in Orders]
RelationHomomorphism [in Orders]


S

Schema [in Schema]
SchemaMorphism [in SchemaMorphism]


T

TerminalObject [in CategoryObjects]
Topology [in Topology]
TotalTopology [in TopologyCategory]



Lemma Index

A

ACommutes_Inverse [in Adjoint]
addedge_equivalent [in Schema]
adjunction_naturality'_pre [in Adjoint]
adjunction_naturality_pre [in Adjoint]
apply_to_classOf [in EquivalenceClass]
apply_to_class_f_surj [in EquivalenceClass]
apply_to_class_f_inj [in EquivalenceClass]
apply2_to_classOf [in EquivalenceClass]
apply2_to_class_f_surj [in EquivalenceClass]
apply2_to_class_f_inj [in EquivalenceClass]
AssociativityNoEvar [in Category]


C

CategoriesIsomorphic_trans [in FunctorIsomorphisms]
CategoriesIsomorphic_sym [in FunctorIsomorphisms]
CategoriesIsomorphic_refl [in FunctorIsomorphisms]
CategoriesIsomorphic_IsomorphismOfCategories [in FunctorIsomorphisms]
classOf_eq [in EquivalenceClass]
classOf_refl [in EquivalenceClass]
closure_respect_subset [in Closure]
closure_closed_same [in Closure]
closure_superset [in Closure]
closure_closed [in Closure]
CommaCategory_RightIdentity [in CommaCategory]
CommaCategory_LeftIdentity [in CommaCategory]
CommaCategory_Associativity [in CommaCategory]
CommaCategory_Morphism_Eq [in CommaCategory]
complement_intersection [in Topology]
complement_union [in Topology]
complement_idempotent [in Topology]
ComposeFunctorsAssociativity [in Functor]
ComposeFunctorsAssociativityNE [in NaturalEquivalence]
ComposeSchemaMorphismsAssociativity [in SchemaMorphism]
compose_transferPath [in SchemaMorphism]
compose_path_prepend [in Path]
compose_path_addedge [in Path]
compose4associativity_helper [in CategoryMorphisms]
concatenate_TransferPath [in SchemaMorphism]
concatenate_transferPath [in SchemaMorphism]
concatenate_equivalent [in Schema]
concatenate_associative [in Path]
concatenate_prepend_p [in Path]
concatenate_p_addedge [in Path]
concatenate_concatenate'_equivalent [in Path]
concatenate_addedge_concatenate'_prepend [in Path]
concatenate_p_noedges [in Path]
concatenate_noedges_p [in Path]
concatenate'_noedges_p [in Path]
concatenate'_p_noedges [in Path]
concatenate'_p_addedge [in Path]
covering_space_inverse_image_open [in CoveringSpace]
covering_space_open_to_open [in CoveringSpace]
covering_space_subset_open [in CoveringSpace]


D

DecidableEqDepSet.eq_dep_eq [in Eqdep_dec_one_variable]
DecidableEqDepSet.eq_rect_eq [in Eqdep_dec_one_variable]
DecidableEqDepSet.inj_pair2 [in Eqdep_dec_one_variable]
DecidableEqDepSet.inj_pairP2 [in Eqdep_dec_one_variable]
DecidableEqDepSet.Streicher_K [in Eqdep_dec_one_variable]
DecidableEqDepSet.UIP [in Eqdep_dec_one_variable]
DecidableEqDepSet.UIP_refl [in Eqdep_dec_one_variable]
DecidableEqDep.eq_dep_eq [in Eqdep_dec_one_variable]
DecidableEqDep.eq_rect_eq [in Eqdep_dec_one_variable]
DecidableEqDep.inj_pairP2 [in Eqdep_dec_one_variable]
DecidableEqDep.inj_pairT2 [in Eqdep_dec_one_variable]
DecidableEqDep.Streicher_K [in Eqdep_dec_one_variable]
DecidableEqDep.UIP [in Eqdep_dec_one_variable]
DecidableEqDep.UIP_refl [in Eqdep_dec_one_variable]
destruct_path [in Exercise_4_1_2_28]
DiscreteObjectIdentity [in DiscreteCategoryFunctors]
disjointClasses_differentClasses [in EquivalenceClass]
disjointSets_differentSets [in EquivalenceSet]
disjoint_union_in [in Topology]


E

Empty_set_JMeqr [in Common]
Empty_set_JMeql [in Common]
Empty_set_eq [in Common]
EpimorphismComposition [in CategoryMorphisms]
EpiSurj [in SetCategoryFacts]
EqdepTheory.eq_dep_eq [in EqdepFacts_one_variable]
EqdepTheory.eq_rec_eq [in EqdepFacts_one_variable]
EqdepTheory.eq_rect_eq [in EqdepFacts_one_variable]
EqdepTheory.inj_pair2 [in EqdepFacts_one_variable]
EqdepTheory.Streicher_K [in EqdepFacts_one_variable]
EqdepTheory.UIP [in EqdepFacts_one_variable]
EqdepTheory.UIP_refl [in EqdepFacts_one_variable]
EquivalenceClass_eq_iso2 [in EquivalenceClass]
EquivalenceClass_eq_iso1 [in EquivalenceClass]
EquivalenceClass_forall__eq [in EquivalenceClass]
EquivalenceClass_forall_equiv__eq [in EquivalenceClass]
EquivalenceOf_Equivalence [in EquivalenceRelationGenerator]
EquivalenceSet_eq_iso2 [in EquivalenceSet]
EquivalenceSet_eq_iso1 [in EquivalenceSet]
EquivalenceSet_forall__eq [in EquivalenceSet]
EquivalenceSet_forall_equiv__eq [in EquivalenceSet]
equiv_helper [in Exercise_5_1_1_9]
eq_sameSet [in EquivalenceSet]
eq_dep_eq_dec [in Eqdep_dec_one_variable]
eq_rect_eq_dec [in Eqdep_dec_one_variable]
eq_proofs_unicity [in Eqdep_dec_one_variable]
eq_dep_eq__inj_pair2 [in EqdepFacts_one_variable]
eq_dep_eq__UIP [in EqdepFacts_one_variable]
eq_rect_eq__eq_dep_eq [in EqdepFacts_one_variable]
eq_rect_eq__eq_dep1_eq [in EqdepFacts_one_variable]
eq_sig_snd [in EqdepFacts_one_variable]
eq_sig_fst [in EqdepFacts_one_variable]
eq_sigT_snd [in EqdepFacts_one_variable]
eq_sigT_fst [in EqdepFacts_one_variable]
eq_sigT_sig_eq [in EqdepFacts_one_variable]
eq_sig_iff_eq_dep [in EqdepFacts_one_variable]
eq_dep_eq_sig [in EqdepFacts_one_variable]
eq_sig_eq_dep [in EqdepFacts_one_variable]
eq_sigT_iff_eq_dep [in EqdepFacts_one_variable]
eq_dep_eq_sigT [in EqdepFacts_one_variable]
eq_sigT_eq_dep [in EqdepFacts_one_variable]
eq_dep_dep1 [in EqdepFacts_one_variable]
eq_dep1_dep [in EqdepFacts_one_variable]
eq_dep_trans [in EqdepFacts_one_variable]
eq_dep_sym [in EqdepFacts_one_variable]
eq_dep_refl [in EqdepFacts_one_variable]
eq_JMeq [in FEqualDep]
eq_trans_id [in Exercise_4_2_3_12]
eq_sameClass [in EquivalenceClass]
Exercise_4_1_2_31.Hom_C_v_x_two_elements [in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom_C_x_v_empty [in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom_C_v_x_only_helper [in Exercise_4_1_2_31]
Exercise_4_1_2_31.Hom_C_x_v_empty_helper [in Exercise_4_1_2_31]
Exercise_4_4_1_1.Exercise_4_4_1_1_a_edges [in Exercise_4_4_1_1]
Exercise_4_4_1_1.nth_edge_in_loop_injective [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Exercise_4_4_1_1_a_vert [in Exercise_4_4_1_1]
Exercise_4_4_1_5.b_schema_morphism_all [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_schema_morphsim_on_paths [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_schema_morphism_all_template' [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_2_0_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_2_1_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_0_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_2_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_2_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_1_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_2_2_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_1_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_0_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_schema_morphism_all [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_schema_morphsim_on_paths [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_schema_morphism_all_template [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_c_a_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_c_b_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_a_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_c_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_c_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_b_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_c_c_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_b_only [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_a_only [in Exercise_4_4_1_5]
Exercise_4_4_1_6.L0_to_singleton_to_L0_id [in Exercise_4_4_1_6]
Exercise_4_4_1_6.singleton_to_L0_to_singleton_id [in Exercise_4_4_1_6]
Exercise_4_4_1_6.count_edges_concatenate [in Exercise_4_4_1_6]
Exercise_4_4_1_6.count_edges_prepend [in Exercise_4_4_1_6]
Exercise_4_6_4_3 [in Exercise_4_6_4_3]
Exercise_4_5_1_14_only [in Exercise_4_5_1_14]
Exercise_4_5_1_28_only [in Exercise_4_5_1_28]
Exercise_4_2_3_2_continuity_bad.f_not_preserve_open [in Exercise_4_2_3_2]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand_subset_flip [in Exercise_4_6_1_5]
Exercise_4_6_1_5.OpenSet_eq [in Exercise_4_6_1_5]
Exercise_4_2_4_3.LawOfTheLand_subset_flip [in Exercise_4_2_4_3]
Exercise_4_5_2_3.triangle_commutes [in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_h [in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_g [in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_f [in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_c [in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_b [in Exercise_4_5_2_3]
Exercise_4_5_2_3.pf_a [in Exercise_4_5_2_3]
Exercise_4_5_2_5.SecondDiagram_MorphismOf_commut [in Exercise_4_5_2_5]
Exercise_4_5_2_9.Exercise_4_5_2_9 [in Exercise_4_5_2_9]
Exercise_4_5_2_9.chain_to_C_MorphismOf [in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_to_chain_MorphismOf [in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_morphism_unicity [in Exercise_4_5_2_9]
Exercise_4_5_2_12.Exercise_4_5_2_12 [in Exercise_4_5_2_12]
Exercise_4_5_2_12.pf_1_le_1 [in Exercise_4_5_2_12]
Exercise_4_5_2_12.pf_0_le_1 [in Exercise_4_5_2_12]
Exercise_4_5_2_12.pf_0_le_0 [in Exercise_4_5_2_12]
Exercise_4_1_1_13 [in Exercise_4_1_1_13]
Exercise_4_1_1_14 [in Exercise_4_1_1_14]
Exercise_3_5_2_4.Exercise_3_5_2_4_c [in Exercise_3_5_2_4]
Exercise_3_5_2_4.Exercise_3_5_2_4_a [in Exercise_3_5_2_4]
Exercise_4_2_1_14 [in Exercise_4_2_1_14]
E_4_1_2_28_Hom_v0_v1 [in Exercise_4_1_2_28]
E_4_1_2_28_Hom_v1_v0 [in Exercise_4_1_2_28]
E_4_1_2_28_Hom_v1_v1 [in Exercise_4_1_2_28]
E_4_1_2_28_Hom_v0_v0 [in Exercise_4_1_2_28]
E_4_1_2_28_Objects_G [in Exercise_4_1_2_28]


F

False_JMeqr [in Common]
False_JMeql [in Common]
False_eq [in Common]
fg_equal [in Common]
fg_equal_JMeq [in FEqualDep]
fiber_is_relation [in Exercise_2_6_1_5]
forall_extensionality_dep_JMeq [in FEqualDep]
forall_extensionality_dep [in FEqualDep]
FunCSet_Hom_Iso_Set [in Exercise_4_3_2_5]
FunCSet_Iso_Set [in Exercise_4_3_2_5]
functional_extensionality_dep_JMeq' [in FEqualDep]
functional_extensionality_dep_JMeq [in FEqualDep]
FunctorIsInverseOf_sym [in FunctorIsomorphisms]
FunctorIsIsomorphism_FunctorIsmorphismOf [in FunctorIsomorphisms]
FunctorIsmorphismOf_FunctorIsIsomorphism [in FunctorIsomorphisms]
functors_naturally_equivalent_trans [in NaturalEquivalence]
functors_naturally_equivalent_sym [in NaturalEquivalence]
functors_naturally_equivalent_refl [in NaturalEquivalence]
FunctorToTerminalUnique [in Exercise_4_1_2_34]
Functor_Eq_by_JMeq [in Functor]
Functor_Eq [in Functor]
f_equal_helper [in Common]
f_equal5_JMeq [in FEqualDep]
f_equal4_JMeq [in FEqualDep]
f_equal3_JMeq [in FEqualDep]
f_equal2_JMeq [in FEqualDep]
f_equal1_JMeq [in FEqualDep]
f_equal_JMeq [in FEqualDep]
f_type_equal [in FEqualDep]


G

GeneralizedPathsEquivalent_trans [in Schema]
GeneralizedPathsEquivalent_sym [in Schema]
GeneralizedPathsEquivalent_refl [in Schema]
GeneralizedPathsEquivalent_eq [in Schema]
GeneralizedPathsEquivalent_PathsEquivalent [in Schema]
generalized_fg_equal [in Common]
GraphHomomorphism_Eq [in Graph]
Graph'Homomorphism_Eq [in Graph]
GrothendieckPair_eta [in Grothendieck]


H

homemorphism_open_to_open [in Homeomorphism]
HomomorphismFromZeroGroup_unique [in ZeroGroup]
HomomorphismToZeroGroup_unique [in ZeroGroup]


I

IdentityIsEpimorphism [in CategoryMorphisms]
IdentityIsMonomorphism [in CategoryMorphisms]
IdentityNaturalEquivalence [in NaturalEquivalence]
InClass_classOf_eq [in EquivalenceClass]
InitialObjectUnique [in CategoryObjects]
injective_projections_JMeq [in Common]
InjMono [in SetCategoryFacts]
inj_pair2_eq_dec [in Eqdep_dec_one_variable]
inj_right_pair [in Eqdep_dec_one_variable]
InSet_setOf_eq [in EquivalenceSet]
interior_respect_subset [in Interior]
interior_open_same [in Interior]
interior_subset [in Interior]
interior_open [in Interior]
IntersectionAAA [in Topology]
IntersectionCover_open [in CoveringSpace]
intersection_arbitrary_union_commute [in Topology]
IsInverseOf_sym [in CategoryIsomorphisms]
IsIsomorphism_IsomorphismOf [in CategoryIsomorphisms]
IsmorphismOfCategories_CategoriesIsomorphic [in FunctorIsomorphisms]
Isomorphic_trans [in CategoryIsomorphisms]
Isomorphic_sym [in CategoryIsomorphisms]
Isomorphic_refl [in CategoryIsomorphisms]
Isomorphic_Isomorphism [in CategoryIsomorphisms]
isomorphic_eq [in Isomorphism]
IsomrphismOf_IsIsomorphism [in CategoryIsomorphisms]
Isomrphism_Isomorphic [in CategoryIsomorphisms]
iso_is_mono [in CategoryIsomorphisms]
iso_is_epi [in CategoryIsomorphisms]


J

JMeq_eqT [in FEqualDep]


K

K_dec_set [in Eqdep_dec_one_variable]
K_dec_type [in Eqdep_dec_one_variable]
K_dec [in Eqdep_dec_one_variable]


L

LeftCone_FCompositionOf [in Cone]
LeftCone_FIdentityOf [in Cone]
LeftIdentityFunctor [in Functor]
LeftIdentityFunctorNE [in NaturalEquivalence]
LeftIdentityFunctorNT_Isomorphism [in NaturalTransformation]
LeftIdentityNaturalTransformation [in NaturalTransformation]
LeftIdentityNaturalTransformation' [in Exercise_4_3_1_3]
LeftIdentitySchemaMorphism [in SchemaMorphism]
le_trans [in NatFacts]
le_refl [in NatFacts]


M

MonoidHomomorphism_Eq [in Monoid]
MonoInj [in SetCategoryFacts]
MonomorphismComposition [in CategoryMorphisms]


N

NaturalEquivalenceInverse_NaturalEquivalence [in NaturalEquivalence]
NaturalTransformationExchangeLaw [in NaturalTransformation]
NaturalTransformation_Eq [in NaturalTransformation]
nat_le_proofs_unicity [in NatFacts]
notDisjointClasses_eq [in EquivalenceClass]
notDisjointClasses_sameClass [in EquivalenceClass]
notDisjointSets_eq [in EquivalenceSet]
notDisjointSets_sameSet [in EquivalenceSet]
no_path' [in Exercise_4_1_2_28]
no_smaller_monoid [in Exercise_3_1_1_7]
NTComposeFIdentityNaturalTransformation [in NaturalTransformation]
nu_left_inv [in Eqdep_dec_one_variable]


O

OneLeOne [in Exercise_4_1_2_28]
OneLtTwo [in Exercise_4_1_2_33]
one_path' [in Exercise_4_1_2_28]
OpenSet_eq [in Exercise_4_2_3_2]
open_subcover_open [in OpenCover]


P

PostComposeFunctorsNE [in NaturalEquivalence]
PostComposeSchemaMorphismsEquivalent [in SchemaMorphism]
PostCompose' [in Schema]
post_compose_identity2 [in CategoryIsomorphisms]
post_compose_identity [in CategoryIsomorphisms]
post_concatenate_equivalent [in Schema]
PreComposeFunctorsNE [in NaturalEquivalence]
PreComposeSchemaMorphismsEquivalent [in SchemaMorphism]
PreCompose' [in Schema]
prepend_equivalent [in Schema]
pre_compose_identity2 [in CategoryIsomorphisms]
pre_compose_identity [in CategoryIsomorphisms]
pre_concatenate_equivalent [in Schema]
prod_eta [in Common]
proof_irrelevance_JMeq [in Exercise_4_1_2_34]
proof_irrelevance_JMeq [in FEqualDep]


R

RelationHomomorphism_Eq [in Orders]
RightCone_FCompositionOf [in Cone]
RightCone_FIdentityOf [in Cone]
RightIdentityFunctor [in Functor]
RightIdentityFunctorNE [in NaturalEquivalence]
RightIdentityFunctorNT_Isomorphism [in NaturalTransformation]
RightIdentityNaturalTransformation [in NaturalTransformation]
RightIdentityNaturalTransformation' [in Exercise_4_3_1_3]
RightIdentitySchemaMorphism [in SchemaMorphism]


S

sameClass_eq [in EquivalenceClass]
sameClass_trans [in EquivalenceClass]
sameClass_sym [in EquivalenceClass]
sameClass_refl [in EquivalenceClass]
sameSet_eq [in EquivalenceSet]
sameSet_trans [in EquivalenceSet]
sameSet_sym [in EquivalenceSet]
sameSet_refl [in EquivalenceSet]
SchemaIdentityInverse [in Schema]
SchemaIdentityIsomorphism [in Schema]
SchemaIsomorphismComposition [in Schema]
SchemaIsomorphism2Isomorphism' [in Schema]
SchemaMorphismsEquivalent_trans [in SchemaMorphism]
SchemaMorphismsEquivalent_sym [in SchemaMorphism]
SchemaMorphismsEquivalent_refl [in SchemaMorphism]
SchemaMorphisms_equivalent [in SchemaMorphism]
SchemaMorphism_equal_parts [in SchemaMorphism]
SchemaMorphism_Eq [in SchemaMorphism]
setOf_eq [in EquivalenceSet]
setOf_refl [in EquivalenceSet]
sigT_eta [in Common]
sigT_eq [in Common]
sigT2_eta [in Common]
sigT2_eq [in Common]
sig_eta [in Common]
sig_eq [in Common]
sig_JMeq [in FEqualDep]
sig_mor_compat [in Subcategory]
sig_mor_eq [in Subcategory]
sig_obj_compat [in Subcategory]
sig_obj_eq [in Subcategory]
sig2_eta [in Common]
sig2_eq [in Common]
SInverseOf_sym [in Schema]
SInverseOf1 [in Schema]
SInverseOf1' [in Schema]
SInverseOf2 [in Schema]
SplitHom [in Hom]
SplitHom' [in Hom]
Streicher_K__eq_rect_eq [in EqdepFacts_one_variable]
subset_ensemble_union [in Topology]
subset_ensemble_intersection [in Topology]
subset_ensemble_iff2 [in Topology]
subset_ensemble_iff1 [in Topology]
subset_ensemble_included [in Topology]
SurjEpi [in SetCategoryFacts]
sym_iff [in EqdepFacts_one_variable]
sym_iff0 [in EqdepFacts_one_variable]
s_iso_is_mono [in Schema]
s_iso_is_epi [in Schema]


T

TerminalObjectUnique [in CategoryObjects]
ThreeNotLtThree [in Exercise_4_1_2_33]
TransferPath_NoEdges [in SchemaMorphism]
trans_sym_eq [in Eqdep_dec_one_variable]
True_JMeq [in Common]
True_eq_eq [in Common]
True_eq_singleton [in Common]
True_eq [in Common]
True_singleton [in Common]
TwoNotLeOne [in Exercise_4_1_2_28]
two_monoid_is_commutative [in Exercise_3_1_1_7]


U

UIP_refl_nat [in Eqdep_dec_one_variable]
UIP_refl_bool [in Eqdep_dec_one_variable]
UIP_refl_unit [in Eqdep_dec_one_variable]
UIP_dec [in Eqdep_dec_one_variable]
UIP_shift [in EqdepFacts_one_variable]
UIP_refl__Streicher_K [in EqdepFacts_one_variable]
UIP__UIP_refl [in EqdepFacts_one_variable]
UnitCounitOf_Helper2 [in Adjoint]
UnitCounitOf_Helper1 [in Adjoint]
unit_JMeq [in Common]
unit_eq_eq [in Common]
unit_eq_singleton [in Common]
unit_eq [in Common]
unit_singleton [in Common]


Z

ZeroLeOne [in Exercise_4_1_2_28]
ZeroLtTwo [in Exercise_4_1_2_33]



Section Index

A

Adjunction [in Adjoint]
AdjunctionEquivalences [in Adjoint]
AdjunctionEquivalences' [in Adjoint]
AdjunctionEquivalences.typeof [in Adjoint]
AdjunctionUnit [in AdjointUnit]
apply1 [in EquivalenceClass]
apply2 [in EquivalenceClass]
ArrowCategory [in CommaCategory]
AssociativityComposition [in CategoryMorphisms]


C

CategoryObjects1 [in CategoryObjects]
CategoryObjects1.initial [in CategoryObjects]
CategoryObjects1.terminal [in CategoryObjects]
CategoryObjects2 [in CategoryObjects]
CategoryOfGraphs [in GraphCategory]
CategoryOfGroups [in GroupCategory]
CategoryOfMonoids [in MonoidCategory]
CategoryOfTopologies [in TopologyCategory]
category_isomorphisms.Isomorphic [in CategoryIsomorphisms]
category_isomorphisms.IsIsomorphism [in CategoryIsomorphisms]
category_isomorphisms.Isomorphism [in CategoryIsomorphisms]
category_isomorphisms.IsomorphismOf [in CategoryIsomorphisms]
category_isomorphisms [in CategoryIsomorphisms]
category_product [in Product]
category_coproduct [in Coproduct]
category_morphisms.properties [in CategoryMorphisms]
category_morphisms [in CategoryMorphisms]
cat_has_products [in ProductCategory]
ChainCat [in ChainCategory]
closure [in Closure]
Coercions [in NaturalEquivalence]
CommaCategory [in CommaCategory]
compact [in Compact]
complement_idempotent [in Topology]
compose [in AdjointComposition]
ComputableCategory [in ComputableCategory]
continuous [in TopologicalContinuity]
continuous.continuous_composition [in TopologicalContinuity]
continuous.continuous_identity [in TopologicalContinuity]
continuous.continuous_definition [in TopologicalContinuity]
conversion [in Graph]
Corollaries [in EqdepFacts_one_variable]
covering_space [in CoveringSpace]
covers [in OpenCover]


D

Dependent_Equality [in EqdepFacts_one_variable]
description [in EquivalenceSet]
description [in EquivalenceClass]
disc [in DiscreteCategoryFunctors]
DiscreteAdjoints [in DiscreteCategoryFunctors]
DiscreteCategory [in DiscreteCategory]
discrete_topology [in DiscreteTopology]
disjoint_union [in Topology]


E

EnsemblePreOrder [in EnsemblePreOrder]
EnsemblesMeetsAndJoins [in Orders]
EpiMono [in SetCategoryFacts]
EqdepDec [in Eqdep_dec_one_variable]
EqdepTheory.Axioms [in EqdepFacts_one_variable]
equiv [in EquivalenceSet]
equiv [in EquivalenceClass]
EquivalenceClass [in EquivalenceClass]
Equivalences [in EqdepFacts_one_variable]
EquivalenceSet [in EquivalenceSet]
Exercise_4_1_2_28 [in Exercise_4_1_2_28]
Exercise_4_1_2_29 [in Exercise_4_1_2_29]
Exercise_4_1_2_30 [in Exercise_4_1_2_30]
Exercise_4_1_2_33 [in Exercise_4_1_2_33]
Exercise_4_1_2_34 [in Exercise_4_1_2_34]
Exercise_4_1_2_35 [in Exercise_4_1_2_35]
Exercise_4_3_1_3 [in Exercise_4_3_1_3]
Exercise_3_2_1_11 [in Exercise_3_2_1_11]
Exercise_3_2_1_14 [in Exercise_3_2_1_14]
Exercise_4_3_1_9 [in Exercise_4_3_1_9]
Exercise_3_3_1_5 [in Exercise_3_3_1_5]
Exercise_3_3_1_9 [in Exercise_3_3_1_9]
Exercise_3_3_1_10 [in Exercise_3_3_1_10]
Exercise_4_4_1_1.part_b [in Exercise_4_4_1_1]
Exercise_4_4_1_5.part_b [in Exercise_4_4_1_5]
Exercise_4_4_1_5.part_a [in Exercise_4_4_1_5]
Exercise_4_6_4_3 [in Exercise_4_6_4_3]
Exercise_4_5_1_14 [in Exercise_4_5_1_14]
Exercise_4_5_1_16 [in Exercise_4_5_1_16]
Exercise_4_5_1_28 [in Exercise_4_5_1_28]
Exercise_4_3_2_5 [in Exercise_4_3_2_5]
Exercise_5_1_4_4.CategoryLeafTable [in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable [in Exercise_5_1_4_4]
Exercise_3_4_1_2 [in Exercise_3_4_1_2]
Exercise_3_4_1_7 [in Exercise_3_4_1_7]
Exercise_3_4_1_8 [in Exercise_3_4_1_8]
Exercise_4_2_3_2 [in Exercise_4_2_3_2]
Exercise_4_5_1_4 [in Exercise_4_5_1_4]
Exercise_3_3_2_4 [in Exercise_3_3_2_4]
Exercise_4_2_3_12 [in Exercise_4_2_3_12]
Exercise_4_6_1_5.Exercise_4_2_4_4.maximal_law [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_3_2 [in Exercise_4_6_1_5]
Exercise_3_4_2_7 [in Exercise_3_4_2_7]
Exercise_4_2_4_3.LawOfTheLand [in Exercise_4_2_4_3]
Exercise_4_2_4_4.maximal_law [in Exercise_4_2_4_4]
Exercise_4_5_2_3.diagram_to_commutative_triangle [in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram [in Exercise_4_5_2_3]
Exercise_5_1_1_6.indiscrete_adjunction [in Exercise_5_1_1_6]
Exercise_5_1_1_6.discrete_adjunction [in Exercise_5_1_1_6]
Exercise_5_1_1_6.uniform_functors [in Exercise_5_1_1_6]
Exercise_5_1_1_6.uniform [in Exercise_5_1_1_6]
Exercise_5_1_1_6.underlying [in Exercise_5_1_1_6]
Exercise_5_1_1_6 [in Exercise_5_1_1_6]
Exercise_5_1_1_9 [in Exercise_5_1_1_9]
Exercise_4_1_1_13 [in Exercise_4_1_1_13]
Exercise_4_1_1_14 [in Exercise_4_1_1_14]
Exercise_2_6_1_6 [in Exercise_2_6_1_6]
Exercise_4_2_1_13 [in Exercise_4_2_1_13]
Exercise_4_2_1_14 [in Exercise_4_2_1_14]
Exercise_4_2_1_16 [in Exercise_4_2_1_16]
Exercise_4_5_3_6 [in Exercise_4_5_3_6]
Exercise_4_5_3_8 [in Exercise_4_5_3_8]
Exercise_3_5_2_12 [in Exercise_3_5_2_12]
Exercise_3_5_2_13 [in Exercise_3_5_2_13]
Exercise_3_5_2_18 [in Exercise_3_5_2_18]
Exercise_4_3_1_10.DiagonalFunctor_parts [in Exercise_4_3_1_10]
Exercise_4_3_1_10 [in Exercise_4_3_1_10]
Exercise_3_2_1_7 [in Exercise_3_2_1_7]
Exercise_3_2_1_8 [in Exercise_3_2_1_8]
Exercise_4_5_3_11 [in Exercise_4_5_3_11]
Exercise_4_5_3_13 [in Exercise_4_5_3_13]
Exercise_4_1_2_21 [in Exercise_4_1_2_21]


F

function_prod [in FunctionProduct]
FunctorCategory [in FunctorCategory]
FunctorComposition [in Functor]
FunctorCompositionLemmas [in Functor]
FunctorFromDiscrete [in DiscreteCategoryFunctors]
FunctorIsomorphism [in FunctorIsomorphisms]
FunctorIsomorphism.CategoriesIsomorphic [in FunctorIsomorphisms]
FunctorIsomorphism.FunctorIsInverseOf [in FunctorIsomorphisms]
FunctorIsomorphism.FunctorIsIsomorphism [in FunctorIsomorphisms]
FunctorIsomorphism.FunctorIsomorphismOf [in FunctorIsomorphisms]
FunctorIsomorphism.IsomorphismOfCategories [in FunctorIsomorphisms]
FunctorNaturalEquivalenceLemmas [in NaturalEquivalence]
FunctorNaturalEquivalenceRelation [in NaturalEquivalence]
FunctorProduct [in ProductCategory]
Functors [in Functor]
Functors_Equal [in Functor]
FunctorToIndiscrete [in IndiscreteCategory]
Functor_preserves_isomorphism [in FunctorIsomorphisms]
f_equal_dep [in FEqualDep]


G

Gen [in EquivalenceRelationGenerator]
GeneralizedPathEquivalence [in Schema]
GeneralizedPathsEquivalenceRelation [in Schema]
graph_homomorphisms [in Graph]
graph_equivalence [in Graph]
graph'_homomorphisms [in Graph]
Grothendieck [in Grothendieck]


H

hausdorff [in Hausdorff]
homeomorphic [in Homeomorphism]
HomFunctor [in Hom]
HomFunctor.covariant_contravariant [in Hom]


I

IdentityFunctor [in Functor]
IdentityFunctorLemmas [in Functor]
IdentityNaturalEquivalence [in NaturalEquivalence]
IdentityNaturalTransformation [in NaturalTransformation]
IdentityNaturalTransformationF [in NaturalTransformation]
IdentityNaturalTransformation.FullIdentity [in NaturalTransformation]
IdentityNaturalTransformation.ProofFreeIdentity [in NaturalTransformation]
IdentitySchemaMorphsims [in SchemaMorphism]
identity_composition_lemmas [in CategoryIsomorphisms]
InClass_classOf [in EquivalenceClass]
inclusion [in Topology]
inclusion2 [in Topology]
inclusion3 [in Topology]
IndexedMeetsAndJoins [in Orders]
IndiscreteCategory [in IndiscreteCategory]
indiscrete_topology [in IndiscreteTopology]
InducedFunctor [in DiscreteCategoryFunctors]
InitialTerminal [in InitialTerminalCategory]
InitialTerminal [in SetCategoryFacts]
InitialTerminalFunctors [in InitialTerminalCategory]
InSet_setOf [in EquivalenceSet]
interior [in Interior]
intersection [in Topology]
intersection_lemmas [in Topology]
intersection_union_commute [in Topology]
intersection_cover [in CoveringSpace]
isomorphic_relation [in Isomorphism]


K

Kleisli [in KleisliCategory]
KleisliCoproducts [in KleisliCategoryCoproducts]
KleisliProducts [in KleisliCategoryProducts]


L

left_cone_f_composition_of [in Cone]
left_cone_f_identity_of [in Cone]
left_cone_morphism_of [in Cone]
left_cone_category [in Cone]
le_rel [in NatFacts]
ListFunctor [in ListFunctor]


M

misc [in FEqualDep]
Monad [in Monad]
MonoidAdjunction [in MonoidAdjunction]
MonoidAdjunction.adjunction [in MonoidAdjunction]
MonoidAdjunction.free [in MonoidAdjunction]
MonoidAdjunction.underlying [in MonoidAdjunction]
morphism [in Morphism]
morphism.inverse [in Morphism]
morphism.inverse_compose [in Morphism]


N

NatualNumbersMonoid [in NaturalNumbersMonoid]
NaturalEquivalence [in NaturalEquivalence]
NaturalEquivalenceOfCategories [in NaturalEquivalence]
NaturalIsomorphism [in NaturalEquivalence]
NaturalIsomorphismOfCategories [in NaturalEquivalence]
NaturalIsomorphism.Composition [in NaturalEquivalence]
NaturalIsomorphism.Inverse [in NaturalEquivalence]
NaturalIsomorphism.NaturalIsomorphism [in NaturalEquivalence]
NaturalTransformation [in NaturalTransformation]
NaturalTransformationComposition [in NaturalTransformation]
NaturalTransformationExchangeLaw [in NaturalTransformation]
NaturalTransformationInverse [in NaturalEquivalence]
NaturalTransformations_Equal [in NaturalTransformation]
nat_le_div [in NatOrders]
nat_le_order [in NatOrders]
NTAssociativity [in NaturalTransformation]
NTIdentityFunctor [in NaturalTransformation]
NTIdentityFunctor.left [in NaturalTransformation]
NTIdentityFunctor.right [in NaturalTransformation]


O

Obj [in DiscreteCategoryFunctors]
OppositeCategory [in Duals]
OppositeFunctor [in Duals]
order_product [in OrderProduct]


P

path [in Path]
PathsCategory [in PathsCategory]
PathsFunctor [in PathsFunctor]
PathsFunctor.paths_functor [in PathsFunctor]
path_Equivalence_Theorems [in Schema]
path_Theorems [in Path]
PowerSetFunctor [in PowerSetFunctor]
PowerSetMonad [in PowerSetMonad]
preorder_category.all_preorders [in PreOrderCategory]
preorder_category.single_preorder [in PreOrderCategory]
preorder_category [in PreOrderCategory]
ProductCategory [in ProductCategory]
ProductCategoryFunctors [in ProductCategory]
ProductInducedFunctors [in ProductInducedFunctors]
ProductInducedNaturalTransformations [in ProductInducedFunctors]
PropPreOrder [in PropPreOrder]


R

relation_coproduct [in OrderCoproduct]
right_cone_f_composition_of [in Cone]
right_cone_f_identity_of [in Cone]
right_cone_morphism_of [in Cone]
right_cone_category [in Cone]


S

Schema [in Schema]
SchemaIsomorphismEquivalenceRelation [in Schema]
SchemaMorphismComposition [in SchemaMorphism]
SchemaMorphismCompositionLemmas [in SchemaMorphism]
SchemaMorphismsEquivalent [in SchemaMorphism]
SchemaMorphismsEquivalent_Relation [in SchemaMorphism]
SchemaMorphisms_Equal [in SchemaMorphism]
Schemas [in SchemaMorphism]
Schemas.transferPath [in SchemaMorphism]
set_cat_has_coprod [in SetCategoryFacts]
set_cat_has_prod [in SetCategoryFacts]
sig [in Common]
sig_mor [in Subcategory]
sig_obj [in Subcategory]
sig_obj_mor [in Subcategory]
SliceCategory [in CommaCategory]
SliceCategoryOver [in CommaCategory]
SplitHomFunctor [in Hom]
subset_ensemble_union_intersection [in Topology]
subspace_topology [in SubspaceTopology]
swap [in SwapExercise]
swap_product [in Product]
swap_coproduct [in Coproduct]


T

telescope [in Common]
topology [in Topology]
True [in Common]


U

underlying_graph [in UnderlyingGraph]
unit [in Common]
univ_prod [in SwapExercise]


Z

zero_group [in ZeroGroup]



Constructor Index

A

Add [in Exercise_4_2_3_12]
AddEdge [in Path]
ArbitraryUnion_inJ [in Topology]


B

Base [in Common]
Build_Equivalence [in Isomorphism]


C

Common_existT [in Common]
comparability [in Orders]
Constant [in Exercise_4_2_3_12]


E

eq_dep1_intro [in EqdepFacts_one_variable]
eq_dep_intro [in EqdepFacts_one_variable]
Exercise_4_1_2_31.hf [in Exercise_4_1_2_31]
Exercise_4_1_2_31.gf [in Exercise_4_1_2_31]
Exercise_4_1_2_31.k [in Exercise_4_1_2_31]
Exercise_4_1_2_31.j [in Exercise_4_1_2_31]
Exercise_4_1_2_31.i [in Exercise_4_1_2_31]
Exercise_4_1_2_31.h [in Exercise_4_1_2_31]
Exercise_4_1_2_31.g [in Exercise_4_1_2_31]
Exercise_4_1_2_31.f [in Exercise_4_1_2_31]
Exercise_4_1_2_31.z [in Exercise_4_1_2_31]
Exercise_4_1_2_31.y [in Exercise_4_1_2_31]
Exercise_4_1_2_31.x [in Exercise_4_1_2_31]
Exercise_4_1_2_31.w [in Exercise_4_1_2_31]
Exercise_4_1_2_31.v [in Exercise_4_1_2_31]
Exercise_4_4_1_1.One_Two [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Zero_One [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Two [in Exercise_4_4_1_1]
Exercise_4_4_1_1.One [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Zero [in Exercise_4_4_1_1]
Exercise_4_4_1_5.One_Two [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Zero_One [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Two [in Exercise_4_4_1_5]
Exercise_4_4_1_5.One [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Zero [in Exercise_4_4_1_5]
Exercise_4_4_1_5.i [in Exercise_4_4_1_5]
Exercise_4_4_1_5.h [in Exercise_4_4_1_5]
Exercise_4_4_1_5.g [in Exercise_4_4_1_5]
Exercise_4_4_1_5.c [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a [in Exercise_4_4_1_5]
Exercise_4_4_1_6.f [in Exercise_4_4_1_6]
Exercise_4_4_1_6.s [in Exercise_4_4_1_6]
Exercise_4_2_3_2_continuity_bad.C [in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.B [in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.A [in Exercise_4_2_3_2]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOfAll [in Exercise_4_6_1_5]
Exercise_4_2_4_4.RespectedLawsOfAll [in Exercise_4_2_4_4]
Exercise_5_1_1_3.c [in Exercise_5_1_1_3]
Exercise_5_1_1_3.b [in Exercise_5_1_1_3]
Exercise_5_1_1_3.a [in Exercise_5_1_1_3]
Exercise_4_5_2_12.B [in Exercise_4_5_2_12]
Exercise_4_5_2_12.A [in Exercise_4_5_2_12]
Exercise_3_5_2_4.name [in Exercise_3_5_2_4]
Exercise_3_5_2_4.secretary [in Exercise_3_5_2_4]
Exercise_3_5_2_4.worksIn [in Exercise_3_5_2_4]
Exercise_3_5_2_4.lastName [in Exercise_3_5_2_4]
Exercise_3_5_2_4.firstName [in Exercise_3_5_2_4]
Exercise_3_5_2_4.manager [in Exercise_3_5_2_4]
Exercise_3_5_2_4.compose [in Exercise_3_5_2_4]
Exercise_3_5_2_4.identity [in Exercise_3_5_2_4]
Exercise_3_5_2_4.DepartmentNameString [in Exercise_3_5_2_4]
Exercise_3_5_2_4.LastNameString [in Exercise_3_5_2_4]
Exercise_3_5_2_4.FirstNameString [in Exercise_3_5_2_4]
Exercise_3_5_2_4.Department [in Exercise_3_5_2_4]
Exercise_3_5_2_4.Employee [in Exercise_3_5_2_4]
Exercise_4_6_2_4.LastName [in Exercise_4_6_2_4]
Exercise_4_6_2_4.FirstName [in Exercise_4_6_2_4]
Exercise_4_6_2_4.hasDay [in Exercise_4_6_2_4]
Exercise_4_6_2_4.hasMonth [in Exercise_4_6_2_4]
Exercise_4_6_2_4.hasYear [in Exercise_4_6_2_4]
Exercise_4_6_2_4.actionDescription [in Exercise_4_6_2_4]
Exercise_4_6_2_4.performedBy [in Exercise_4_6_2_4]
Exercise_4_6_2_4.occuredOn [in Exercise_4_6_2_4]
Exercise_4_6_2_4.Month [in Exercise_4_6_2_4]
Exercise_4_6_2_4.Day [in Exercise_4_6_2_4]
Exercise_4_6_2_4.Year [in Exercise_4_6_2_4]
Exercise_4_6_2_4.String [in Exercise_4_6_2_4]
Exercise_4_6_2_4.PersonId [in Exercise_4_6_2_4]
Exercise_4_6_2_4.DateId [in Exercise_4_6_2_4]
Exercise_4_6_2_4.ActionId [in Exercise_4_6_2_4]
Exercise_4_6_2_4.December [in Exercise_4_6_2_4]
Exercise_4_6_2_4.November [in Exercise_4_6_2_4]
Exercise_4_6_2_4.October [in Exercise_4_6_2_4]
Exercise_4_6_2_4.September [in Exercise_4_6_2_4]
Exercise_4_6_2_4.August [in Exercise_4_6_2_4]
Exercise_4_6_2_4.July [in Exercise_4_6_2_4]
Exercise_4_6_2_4.June [in Exercise_4_6_2_4]
Exercise_4_6_2_4.May [in Exercise_4_6_2_4]
Exercise_4_6_2_4.April [in Exercise_4_6_2_4]
Exercise_4_6_2_4.March [in Exercise_4_6_2_4]
Exercise_4_6_2_4.February [in Exercise_4_6_2_4]
Exercise_4_6_2_4.January [in Exercise_4_6_2_4]
Exercise_4_6_2_4.A01 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.P44 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.D13114 [in Exercise_4_6_2_4]


G

gen_trans [in EquivalenceRelationGenerator]
gen_sym [in EquivalenceRelationGenerator]
gen_refl [in EquivalenceRelationGenerator]
gen_underlying [in EquivalenceRelationGenerator]
GPathsEquivalent [in Schema]
G_e [in Exercise_4_1_2_28]
G_v1 [in Exercise_4_1_2_28]
G_v0 [in Exercise_4_1_2_28]


I

identity_dep_refl [in FEqualDep]


M

Multiply [in Exercise_4_2_3_12]


N

Negate [in Exercise_4_2_3_12]
NoEdges [in Path]


O

one [in Exercise_3_1_1_7]


P

PairwiseIntersection_intro [in Topology]
Pos [in Exercise_4_2_3_12]


Q

Quant [in Common]


R

Relation_dec [in Orders]


S

Subtract [in Exercise_4_2_3_12]


T

twoa [in Exercise_3_1_1_7]
twob [in Exercise_3_1_1_7]


Z

zeroa [in Exercise_3_1_1_7]
zerob [in Exercise_3_1_1_7]



Notation Index

C

_ ≅ _ (type_scope) [in CategoryIsomorphisms]
_ ≅ _ [in CategoryIsomorphisms]
_ ≅ _ (type_scope) [in CategoryIsomorphisms]
_ ≅ _ (category_scope) [in CategoryIsomorphisms]
_ ⁻¹ [in CoveringSpace]


E

_ <= _ [in Orders]
_ ~= _ [in EquivalenceSet]
_ ~= _ [in EquivalenceClass]
_ = _ (nat_scope) [in Exercise_3_3_1_9]
_ ~~> _ [in Exercise_4_4_1_1]
_ ~> _ [in Exercise_4_4_1_1]
Paths_f _ [in Exercise_4_4_1_1]
[] [in Exercise_4_4_1_1]
[ _ , .. , _ ] [in Exercise_4_4_1_1]
_ ≃_ _ _ [in Exercise_4_4_1_6]
_ ≤ _ [in Exercise_4_5_1_16]
| _ - _ | [in Exercise_3_4_1_2]
_ ≼ _ [in Exercise_4_5_1_4]
_ ≤ _ [in Exercise_4_5_1_4]
_ ≤ _ [in Exercise_4_6_1_5]
_ <= _ [in Exercise_4_6_1_5]
_ ≤ _ [in Exercise_3_4_2_7]
_ ≤ _ [in Exercise_4_2_4_3]
_ <= _ [in Exercise_4_2_4_3]
_ o _ [in Exercise_3_5_2_4]
_ ≃ _ [in Exercise_3_5_2_4]
[ _ ] [in Exercise_4_6_2_4]
_ ~~~> _ [in Exercise_4_6_2_4]
_ ~~> _ [in Exercise_4_6_2_4]
_ ~~> _ [in Exercise_4_6_2_4]
_ ≤ _ [in Exercise_4_2_1_13]
_ ≤ _ [in Exercise_4_2_1_14]
_ ≤ _ [in Exercise_4_2_1_16]


I

_ <= _ [in Orders]


M

_ ⁻¹ (function_scope) [in Morphism]
_ o _ [in Morphism]


P

_ ≤ _ [in PreOrderCategory]


other

_ ≅ _ (category_scope) [in CategoryIsomorphisms]
_ ▻ (category_scope) [in Cone]
_ ◅ (category_scope) [in Cone]
_ ^ _ (category_scope) [in FunctorCategory]
[ ω ] (category_scope) [in ChainCategory]
[ ∞ ] (category_scope) [in ChainCategory]
[ _ ] (category_scope) [in ChainCategory]
_ ~> _ (category_scope) [in Category]
_ * _ (category_scope) [in ProductCategory]
_ ↓ _ (category_scope) [in CommaCategory]
_ ⁻¹ (function_scope) [in Morphism]
_ ⟨ - , _ ⟩ (functor_scope) [in ProductInducedFunctors]
_ ⟨ _ , - ⟩ (functor_scope) [in ProductInducedFunctors]
_ ▻ (functor_scope) [in Cone]
_ ◅ (functor_scope) [in Cone]
_ o _ (functor_scope) [in Functor]
_ * _ (functor_scope) [in ProductCategory]
π₂ (functor_scope) [in ProductCategory]
π₁ (functor_scope) [in ProductCategory]
_ ⁻¹ (morphism_scope) [in CategoryIsomorphisms]
π₂ (morphism_scope) [in Product]
π₁ (morphism_scope) [in Product]
i₂ (morphism_scope) [in Coproduct]
i₁ (morphism_scope) [in Coproduct]
_ o _ (morphism_scope) [in Category]
_ ⟨ - , _ ⟩ (natural_transformation_scope) [in ProductInducedFunctors]
_ ⟨ _ , - ⟩ (natural_transformation_scope) [in ProductInducedFunctors]
_ o _ (natural_transformation_scope) [in NaturalTransformation]
_ ◇ _ (natural_transformation_scope) [in NaturalTransformation]
( _ | _ ) (nat_scope) [in NatOrders]
π₂ (object_scope) [in Product]
π₁ (object_scope) [in Product]
_ × _ (object_type_scope) [in Product]
_ × _ (object_scope) [in Product]
i₂ (object_scope) [in Coproduct]
i₁ (object_scope) [in Coproduct]
_ ⊔ _ (object_type_scope) [in Coproduct]
_ ⊔ _ (object_scope) [in Coproduct]
_ × _ (old_type_scope) [in SwapExercise]
_ × _ (product_scope) [in SwapExercise]
_ × _ (product_type_scope) [in SwapExercise]
_ * _ (relation_scope) [in OrderProduct]
_ + _ (relation_scope) [in OrderCoproduct]
_ ⁻¹ (topology_scope) [in Topology]
⋂ _ (topology_scope) [in Topology]
⋃ _ (topology_scope) [in Topology]
_ ⊔ _ (type_scope) [in Notations]
_ × _ (type_scope) [in Notations]
_ ↷ _ (type_scope) [in Monoid]
_ × _ (type_scope) [in SwapExercise]
_ ~> _ (type_scope) [in Category]
_ ⁻¹ (type_scope) [in Group]
_ ≅ _ (type_scope) [in Isomorphism]
_ ⊆ _ [in Notations]
_ ∪ _ [in Notations]
_ ∩ _ [in Notations]
_ ∈ _ [in Notations]
_ == _ [in Notations]
_ ⊔ _ [in Morphism]
_ o _ [in Morphism]
_ ↷ _ [in Monoid]
_ ★ _ [in Monoid]
_ -| _ [in Adjoint]
_ ⊣ _ [in Adjoint]
_ ⁻¹ [in Isomorphism]
[in Notations]
∫ _ [in Grothendieck]
π₁ [in SwapExercise]
π₂ [in SwapExercise]



Inductive Index

A

ArbitraryUnion [in Topology]


C

Common_sigT [in Common]
Comparable [in Orders]


E

EquivalenceOf [in EquivalenceRelationGenerator]
eq_dep1 [in EqdepFacts_one_variable]
eq_dep [in EqdepFacts_one_variable]
Exercise_4_1_2_31.Hom_C_v_x [in Exercise_4_1_2_31]
Exercise_4_1_2_31.A [in Exercise_4_1_2_31]
Exercise_4_1_2_31.V [in Exercise_4_1_2_31]
Exercise_4_4_1_1.LinearOrder2Graph_Edge [in Exercise_4_4_1_1]
Exercise_4_4_1_1.LinearOrder2Graph_Vertex [in Exercise_4_4_1_1]
Exercise_4_4_1_5.LinearOrder2Schema_Edge [in Exercise_4_4_1_5]
Exercise_4_4_1_5.LinearOrder2Schema_Vertex [in Exercise_4_4_1_5]
Exercise_4_4_1_5.C_Edge [in Exercise_4_4_1_5]
Exercise_4_4_1_5.C_Vertex [in Exercise_4_4_1_5]
Exercise_4_4_1_6.Loop_Edge [in Exercise_4_4_1_6]
Exercise_4_4_1_6.Loop_Vertex [in Exercise_4_4_1_6]
Exercise_4_2_3_2_continuity_bad.Three [in Exercise_4_2_3_2]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOf [in Exercise_4_6_1_5]
Exercise_4_2_4_4.RespectedLawsOf [in Exercise_4_2_4_4]
Exercise_5_1_1_3.X [in Exercise_5_1_1_3]
Exercise_4_5_2_12.Two [in Exercise_4_5_2_12]
Exercise_3_5_2_4.Arrow [in Exercise_3_5_2_4]
Exercise_3_5_2_4.Node [in Exercise_3_5_2_4]
Exercise_4_6_2_4.morC [in Exercise_4_6_2_4]
Exercise_4_6_2_4.objC [in Exercise_4_6_2_4]
Exercise_4_6_2_4.Months [in Exercise_4_6_2_4]
Exercise_4_6_2_4.ActionIds [in Exercise_4_6_2_4]
Exercise_4_6_2_4.PersonIds [in Exercise_4_6_2_4]
Exercise_4_6_2_4.DateIds [in Exercise_4_6_2_4]
Expression [in Exercise_4_2_3_12]


G

GeneralizedPathsEquivalent [in Schema]
G_Edge [in Exercise_4_1_2_28]
G_Vertex [in Exercise_4_1_2_28]


I

identity_dep [in FEqualDep]


P

PairwiseIntersection [in Topology]
path [in Path]


R

RelationDecidable [in Orders]


T

telescope [in Common]
three [in Exercise_3_1_1_7]
two [in Exercise_3_1_1_7]



Abbreviation Index

C

CategoryOf [in SetCategory]
CategoryOfCategoriesOn [in ComputableCategory]
CoercedEmptySetInitialOf [in SetCategoryFacts]
CoercedFalseInitialOf [in SetCategoryFacts]
CoercedTrueTerminalOf [in SetCategoryFacts]
CoercedUnitTerminalOf [in SetCategoryFacts]


D

DecidableEqDepSet.inj_pairT2 [in Eqdep_dec_one_variable]


E

EmptySetInitialOf [in SetCategoryFacts]
EqdepTheory.inj_pairT2 [in EqdepFacts_one_variable]
equiv_eqex_eqdep [in EqdepFacts_one_variable]
eq_dep_eq__inj_pairT2 [in EqdepFacts_one_variable]
eq_sigS_eq_dep [in EqdepFacts_one_variable]
Exercise_4_6_2_4.Build_RDF [in Exercise_4_6_2_4]


F

FalseInitialOf [in SetCategoryFacts]


I

IndexedCategoryOf [in SetCategory]
IndexedEmptySetInitialOf [in SetCategoryFacts]
IndexedFalseInitialOf [in SetCategoryFacts]
IndexedTInitialOf [in SetCategoryFacts]
IndexedTrueTerminalOf [in SetCategoryFacts]
IndexedTTerminalOf [in SetCategoryFacts]
IndexedUnitTerminalOf [in SetCategoryFacts]
Inj_dep_pairT [in EqdepFacts_one_variable]
Inj_dep_pairS [in EqdepFacts_one_variable]


O

ObjectFunctorTo [in DiscreteCategoryFunctors]


R

relation [in Isomorphism]


T

TrueTerminalOf [in SetCategoryFacts]


U

UnitTerminalOf [in SetCategoryFacts]


other

[in Notations]
[in Exercise_4_5_3_6]
[in Exercise_4_2_3_12]



Definition Index

A

AdjunctionCounit [in AdjointUnit]
AdjunctionUnit [in AdjointUnit]
adjunction_naturality' [in Adjoint]
adjunction_naturality [in Adjoint]
Adjunction2HomAdjunction [in Adjoint]
apply_to_class [in EquivalenceClass]
apply2_to_class [in EquivalenceClass]
ArbitraryIntersection [in Topology]
ArithmeticCategory [in Exercise_4_2_3_12]
ArithmeticGroupoid [in Exercise_4_2_3_12]
ArrowCategory [in CommaCategory]


B

Build_CommaCategory_Morphism' [in CommaCategory]
Build_CommaCategory_Object' [in CommaCategory]


C

C [in Exercise_4_3_1_10]
CategoriesIsomorphic [in FunctorIsomorphisms]
CategoriesNaturallyEquivalent [in NaturalEquivalence]
CategoryInCategoryOfCategories [in ComputableCategory]
CategoryInCategoryOfCategories' [in ComputableCategory]
CategoryOfCategories [in ComputableCategory]
CategoryOfElements [in Grothendieck]
CategoryOfGraphs [in GraphCategory]
CategoryOfGraph's [in GraphCategory]
CategoryOfGroupoids [in Groupoid]
CategoryOfGroups [in GroupCategory]
CategoryOfMonoids [in MonoidCategory]
CategoryOfPreOrders [in PreOrderCategory]
CategoryOfProps [in SetCategory]
CategoryOfPropsFalseInitial [in SetCategoryFacts]
CategoryOfPropsTrueTerminal [in SetCategoryFacts]
CategoryOfSets [in SetCategory]
CategoryOfSetsEmptyInitial [in SetCategoryFacts]
CategoryOfSetsFalseInitial [in SetCategoryFacts]
CategoryOfSetsSingletonTerminal [in SetCategoryFacts]
CategoryOfSetsTrueTerminal [in SetCategoryFacts]
CategoryOfSetsUnitTerminal [in SetCategoryFacts]
CategoryOfTopologies [in TopologyCategory]
CategoryOfTypes [in SetCategory]
CategoryOfTypesEmptyInitial [in SetCategoryFacts]
CategoryOfTypesFalseInitial [in SetCategoryFacts]
CategoryOfTypesSingletonTerminal [in SetCategoryFacts]
CategoryOfTypesTrueTerminal [in SetCategoryFacts]
CategoryOfTypesUnitTerminal [in SetCategoryFacts]
Category_sig_mor_as_sig [in Subcategory]
Category_sig_mor [in Subcategory]
Category_sig_obj_as_sig [in Subcategory]
Category_sig_obj [in Subcategory]
Category_sig [in Subcategory]
ChainCategory [in ChainCategory]
ChainCategory' [in ChainCategory]
classOf [in EquivalenceClass]
Closed [in Topology]
closure [in Closure]
CommaCategory [in CommaCategory]
CommaCategory_Identity [in CommaCategory]
CommaCategory_Compose [in CommaCategory]
CommaCategory_MorphismT [in CommaCategory]
CommaCategory_ObjectT [in CommaCategory]
Common_projT2 [in Common]
Common_projT1 [in Common]
compact [in Compact]
CompleteGraph [in Exercise_3_3_1_5]
compose [in Morphism]
ComposeAdjunctions [in AdjointComposition]
ComposeAdjunctionsUnitMorphism [in AdjointComposition]
ComposeFunctorIsmorphismOf [in FunctorIsomorphisms]
ComposeFunctors [in Functor]
ComposeFunctorsAssociator1 [in NaturalTransformation]
ComposeFunctorsAssociator2 [in NaturalTransformation]
ComposeSchemaMorphisms [in SchemaMorphism]
compose_relation_homomorphisms [in Orders]
compose_graph'_homomorphisms [in Graph]
compose_graph_homomorphisms [in Graph]
compose_monoid_homomorphisms [in Monoid]
compose_group_homomorphisms [in Group]
compose_continuous [in TopologicalContinuity]
compose_path [in Path]
ComputableCategory [in ComputableCategory]
ComputationalGroupOfAutomorphisms [in Exercise_3_2_1_7]
ComputationalGroupOfAutomorphismsAction [in Exercise_3_2_1_11]
ComputationalMonoidOfAutomorphisms [in Exercise_3_2_1_7]
concatenate [in Path]
concatenate' [in Path]
ConnectedComponents [in Exercise_5_1_1_9]
ConnectedComponentsInjectionFunction [in Exercise_5_1_1_9]
ConnectedComponentsProjectionFunctor [in Exercise_5_1_1_9]
ConstantGraph [in Exercise_3_3_1_5]
continuous [in TopologicalContinuity]
continuous_induced_functor [in Exercise_4_2_3_2]
continuous_induced_functor_morphism_of [in Exercise_4_2_3_2]
continuous_induced_functor_object_of [in Exercise_4_2_3_2]
ContravariantHomFunctor [in Hom]
CosliceCategory [in CommaCategory]
CosliceCategoryOver [in CommaCategory]
CounitOf [in Adjoint]
CovariantHomFunctor [in Hom]
cover_open [in OpenCover]


D

dec_rel [in Orders]
DenoteExpression [in Exercise_4_2_3_12]
diagonal_functor_morphism_of [in Exercise_4_3_1_10]
diagonal_functor_object_of [in Exercise_4_3_1_10]
differentClasses [in EquivalenceClass]
differentSets [in EquivalenceSet]
DiscreteCategory [in DiscreteCategory]
DiscreteCategory_Identity [in DiscreteCategory]
DiscreteCategory_Compose [in DiscreteCategory]
DiscreteFunctor [in DiscreteCategoryFunctors]
DiscreteGraph [in Exercise_3_3_1_5]
DiscreteGraph [in Exercise_5_1_1_6]
DiscreteGraphAdjunction [in Exercise_5_1_1_6]
DiscreteGraphFunctor [in Exercise_5_1_1_6]
DiscreteGraphInjection [in Exercise_5_1_1_6]
DiscreteSetFunctor [in DiscreteCategoryFunctors]
DiscreteTopology [in DiscreteTopology]
disjointClasses [in EquivalenceClass]
disjointSets [in EquivalenceSet]
divides [in NatOrders]


E

ensemble2sig [in Topology]
EquivalenceClass_eq_proj [in EquivalenceClass]
EquivalenceClass_eq_lift [in EquivalenceClass]
EquivalenceSet_eq_proj [in EquivalenceSet]
EquivalenceSet_eq_lift [in EquivalenceSet]
Eq_dep_eq [in EqdepFacts_one_variable]
Eq_rect_eq [in EqdepFacts_one_variable]
eq_indd [in EqdepFacts_one_variable]
Exercise_4_1_2_31.Hom_C_x_v [in Exercise_4_1_2_31]
Exercise_4_1_2_31.C [in Exercise_4_1_2_31]
Exercise_4_1_2_31.G [in Exercise_4_1_2_31]
Exercise_3_3_1_9 [in Exercise_3_3_1_9]
Exercise_3_3_1_9' [in Exercise_3_3_1_9]
Exercise_5_3_2_5.ExceptionMonad [in Exercise_5_3_2_5]
Exercise_5_3_2_5.T [in Exercise_5_3_2_5]
Exercise_4_4_1_1.Paths2Path5 [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path4 [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path3 [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path2 [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path1 [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2Path0 [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Paths2 [in Exercise_4_4_1_1]
Exercise_4_4_1_1.f' [in Exercise_4_4_1_1]
Exercise_4_4_1_1.f [in Exercise_4_4_1_1]
Exercise_4_4_1_1.nth_edge_in_loop [in Exercise_4_4_1_1]
Exercise_4_4_1_1.LinearOrder2Graph [in Exercise_4_4_1_1]
Exercise_4_4_1_1.Loop [in Exercise_4_4_1_1]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism5 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism4 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism3 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism2 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism1 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_b_SchemaMorphism0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_2 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_2 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_1 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_2_2 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_1_1 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_path_0_0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices8 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices7 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices6 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices5 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices4 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices3 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices2 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices1 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.b_OnVertices0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism7 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism6 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism5 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism4 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism3 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism2 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism1 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.Exercise_4_4_1_5_a_SchemaMorphism0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_c_1 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_c_0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_c_0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_b_0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_c_c_0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_b_b_0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_path_a_a_0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices8 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices7 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices6 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices5 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices4 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices3 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices2 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices1 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.a_OnVertices0 [in Exercise_4_4_1_5]
Exercise_4_4_1_5.SchemaMorphism_template' [in Exercise_4_4_1_5]
Exercise_4_4_1_5.SchemaMorphism_template [in Exercise_4_4_1_5]
Exercise_4_4_1_5.LinearOrder2Schema [in Exercise_4_4_1_5]
Exercise_4_4_1_5.C [in Exercise_4_4_1_5]
Exercise_4_4_1_6.singleton_to_L0 [in Exercise_4_4_1_6]
Exercise_4_4_1_6.L0_to_singleton [in Exercise_4_4_1_6]
Exercise_4_4_1_6.SingletonSchema [in Exercise_4_4_1_6]
Exercise_4_4_1_6.L [in Exercise_4_4_1_6]
Exercise_4_4_1_6.Loop_Equiv [in Exercise_4_4_1_6]
Exercise_4_4_1_6.count_edges [in Exercise_4_4_1_6]
Exercise_4_6_4_3_G [in Exercise_4_6_4_3]
Exercise_4_6_4_3_G_MorphismOf [in Exercise_4_6_4_3]
Exercise_4_6_4_3_F [in Exercise_4_6_4_3]
Exercise_4_6_4_3_F_MorphismOf [in Exercise_4_6_4_3]
Exercise_4_5_1_14_ex [in Exercise_4_5_1_14]
Exercise_4_5_1_28_ex [in Exercise_4_5_1_28]
Exercise_5_1_4_4.CategoryLeafTable [in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable [in Exercise_5_1_4_4]
Exercise_3_4_1_2_right_relation_not_transitive [in Exercise_3_4_1_2]
Exercise_3_4_1_2_middle_relation_not_reflexive [in Exercise_3_4_1_2]
Exercise_3_4_1_2_left_relation_linear_order [in Exercise_3_4_1_2]
Exercise_3_4_1_2_right_relation [in Exercise_3_4_1_2]
Exercise_3_4_1_2_middle_relation [in Exercise_3_4_1_2]
Exercise_3_4_1_2_left_relation [in Exercise_3_4_1_2]
Exercise_3_4_1_7_R'_not_antisymmetric [in Exercise_3_4_1_7]
Exercise_3_4_1_7_R_not_comparable [in Exercise_3_4_1_7]
Exercise_3_4_1_7_R_partial_order [in Exercise_3_4_1_7]
Exercise_3_4_1_7_R'_preorder [in Exercise_3_4_1_7]
Exercise_3_4_1_8_R4_preorder [in Exercise_3_4_1_8]
Exercise_3_4_1_8_R3_preorder [in Exercise_3_4_1_8]
Exercise_3_4_1_8_R2_preorder [in Exercise_3_4_1_8]
Exercise_3_4_1_8_R1_preorder [in Exercise_3_4_1_8]
Exercise_3_4_1_8_R4 [in Exercise_3_4_1_8]
Exercise_3_4_1_8_R3 [in Exercise_3_4_1_8]
Exercise_3_4_1_8_R2 [in Exercise_3_4_1_8]
Exercise_3_4_1_8_R1 [in Exercise_3_4_1_8]
Exercise_4_2_3_2_continuity_bad.continuous_function_continuous [in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.f [in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.ThreeTopology2 [in Exercise_4_2_3_2]
Exercise_4_2_3_2_continuity_bad.ThreeTopology1 [in Exercise_4_2_3_2]
Exercise_3_3_2_4_SingletonGraphCMonoid [in Exercise_3_3_2_4]
Exercise_4_6_1_5.Exercise_4_2_4_4.MaximalRespectedLawOfFunctor [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.MaximalRespectedLawOfFunctor_MorphismOf [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.maximal_law [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOfFunctor [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOfFunctor_MorphismOf [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.SetOfLaws [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.Jurisdiction [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLandFunctor [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand [in Exercise_4_6_1_5]
Exercise_4_6_1_5.PreOrderedSets [in Exercise_4_6_1_5]
Exercise_4_6_1_5.continuous_induced_functor [in Exercise_4_6_1_5]
Exercise_4_6_1_5.continuous_induced_functor_morphism_of [in Exercise_4_6_1_5]
Exercise_4_6_1_5.continuous_induced_functor_object_of [in Exercise_4_6_1_5]
Exercise_4_2_4_3.LawOfTheLandFunctor [in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand [in Exercise_4_2_4_3]
Exercise_4_2_4_4.MaximalRespectedLawOfFunctor [in Exercise_4_2_4_4]
Exercise_4_2_4_4.MaximalRespectedLawOfFunctor_MorphismOf [in Exercise_4_2_4_4]
Exercise_4_2_4_4.maximal_law [in Exercise_4_2_4_4]
Exercise_4_2_4_4.RespectedLawsOfFunctor [in Exercise_4_2_4_4]
Exercise_4_2_4_4.RespectedLawsOfFunctor_MorphismOf [in Exercise_4_2_4_4]
Exercise_4_2_4_4.SetOfLaws [in Exercise_4_2_4_4]
Exercise_4_2_4_4.Jurisdiction [in Exercise_4_2_4_4]
Exercise_4_5_2_3.diagram_triangle_iso [in Exercise_4_5_2_3]
Exercise_4_5_2_3.CommutativeTriangleOfDiagram [in Exercise_4_5_2_3]
Exercise_4_5_2_3.DiagramOfCommutativeTriangle [in Exercise_4_5_2_3]
Exercise_4_5_2_3.CommutativeTriangleDiagram_MorphismOf [in Exercise_4_5_2_3]
Exercise_4_5_2_3.CommutativeTriangleDiagram_ObjectOf [in Exercise_4_5_2_3]
Exercise_4_5_2_3.nat_eq_dec [in Exercise_4_5_2_3]
Exercise_4_5_2_5.FirstDiagram [in Exercise_4_5_2_5]
Exercise_4_5_2_5.FirstDiagram_helper [in Exercise_4_5_2_5]
Exercise_4_5_2_5.SecondDiagram [in Exercise_4_5_2_5]
Exercise_4_5_2_5.SecondDiagram_MorphismOf [in Exercise_4_5_2_5]
Exercise_4_5_2_5.SecondIndex [in Exercise_4_5_2_5]
Exercise_4_5_2_5.FirstIndex [in Exercise_4_5_2_5]
Exercise_4_5_2_5.NatGroup [in Exercise_4_5_2_5]
Exercise_4_5_2_9.chain_to_C_functor [in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_to_chain_functor [in Exercise_4_5_2_9]
Exercise_4_5_2_9.chain_to_C [in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_to_chain [in Exercise_4_5_2_9]
Exercise_4_5_2_9.C [in Exercise_4_5_2_9]
Exercise_4_5_2_9.C_obj [in Exercise_4_5_2_9]
Exercise_4_5_2_12.sq_to_C_functor [in Exercise_4_5_2_12]
Exercise_4_5_2_12.C_to_sq_functor [in Exercise_4_5_2_12]
Exercise_4_5_2_12.sq_to_C_MorphismOf [in Exercise_4_5_2_12]
Exercise_4_5_2_12.C_to_sq_MorphismOf [in Exercise_4_5_2_12]
Exercise_4_5_2_12.sq_to_C [in Exercise_4_5_2_12]
Exercise_4_5_2_12.C_to_sq [in Exercise_4_5_2_12]
Exercise_4_5_2_12.mor_0_1 [in Exercise_4_5_2_12]
Exercise_4_5_2_12.obj_1 [in Exercise_4_5_2_12]
Exercise_4_5_2_12.obj_0 [in Exercise_4_5_2_12]
Exercise_4_5_2_12.pf_0_le_n [in Exercise_4_5_2_12]
Exercise_4_5_2_12.C [in Exercise_4_5_2_12]
Exercise_5_1_1_9 [in Exercise_5_1_1_9]
Exercise_5_1_1_9_Counit [in Exercise_5_1_1_9]
Exercise_5_1_1_9_Unit [in Exercise_5_1_1_9]
Exercise_2_6_1_6 [in Exercise_2_6_1_6]
Exercise_4_6_2_4.RDF_bad [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_8 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_7 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_6 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_5 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_4 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_3 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_2 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF_1 [in Exercise_4_6_2_4]
Exercise_4_6_2_4.P [in Exercise_4_6_2_4]
Exercise_4_6_2_4.RDF [in Exercise_4_6_2_4]
Exercise_4_6_2_4.I [in Exercise_4_6_2_4]
Exercise_4_6_2_4.Inst_MorphismOf [in Exercise_4_6_2_4]
Exercise_4_6_2_4.Inst_MorphismOf_Gen [in Exercise_4_6_2_4]
Exercise_4_6_2_4.Inst_ObjectOf [in Exercise_4_6_2_4]
Exercise_4_6_2_4.C [in Exercise_4_6_2_4]
Exercise_4_5_3_6_b [in Exercise_4_5_3_6]
Exercise_4_5_3_6_a [in Exercise_4_5_3_6]
Exercise_4_5_3_8_b [in Exercise_4_5_3_8]
Exercise_4_5_3_8_a [in Exercise_4_5_3_8]
Exercise_4_3_1_10_NT [in Exercise_4_3_1_10]
Exercise_4_5_3_11_b [in Exercise_4_5_3_11]
Exercise_4_5_3_11_a [in Exercise_4_5_3_11]
Exercise_4_5_3_13_b [in Exercise_4_5_3_13]
Exercise_4_5_3_13_a [in Exercise_4_5_3_13]
ExtendedConstantGraph [in Exercise_3_3_1_5]
E_4_1_2_33_Functor_8 [in Exercise_4_1_2_33]
E_4_1_2_33_Functor_7 [in Exercise_4_1_2_33]
E_4_1_2_33_Functor_6 [in Exercise_4_1_2_33]
E_4_1_2_33_Functor_5 [in Exercise_4_1_2_33]
E_4_1_2_33_Functor_4 [in Exercise_4_1_2_33]
E_4_1_2_33_Functor_3 [in Exercise_4_1_2_33]
E_4_1_2_33_Functor_2 [in Exercise_4_1_2_33]
E_4_1_2_33_Functor_1 [in Exercise_4_1_2_33]


F

f [in Exercise_3_1_1_7]
FIsomorphismOf [in Exercise_4_1_2_21]
FreeArrowCategory [in Exercise_4_1_2_28]
FreeMonoid [in MonoidAdjunction]
FreeMonoidMorphism [in MonoidAdjunction]
FreeMonoidOn [in MonoidAdjunction]
fst_Functor [in ProductCategory]
FullSubcategory [in Subcategory]
FullSubcategoryInclusionFunctor [in Subcategory]
function_prod [in FunctionProduct]
FunctorCategory [in FunctorCategory]
FunctorFromDiscrete [in DiscreteCategoryFunctors]
FunctorFromInitial [in InitialTerminalCategory]
FunctorFromTerminal [in InitialTerminalCategory]
FunctorIsInverseOf [in FunctorIsomorphisms]
FunctorIsInverseOf1 [in FunctorIsomorphisms]
FunctorIsInverseOf2 [in FunctorIsomorphisms]
FunctorIsIsomorphism [in FunctorIsomorphisms]
FunctorIsomorphismOf_Identity [in FunctorIsomorphisms]
FunctorProduct [in ProductCategory]
FunctorProductFunctorial [in ProductCategory]
FunctorsNaturallyEquivalent [in NaturalEquivalence]
FunctorToIndiscrete [in IndiscreteCategory]
FunctorToTerminal [in Exercise_4_1_2_34]
FunctorToTerminal [in InitialTerminalCategory]


G

G [in Exercise_4_1_2_28]
gcd_9_12 [in Exercise_4_5_1_16]
generateEquivalence [in EquivalenceRelationGenerator]
GraphHomomorphismToGraph'Homomorphism [in Graph]
GraphToGraph' [in Graph]
Graph'HomomorphismToGraphHomomorphism [in Graph]
Graph'ToGraph [in Graph]
GrothendieckCompose [in Grothendieck]
GrothendieckIdentity [in Grothendieck]
GrothendieckProjectionFunctor [in Grothendieck]
GroupHomomorphism [in Group]


H

hausdorff [in Hausdorff]
HomAdjunctionOfCounit [in Adjoint]
HomAdjunctionOfUnit [in Adjoint]
HomAdjunctionOfUnitCounit [in Adjoint]
HomAdjunction2Adjunction [in Adjoint]
HomAdjunction2Adjunction_AMateOf [in Adjoint]
HomFunctor [in Hom]
HomomorphismFromZeroGroup [in ZeroGroup]
HomomorphismToZeroGroup [in ZeroGroup]


I

IdentityFunctor [in Functor]
IdentityNaturalTransformation [in NaturalTransformation]
IdentityNaturalTransformation' [in Exercise_4_3_1_3]
IdentityNaturalTransformation' [in NaturalTransformation]
IdentitySchemaMorphism [in SchemaMorphism]
identity_relation_homomorphism [in Orders]
identity_graph'_homomorphism [in Graph]
identity_graph_homomorphism [in Graph]
identity_monoid_homomorphism [in Monoid]
identity_group_homomorphism [in Group]
identity_is_continuous [in TopologicalContinuity]
image [in Morphism]
InClass_classOf_eq' [in EquivalenceClass]
include_subset [in Topology]
inclusion [in Topology]
IndiscreteCategory [in IndiscreteCategory]
IndiscreteGraph [in Exercise_5_1_1_6]
IndiscreteGraphAdjunction [in Exercise_5_1_1_6]
IndiscreteGraphFunctor [in Exercise_5_1_1_6]
IndiscreteGraphSurjection [in Exercise_5_1_1_6]
IndiscreteTopology [in IndiscreteTopology]
InducedDiscreteFunctor [in DiscreteCategoryFunctors]
InducedProductFstFunctor [in ProductInducedFunctors]
InducedProductFstNaturalTransformation [in ProductInducedFunctors]
InducedProductSndFunctor [in ProductInducedFunctors]
InducedProductSndNaturalTransformation [in ProductInducedFunctors]
InitialCategory [in InitialTerminalCategory]
InitialObject_IsInitialObject [in CategoryObjects]
InitialObject_Object [in CategoryObjects]
Inj_dep_pair [in EqdepFacts_one_variable]
InSet_setOf_eq' [in EquivalenceSet]
interior [in Interior]
IntersectionCover [in CoveringSpace]
InverseNaturalIsomorphism [in NaturalEquivalence]
InverseNaturalIsomorphism_NT [in NaturalEquivalence]
InverseOfFunctor [in FunctorIsomorphisms]
inverse_compose_commutes [in Morphism]
inverse_image [in Morphism]
inverse_map [in Morphism]
inverse_of [in Group]
IsEpimorphism [in CategoryMorphisms]
IsGroupHomomorphism [in Group]
IsInitialObject [in CategoryObjects]
IsInitialObject_InitialObject [in CategoryObjects]
IsInitialObject' [in CategoryObjects]
IsInverseOf [in CategoryIsomorphisms]
IsInverseOf1 [in CategoryIsomorphisms]
IsInverseOf2 [in CategoryIsomorphisms]
IsIsomorphism [in CategoryIsomorphisms]
IsMonomorphism [in CategoryMorphisms]
Isomorphic [in CategoryIsomorphisms]
isomorphic_transitive [in Isomorphism]
isomorphic_symmetric [in Isomorphism]
isomorphic_reflexive [in Isomorphism]
IsomorphismOf_sig [in CategoryIsomorphisms]
IsomorphismOf_sig2 [in CategoryIsomorphisms]
IsTerminalObject [in CategoryObjects]
IsTerminalObject_TerminalObject [in CategoryObjects]
IsTerminalObject' [in CategoryObjects]
is_unique [in Common]
is_injective [in Morphism]
is_ensemble_join [in Orders]
is_ensemble_meet [in Orders]
is_indexed_join [in Orders]
is_indexed_meet [in Orders]
is_join [in Orders]
is_meet [in Orders]
is_commutative [in Monoid]
is_inverse_of [in Group]


K

KleisliCategory [in KleisliCategory]


L

LeftCone [in Cone]
LeftCone_MorphismOf [in Cone]
LeftCone_Compose [in Cone]
LeftCone_Identity [in Cone]
LeftCone_Morphism [in Cone]
LeftIdentityFunctorNaturalTransformation1 [in NaturalTransformation]
LeftIdentityFunctorNaturalTransformation2 [in NaturalTransformation]
LiftConnectedFunctor [in Exercise_5_1_1_9]
LiftConnectedFunctor_Functor [in Exercise_5_1_1_9]
LiftMonoidFunction [in MonoidAdjunction]
ListFunctor [in ListFunctor]
LocallySmallCategory [in Category]


M

MonoidFreeUnderlyingAdjunction [in MonoidAdjunction]
MorphismOf_IsomorphismOf [in FunctorIsomorphisms]


N

NatCategory [in NatCategory]
NaturalEquivalenceInverse [in NaturalEquivalence]
NaturalEquivalenceOf [in NaturalEquivalence]
NaturalEquivalenceOfCategories [in NaturalEquivalence]
NaturalEquivalence_of_NaturalIsomorphism [in NaturalEquivalence]
NaturalIsomorphism_of_NaturalEquivalence [in NaturalEquivalence]
NaturalNumbersMonoid [in NaturalNumbersMonoid]
NIComposeF [in NaturalEquivalence]
NIComposeT [in NaturalEquivalence]
NoEvar [in Category]
notDisjointClasses [in EquivalenceClass]
notDisjointClasses' [in EquivalenceClass]
notDisjointSets [in EquivalenceSet]
notDisjointSets' [in EquivalenceSet]
NTComposeF [in NaturalTransformation]
NTComposeT [in NaturalTransformation]


O

ObFunctor [in Exercise_4_1_2_35]
ObjectFunctor [in DiscreteCategoryFunctors]
ObjectFunctorToProp [in DiscreteCategoryFunctors]
ObjectFunctorToSet [in DiscreteCategoryFunctors]
OmegaCategory [in ChainCategory]
OppositeCategory [in Duals]
OppositeFunctor [in Duals]
opposite_relation [in Orders]


P

PathsCategory [in PathsCategory]
PathsFunctor [in PathsFunctor]
PathsHomomorphism [in PathsFunctor]
PathsHomomorphism_on_edges [in PathsFunctor]
PathsOf [in Path]
path_unique [in Schema]
PowerSetFunctor [in PowerSetFunctor]
PowerSetFunctorOp [in PowerSetFunctor]
PowerSetMonad [in PowerSetMonad]
PreOrderCategory [in PreOrderCategory]
PreOrderedSets [in Exercise_4_2_3_2]
prepend [in Path]
product [in SwapExercise]
ProductCategory [in ProductCategory]
product_of [in SwapExercise]
product_element [in SwapExercise]
projT3 [in Common]
proj1_sig_mor_functor [in Subcategory]
proj1_sig_obj_functor [in Subcategory]
proj1_sig_functor [in Subcategory]
proj3_sig [in Common]


R

Reflexive [in Isomorphism]
relation_product [in OrderProduct]
relation_sum [in OrderCoproduct]
restrict [in Morphism]
restrict_range [in Morphism]
restrict_domain [in Morphism]
RightCone [in Cone]
RightCone_MorphismOf [in Cone]
RightCone_Compose [in Cone]
RightCone_Identity [in Cone]
RightCone_Morphism [in Cone]
RightIdentityFunctorNaturalTransformation1 [in NaturalTransformation]
RightIdentityFunctorNaturalTransformation2 [in NaturalTransformation]


S

sameClass [in EquivalenceClass]
sameSet [in EquivalenceSet]
Same_relation [in Orders]
SchemaIsomorphism [in Schema]
SchemaIsomorphism' [in Schema]
SchemaMorphismsEquivalent [in SchemaMorphism]
SEpimorphism [in Schema]
setOf [in EquivalenceSet]
SetUnderlyingGraphFunctor [in Exercise_5_1_1_6]
sigT_of_sigT2 [in Common]
sig_of_sig2 [in Common]
sig_functor_mor_inv [in Subcategory]
sig_functor_mor [in Subcategory]
sig_functor_obj_inv [in Subcategory]
sig_functor_obj [in Subcategory]
SingletonList [in Exercise_4_3_1_9]
SingletonNaturalTransformation [in Exercise_4_3_1_9]
SInverseOf [in Schema]
SliceCategory [in CommaCategory]
SliceCategoryOver [in CommaCategory]
SliceCategory_Functor [in CommaCategory]
SmallCategory [in Category]
smallest_monoid [in Exercise_3_1_1_7]
SMonomorphism [in Schema]
snd_Functor [in ProductCategory]
Streicher_K_ [in EqdepFacts_one_variable]
Subcategory [in Subcategory]
SubcategoryInclusionFunctor [in Subcategory]
subcover [in OpenCover]
subset_ensemble [in Topology]
sumbool_to_bool [in Common]
sum_function [in Morphism]
swap [in SwapExercise]
swap_iso [in SwapExercise]
swap_types_iso [in SwapExercise]
swap_types [in SwapExercise]
swap_product [in Product]
swap_coproduct [in Coproduct]
Symmetric [in Isomorphism]


T

telescopeOut [in Common]
telescopeOut' [in Common]
TerminalCategory [in InitialTerminalCategory]
TerminalObject_IsTerminalObject [in CategoryObjects]
TerminalObject_Object [in CategoryObjects]
three_monoid [in Exercise_3_1_1_7]
transferPath [in SchemaMorphism]
Transitive [in Isomorphism]


U

UIP_refl_ [in EqdepFacts_one_variable]
UIP_ [in EqdepFacts_one_variable]
UnderlyingGraph [in UnderlyingGraph]
UnderlyingGraph' [in UnderlyingGraph]
UnderlyingPoints [in Exercise_4_2_3_2]
UnderlyingSetOfMonoid [in MonoidAdjunction]
UniformGraph [in Exercise_5_1_1_6]
UniformGraphFunctor [in Exercise_5_1_1_6]
UniformGraphInjection [in Exercise_5_1_1_6]
UniformGraphSurjection [in Exercise_5_1_1_6]
UniqueUpToUniqueIsomorphism [in CategoryObjects]
UniqueUpToUniqueIsomorphism' [in CategoryObjects]
UnitCounitOf [in Adjoint]
UnitOf [in Adjoint]


W

WideSubcategory [in Subcategory]
WideSubcategoryInclusionFunctor [in Subcategory]


Z

ZeroComputationalGroup [in ZeroGroup]
ZeroGroup [in ZeroGroup]



Module Index

D

DecidableEqDep [in Eqdep_dec_one_variable]
DecidableEqDepSet [in Eqdep_dec_one_variable]
DecidableEqDepSet.N [in Eqdep_dec_one_variable]
DecidableSet [in Eqdep_dec_one_variable]
DecidableType [in Eqdep_dec_one_variable]


E

EqdepElimination [in EqdepFacts_one_variable]
EqdepTheory [in EqdepFacts_one_variable]
Exercise_4_1_2_31 [in Exercise_4_1_2_31]
Exercise_5_3_2_3 [in Exercise_5_3_2_3]
Exercise_5_3_2_5 [in Exercise_5_3_2_5]
Exercise_4_4_1_1 [in Exercise_4_4_1_1]
Exercise_4_4_1_5 [in Exercise_4_4_1_5]
Exercise_4_4_1_6 [in Exercise_4_4_1_6]
Exercise_4_4_1_7 [in Exercise_4_4_1_7]
Exercise_5_1_4_4 [in Exercise_5_1_4_4]
Exercise_5_1_4_5 [in Exercise_5_1_4_5]
Exercise_5_1_4_9 [in Exercise_5_1_4_9]
Exercise_4_2_3_2_continuity_bad [in Exercise_4_2_3_2]
Exercise_5_3_3_6 [in Exercise_5_3_3_6]
Exercise_5_3_3_7 [in Exercise_5_3_3_7]
Exercise_4_6_1_5.Exercise_4_2_4_4 [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3 [in Exercise_4_6_1_5]
Exercise_4_6_1_5 [in Exercise_4_6_1_5]
Exercise_4_2_4_3 [in Exercise_4_2_4_3]
Exercise_4_2_4_4 [in Exercise_4_2_4_4]
Exercise_4_5_2_3 [in Exercise_4_5_2_3]
Exercise_4_5_2_5 [in Exercise_4_5_2_5]
Exercise_4_5_2_9 [in Exercise_4_5_2_9]
Exercise_5_1_1_3 [in Exercise_5_1_1_3]
Exercise_4_5_2_12 [in Exercise_4_5_2_12]
Exercise_3_5_2_4 [in Exercise_3_5_2_4]
Exercise_4_6_2_4 [in Exercise_4_6_2_4]
Exercise_4_2_1_10 [in Exercise_4_2_1_10]



Axiom Index

D

DecidableSet.eq_dec [in Eqdep_dec_one_variable]
DecidableSet.U [in Eqdep_dec_one_variable]
DecidableSet.x [in Eqdep_dec_one_variable]
DecidableType.eq_dec [in Eqdep_dec_one_variable]
DecidableType.U [in Eqdep_dec_one_variable]
DecidableType.x [in Eqdep_dec_one_variable]


E

EqdepElimination.eq_rect_eq [in EqdepFacts_one_variable]
Exercise_5_3_2_5.E [in Exercise_5_3_2_5]
Exercise_4_5_2_3.C [in Exercise_4_5_2_3]
Exercise_4_5_2_3.objC [in Exercise_4_5_2_3]
Exercise_4_5_2_5.f [in Exercise_4_5_2_5]
Exercise_4_5_2_5.A [in Exercise_4_5_2_5]
Exercise_4_5_2_5.C [in Exercise_4_5_2_5]
Exercise_4_5_2_5.objC [in Exercise_4_5_2_5]
Exercise_3_5_2_4.Associativity [in Exercise_3_5_2_4]
Exercise_3_5_2_4.RightIdentity [in Exercise_3_5_2_4]
Exercise_3_5_2_4.LeftIdentity [in Exercise_3_5_2_4]
Exercise_3_5_2_4.Rule2 [in Exercise_3_5_2_4]
Exercise_3_5_2_4.Rule1 [in Exercise_3_5_2_4]



Variable Index

A

AdjunctionEquivalences'.F [in Adjoint]
AdjunctionEquivalences'.G [in Adjoint]
AdjunctionEquivalences.F [in Adjoint]
AdjunctionEquivalences.G [in Adjoint]
AdjunctionEquivalences.typeof.adjunction_naturality'T' [in Adjoint]
AdjunctionEquivalences.typeof.adjunction_naturalityT' [in Adjoint]
AdjunctionEquivalences.typeof.adjunction_naturality'T [in Adjoint]
AdjunctionEquivalences.typeof.adjunction_naturalityT [in Adjoint]
AdjunctionEquivalences.typeof.typeof [in Adjoint]
AdjunctionUnit.F [in AdjointUnit]
AdjunctionUnit.G [in AdjointUnit]
Adjunction.COp [in Adjoint]
Adjunction.DOp [in Adjoint]
Adjunction.F [in Adjoint]
Adjunction.FOp [in Adjoint]
Adjunction.G [in Adjoint]
Adjunction.HomCPreFunctor [in Adjoint]
Adjunction.HomDPreFunctor [in Adjoint]
apply1.equiv' [in EquivalenceClass]
apply1.equiv'_Equivalence [in EquivalenceClass]
apply1.equiv0 [in EquivalenceClass]
apply1.E0 [in EquivalenceClass]
apply1.f [in EquivalenceClass]
apply1.f_mor [in EquivalenceClass]
apply1.value' [in EquivalenceClass]
apply1.value0 [in EquivalenceClass]
apply2.equiv' [in EquivalenceClass]
apply2.equiv'_Equivalence [in EquivalenceClass]
apply2.equiv0 [in EquivalenceClass]
apply2.equiv1 [in EquivalenceClass]
apply2.E0 [in EquivalenceClass]
apply2.E1 [in EquivalenceClass]
apply2.f [in EquivalenceClass]
apply2.f_mor [in EquivalenceClass]
apply2.value' [in EquivalenceClass]
apply2.value0 [in EquivalenceClass]
apply2.value1 [in EquivalenceClass]
AssociativityComposition.o0 [in CategoryMorphisms]
AssociativityComposition.o1 [in CategoryMorphisms]
AssociativityComposition.o2 [in CategoryMorphisms]
AssociativityComposition.o3 [in CategoryMorphisms]
AssociativityComposition.o4 [in CategoryMorphisms]


C

category_product.Y [in Product]
category_product.X [in Product]
category_coproduct.Y [in Coproduct]
category_coproduct.X [in Coproduct]
Coercions.F [in NaturalEquivalence]
Coercions.F' [in NaturalEquivalence]
Coercions.G [in NaturalEquivalence]
Coercions.G' [in NaturalEquivalence]
CommaCategory.S [in CommaCategory]
CommaCategory.SortPolymorphic_Helper [in CommaCategory]
CommaCategory.T [in CommaCategory]
compact.T [in Compact]
compact.X [in Compact]
compose.A [in AdjointComposition]
compose.A' [in AdjointComposition]
compose.F [in AdjointComposition]
compose.F' [in AdjointComposition]
compose.G [in AdjointComposition]
compose.G' [in AdjointComposition]
ComputableCategory.I [in ComputableCategory]
ComputableCategory.Index2Cat [in ComputableCategory]
ComputableCategory.Index2Object [in ComputableCategory]
continuous.continuous_identity.Tx [in TopologicalContinuity]
continuous.continuous_identity.X [in TopologicalContinuity]
continuous.continuous_definition.Ty [in TopologicalContinuity]
continuous.continuous_definition.Tx [in TopologicalContinuity]
continuous.continuous_definition.Y [in TopologicalContinuity]
continuous.continuous_definition.X [in TopologicalContinuity]
Corollaries.p [in EqdepFacts_one_variable]
Corollaries.U [in EqdepFacts_one_variable]
covering_space.T [in CoveringSpace]
covering_space.X [in CoveringSpace]
covers.T [in OpenCover]
covers.X [in OpenCover]


D

Dependent_Equality.P [in EqdepFacts_one_variable]
Dependent_Equality.U [in EqdepFacts_one_variable]
description.constructive_definite_description [in EquivalenceSet]
description.constructive_definite_description [in EquivalenceClass]
description.eq_dec [in EquivalenceSet]
description.T [in EquivalenceSet]
description.T [in EquivalenceClass]
DiscreteCategory.DiscreteCategory_Morphism [in DiscreteCategory]
DiscreteCategory.O [in DiscreteCategory]
discrete_topology.X [in DiscreteTopology]
disjoint_union.X [in Topology]


E

EnsemblePreOrder.T [in EnsemblePreOrder]
EnsemblesMeetsAndJoins.leq [in Orders]
EnsemblesMeetsAndJoins.T [in Orders]
EnsemblesMeetsAndJoins.U [in Orders]
EpiMono.S [in SetCategoryFacts]
EqdepDec.A [in Eqdep_dec_one_variable]
EqdepDec.comp [in Eqdep_dec_one_variable]
EqdepDec.eq_dec [in Eqdep_dec_one_variable]
EqdepDec.nu [in Eqdep_dec_one_variable]
EqdepDec.nu_inv [in Eqdep_dec_one_variable]
EqdepDec.nu_constant [in Eqdep_dec_one_variable]
EqdepDec.proj [in Eqdep_dec_one_variable]
EqdepDec.x [in Eqdep_dec_one_variable]
EqdepTheory.Axioms.U [in EqdepFacts_one_variable]
EquivalenceClass.equiv [in EquivalenceClass]
EquivalenceClass.value [in EquivalenceClass]
EquivalenceSet.equiv [in EquivalenceSet]
EquivalenceSet.value [in EquivalenceSet]
Equivalences.p [in EqdepFacts_one_variable]
Equivalences.U [in EqdepFacts_one_variable]
equiv.equiv [in EquivalenceSet]
equiv.equiv [in EquivalenceClass]
equiv.equiv_dec [in EquivalenceSet]
equiv.equiv_Equivalence [in EquivalenceSet]
equiv.equiv_Equivalence [in EquivalenceClass]
equiv.value [in EquivalenceSet]
equiv.value [in EquivalenceClass]
Exercise_4_1_2_31.Hom [in Exercise_4_1_2_31]
Exercise_4_1_2_33.D_2 [in Exercise_4_1_2_33]
Exercise_4_1_2_33.D_3 [in Exercise_4_1_2_33]
Exercise_4_1_2_34.C [in Exercise_4_1_2_34]
Exercise_4_1_2_34.obj [in Exercise_4_1_2_34]
Exercise_4_1_2_35.Sets [in Exercise_4_1_2_35]
Exercise_4_1_2_35.Cat [in Exercise_4_1_2_35]
Exercise_4_3_1_3.F [in Exercise_4_3_1_3]
Exercise_3_2_1_11.X [in Exercise_3_2_1_11]
Exercise_3_2_1_11.Σ [in Exercise_3_2_1_11]
Exercise_3_3_1_5.V [in Exercise_3_3_1_5]
Exercise_5_3_2_5.µ [in Exercise_5_3_2_5]
Exercise_5_3_2_5.η [in Exercise_5_3_2_5]
Exercise_4_4_1_1.part_b.m [in Exercise_4_4_1_1]
Exercise_4_4_1_1.part_b.n [in Exercise_4_4_1_1]
Exercise_4_6_4_3.G_ObjectOf [in Exercise_4_6_4_3]
Exercise_4_6_4_3.c' [in Exercise_4_6_4_3]
Exercise_4_6_4_3.c [in Exercise_4_6_4_3]
Exercise_4_5_1_14.X' [in Exercise_4_5_1_14]
Exercise_4_5_1_14.X [in Exercise_4_5_1_14]
Exercise_4_5_1_28.X' [in Exercise_4_5_1_28]
Exercise_4_5_1_28.X [in Exercise_4_5_1_28]
Exercise_4_3_2_5.FunCSet [in Exercise_4_3_2_5]
Exercise_4_3_2_5.C [in Exercise_4_3_2_5]
Exercise_5_1_4_4.CategoryLeafTable.Hom [in Exercise_5_1_4_4]
Exercise_5_1_4_4.CategoryLeafTable.Ob [in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.tgt [in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.src [in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.A [in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.V [in Exercise_5_1_4_4]
Exercise_5_1_4_4.GraphLeafTable.G [in Exercise_5_1_4_4]
Exercise_3_4_1_7.R' [in Exercise_3_4_1_7]
Exercise_3_4_1_7.R [in Exercise_3_4_1_7]
Exercise_3_4_1_7.S [in Exercise_3_4_1_7]
Exercise_3_4_1_8.finite_set_relation [in Exercise_3_4_1_8]
Exercise_3_4_1_8.finite_set [in Exercise_3_4_1_8]
Exercise_5_3_3_6.µ [in Exercise_5_3_3_6]
Exercise_5_3_3_6.η [in Exercise_5_3_3_6]
Exercise_5_3_3_6.T [in Exercise_5_3_3_6]
Exercise_5_3_3_7.µ [in Exercise_5_3_3_7]
Exercise_5_3_3_7.η [in Exercise_5_3_3_7]
Exercise_5_3_3_7.T [in Exercise_5_3_3_7]
Exercise_4_6_1_5.Exercise_4_2_4_4.maximal_law.SetOfLawsAsProp [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.maximal_law.S [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.RespectedLawsOfPerson [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.LawAsProp [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.Law [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_4.Person [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand.V_LawsAsProp [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand.V_Laws [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawOfTheLand.V [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawsOf [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.Jurisdiction [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.LawAsProp [in Exercise_4_6_1_5]
Exercise_4_6_1_5.Exercise_4_2_4_3.Law [in Exercise_4_6_1_5]
Exercise_3_4_2_7.le [in Exercise_3_4_2_7]
Exercise_3_4_2_7.S [in Exercise_3_4_2_7]
Exercise_4_2_4_3.LawOfTheLand.V_LawsAsProp [in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand.V_Laws [in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawOfTheLand.V [in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawsOf [in Exercise_4_2_4_3]
Exercise_4_2_4_3.Jurisdiction [in Exercise_4_2_4_3]
Exercise_4_2_4_3.LawAsProp [in Exercise_4_2_4_3]
Exercise_4_2_4_3.Law [in Exercise_4_2_4_3]
Exercise_4_2_4_4.maximal_law.SetOfLawsAsProp [in Exercise_4_2_4_4]
Exercise_4_2_4_4.maximal_law.S [in Exercise_4_2_4_4]
Exercise_4_2_4_4.RespectedLawsOfPerson [in Exercise_4_2_4_4]
Exercise_4_2_4_4.LawAsProp [in Exercise_4_2_4_4]
Exercise_4_2_4_4.Law [in Exercise_4_2_4_4]
Exercise_4_2_4_4.Person [in Exercise_4_2_4_4]
Exercise_4_5_2_3.C_obj_trunc [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.h [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.g [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.f [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.c [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.b [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.a [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.c' [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.b' [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.a' [in Exercise_4_5_2_3]
Exercise_4_5_2_3.diagram_to_commutative_triangle.CommutativeTriangleDiagram [in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.h [in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.g [in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.f [in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.c [in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.b [in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.a [in Exercise_4_5_2_3]
Exercise_4_5_2_3.commutative_triangle_to_diagram.T [in Exercise_4_5_2_3]
Exercise_5_1_1_3.β [in Exercise_5_1_1_3]
Exercise_5_1_1_3.f [in Exercise_5_1_1_3]
Exercise_5_1_1_3.M [in Exercise_5_1_1_3]
Exercise_5_1_1_6.uniform.UniformGraphFunctor_MorphismOf [in Exercise_5_1_1_6]
Exercise_5_1_1_6.uniform.edge_set [in Exercise_5_1_1_6]
Exercise_5_1_1_9.p [in Exercise_5_1_1_9]
Exercise_5_1_1_9.Disc [in Exercise_5_1_1_9]
Exercise_4_1_1_13.Grph [in Exercise_4_1_1_13]
Exercise_4_1_1_14.Grph [in Exercise_4_1_1_14]
Exercise_2_6_1_6.X [in Exercise_2_6_1_6]
Exercise_2_6_1_6.I [in Exercise_2_6_1_6]
Exercise_4_6_2_4.Year_2013 [in Exercise_4_6_2_4]
Exercise_4_2_1_14.C [in Exercise_4_2_1_14]
Exercise_4_2_1_16.C [in Exercise_4_2_1_16]
Exercise_4_5_3_6.ℙX [in Exercise_4_5_3_6]
Exercise_4_5_3_6.X [in Exercise_4_5_3_6]
Exercise_4_5_3_8.Grp [in Exercise_4_5_3_8]
Exercise_4_3_1_10.f [in Exercise_4_3_1_10]
Exercise_4_3_1_10.Y [in Exercise_4_3_1_10]
Exercise_4_3_1_10.X [in Exercise_4_3_1_10]
Exercise_3_2_1_7.S [in Exercise_3_2_1_7]
Exercise_4_5_3_11.C [in Exercise_4_5_3_11]
Exercise_4_5_3_13.S [in Exercise_4_5_3_13]
Exercise_4_5_3_13.K [in Exercise_4_5_3_13]
Exercise_4_1_2_21.F [in Exercise_4_1_2_21]


F

FunctorFromDiscrete.FunctorFromDiscrete_MorphismOf [in DiscreteCategoryFunctors]
FunctorFromDiscrete.O [in DiscreteCategoryFunctors]
FunctorFromDiscrete.objOf [in DiscreteCategoryFunctors]
FunctorToIndiscrete.O [in IndiscreteCategory]
FunctorToIndiscrete.objOf [in IndiscreteCategory]
Functor_preserves_isomorphism.F [in FunctorIsomorphisms]


G

GeneralizedPathEquivalence.S [in Schema]
GeneralizedPathsEquivalenceRelation.S [in Schema]
Gen.A [in EquivalenceRelationGenerator]
Gen.equiv [in EquivalenceRelationGenerator]
Grothendieck.F [in Grothendieck]


H

hausdorff.T [in Hausdorff]
hausdorff.X [in Hausdorff]
homeomorphic.Tx [in Homeomorphism]
homeomorphic.Ty [in Homeomorphism]
homeomorphic.X [in Homeomorphism]
homeomorphic.Y [in Homeomorphism]
HomFunctor.COp [in Hom]


I

IdentityNaturalEquivalence.F [in NaturalEquivalence]
IdentityNaturalTransformationF.F [in NaturalTransformation]
IdentityNaturalTransformationF.G [in NaturalTransformation]
IdentityNaturalTransformation.FullIdentity.F [in NaturalTransformation]
IdentityNaturalTransformation.ProofFreeIdentity.FMO [in NaturalTransformation]
IdentityNaturalTransformation.ProofFreeIdentity.FOO [in NaturalTransformation]
IdentitySchemaMorphsims.C [in SchemaMorphism]
IdentitySchemaMorphsims.D [in SchemaMorphism]
InClass_classOf.C_Equivalence [in EquivalenceClass]
InClass_classOf.C [in EquivalenceClass]
InClass_classOf.equiv [in EquivalenceClass]
InClass_classOf.value [in EquivalenceClass]
inclusion.T [in Topology]
inclusion2.E [in Topology]
inclusion2.X [in Topology]
inclusion3.X [in Topology]
IndexedMeetsAndJoins.Index [in Orders]
IndexedMeetsAndJoins.IndexToSet [in Orders]
IndexedMeetsAndJoins.leq [in Orders]
IndexedMeetsAndJoins.T [in Orders]
IndiscreteCategory.O [in IndiscreteCategory]
indiscrete_topology.X [in IndiscreteTopology]
InducedFunctor.f [in DiscreteCategoryFunctors]
InducedFunctor.O [in DiscreteCategoryFunctors]
InSet_setOf.C_Equivalence [in EquivalenceSet]
InSet_setOf.equiv_dec [in EquivalenceSet]
InSet_setOf.C [in EquivalenceSet]
InSet_setOf.equiv [in EquivalenceSet]
InSet_setOf.value [in EquivalenceSet]
intersection_lemmas.X [in Topology]
intersection_union_commute.C' [in Topology]
intersection_union_commute.C [in Topology]
intersection_union_commute.X [in Topology]
intersection_cover.C' [in CoveringSpace]
intersection_cover.C [in CoveringSpace]
intersection_cover.T [in CoveringSpace]
intersection_cover.X [in CoveringSpace]
intersection.C [in Topology]
intersection.C' [in Topology]
intersection.X [in Topology]


K

KleisliCoproducts.KT [in KleisliCategoryCoproducts]
KleisliProducts.KT [in KleisliCategoryProducts]
Kleisli.µ [in KleisliCategory]
Kleisli.η [in KleisliCategory]


L

left_cone_f_composition_of.G [in Cone]
left_cone_f_composition_of.F [in Cone]
left_cone_morphism_of.F [in Cone]
left_cone_category.obj [in Cone]


M

morphism.inverse_compose.g [in Morphism]
morphism.inverse_compose.f [in Morphism]
morphism.inverse_compose.Z [in Morphism]
morphism.inverse_compose.Y [in Morphism]
morphism.inverse_compose.X [in Morphism]
morphism.inverse.X [in Morphism]
morphism.inverse.Y [in Morphism]


N

NaturalEquivalence.F [in NaturalEquivalence]
NaturalEquivalence.G [in NaturalEquivalence]
NaturalIsomorphism.Composition.F [in NaturalEquivalence]
NaturalIsomorphism.Composition.F' [in NaturalEquivalence]
NaturalIsomorphism.Composition.F'' [in NaturalEquivalence]
NaturalIsomorphism.Composition.G [in NaturalEquivalence]
NaturalIsomorphism.Composition.G' [in NaturalEquivalence]
NaturalIsomorphism.Inverse.F [in NaturalEquivalence]
NaturalIsomorphism.Inverse.G [in NaturalEquivalence]
NaturalIsomorphism.NaturalIsomorphism.F [in NaturalEquivalence]
NaturalIsomorphism.NaturalIsomorphism.G [in NaturalEquivalence]
NaturalTransformationComposition.F [in NaturalTransformation]
NaturalTransformationComposition.F' [in NaturalTransformation]
NaturalTransformationComposition.F'' [in NaturalTransformation]
NaturalTransformationComposition.G [in NaturalTransformation]
NaturalTransformationComposition.G' [in NaturalTransformation]
NaturalTransformationExchangeLaw.F [in NaturalTransformation]
NaturalTransformationExchangeLaw.F' [in NaturalTransformation]
NaturalTransformationExchangeLaw.G [in NaturalTransformation]
NaturalTransformationExchangeLaw.G' [in NaturalTransformation]
NaturalTransformationExchangeLaw.H [in NaturalTransformation]
NaturalTransformationExchangeLaw.H' [in NaturalTransformation]
NaturalTransformationExchangeLaw.T [in NaturalTransformation]
NaturalTransformationExchangeLaw.T' [in NaturalTransformation]
NaturalTransformationExchangeLaw.U [in NaturalTransformation]
NaturalTransformationExchangeLaw.U' [in NaturalTransformation]
NaturalTransformationInverse.F [in NaturalEquivalence]
NaturalTransformationInverse.G [in NaturalEquivalence]
NaturalTransformationInverse.T [in NaturalEquivalence]
NaturalTransformation.F [in NaturalTransformation]
NaturalTransformation.G [in NaturalTransformation]
NTAssociativity.F [in NaturalTransformation]
NTAssociativity.F0 [in NaturalTransformation]
NTAssociativity.F1 [in NaturalTransformation]
NTAssociativity.G [in NaturalTransformation]
NTAssociativity.H [in NaturalTransformation]
NTIdentityFunctor.left.F [in NaturalTransformation]
NTIdentityFunctor.right.F [in NaturalTransformation]


O

OppositeFunctor.COp [in Duals]
OppositeFunctor.DOp [in Duals]
OppositeFunctor.F [in Duals]


P

PathsCategory.E [in PathsCategory]
PathsCategory.V [in PathsCategory]
PathsFunctor.paths_functor.f [in PathsFunctor]
PathsFunctor.paths_functor.G' [in PathsFunctor]
PathsFunctor.paths_functor.G [in PathsFunctor]
path_Equivalence_Theorems.S [in Schema]
path_Theorems.E [in Path]
path_Theorems.V [in Path]
path.E [in Path]
path.functionOf [in Path]
path.typeOf [in Path]
path.V [in Path]
PowerSetMonad.µ [in PowerSetMonad]
PowerSetMonad.η [in PowerSetMonad]
ProductInducedFunctors.F [in ProductInducedFunctors]
ProductInducedNaturalTransformations.F [in ProductInducedFunctors]


R

right_cone_f_composition_of.G [in Cone]
right_cone_f_composition_of.F [in Cone]
right_cone_morphism_of.F [in Cone]
right_cone_category.obj [in Cone]


S

SchemaIsomorphismEquivalenceRelation.C [in Schema]
SchemaIsomorphismEquivalenceRelation.d [in Schema]
SchemaIsomorphismEquivalenceRelation.d' [in Schema]
SchemaIsomorphismEquivalenceRelation.s [in Schema]
SchemaMorphismCompositionLemmas.B [in SchemaMorphism]
SchemaMorphismCompositionLemmas.C [in SchemaMorphism]
SchemaMorphismCompositionLemmas.D [in SchemaMorphism]
SchemaMorphismCompositionLemmas.E [in SchemaMorphism]
SchemaMorphismComposition.B [in SchemaMorphism]
SchemaMorphismComposition.C [in SchemaMorphism]
SchemaMorphismComposition.D [in SchemaMorphism]
SchemaMorphismComposition.E [in SchemaMorphism]
SchemaMorphismsEquivalent_Relation.E [in SchemaMorphism]
SchemaMorphismsEquivalent_Relation.D [in SchemaMorphism]
SchemaMorphismsEquivalent_Relation.C [in SchemaMorphism]
SchemaMorphismsEquivalent.C [in SchemaMorphism]
SchemaMorphismsEquivalent.D [in SchemaMorphism]
SchemaMorphismsEquivalent.F [in SchemaMorphism]
SchemaMorphismsEquivalent.G [in SchemaMorphism]
Schemas.C [in SchemaMorphism]
Schemas.D [in SchemaMorphism]
Schemas.transferPath.pathOf [in SchemaMorphism]
Schemas.transferPath.vertexOf [in SchemaMorphism]
Schema.C [in Schema]
sig_mor.Pcompose [in Subcategory]
sig_mor.Pidentity [in Subcategory]
sig_mor.Pmor [in Subcategory]
sig_obj.Pobj [in Subcategory]
sig_obj_mor.Pcompose [in Subcategory]
sig_obj_mor.Pidentity [in Subcategory]
sig_obj_mor.Pmor [in Subcategory]
sig_obj_mor.Pobj [in Subcategory]
SliceCategoryOver.a [in CommaCategory]
SliceCategory.a [in CommaCategory]
SliceCategory.B [in CommaCategory]
SliceCategory.S [in CommaCategory]
SplitHomFunctor.COp [in Hom]
subset_ensemble_union_intersection.U [in Topology]
subset_ensemble_union_intersection.X [in Topology]
subspace_topology.P [in SubspaceTopology]
subspace_topology.T [in SubspaceTopology]
subspace_topology.X [in SubspaceTopology]


T

topology.X [in Topology]


U

univ_prod.Y [in SwapExercise]
univ_prod.X [in SwapExercise]



Library Index

A

Adjoint
AdjointComposition
AdjointUnit


C

Category
CategoryIsomorphisms
CategoryMorphisms
CategoryObjects
ChainCategory
Closure
CommaCategory
Common
Compact
ComputableCategory
Cone
Coproduct
CoveringSpace


D

DiscreteCategory
DiscreteCategoryFunctors
DiscreteTopology
Duals


E

EnsemblePreOrder
EqdepFacts_one_variable
Eqdep_dec_one_variable
EquivalenceClass
EquivalenceRelationGenerator
EquivalenceSet
Exercise_4_3_2_5
Exercise_4_5_2_3
Exercise_4_5_2_5
Exercise_3_3_1_10
Exercise_5_3_2_3
Exercise_4_5_2_9
Exercise_5_3_2_5
Exercise_4_5_1_28
Exercise_4_2_3_2
Exercise_3_1_1_7
Exercise_3_3_1_5
Exercise_3_3_1_9
Exercise_4_1_1_5
Exercise_3_2_1_11
Exercise_4_3_1_3
Exercise_4_3_1_10
Exercise_4_1_1_6
Exercise_4_5_3_11
Exercise_3_2_1_14
Exercise_4_5_3_13
Exercise_4_5_1_4
Exercise_5_1_1_3
Exercise_4_3_1_9
Exercise_5_1_1_6
Exercise_3_5_2_12
Exercise_3_5_2_13
Exercise_5_1_1_9
Exercise_3_5_2_18
Exercise_3_4_2_7
Exercise_4_2_1_10
Exercise_5_1_4_4
Exercise_5_1_4_5
Exercise_4_2_1_13
Exercise_4_2_1_14
Exercise_4_2_1_16
Exercise_5_1_4_9
Exercise_4_6_2_4
Exercise_4_5_2_12
Exercise_4_1_2_21
Exercise_4_1_2_28
Exercise_2_6_1_5
Exercise_4_1_2_29
Exercise_2_6_1_6
Exercise_3_4_1_2
Exercise_4_1_1_13
Exercise_3_2_1_7
Exercise_4_1_1_14
Exercise_3_2_1_8
Exercise_3_4_1_7
Exercise_3_4_1_8
Exercise_4_4_1_1
Exercise_4_5_3_6
Exercise_4_1_2_30
Exercise_4_5_3_8
Exercise_4_1_2_31
Exercise_4_4_1_5
Exercise_4_4_1_6
Exercise_4_1_2_33
Exercise_5_3_3_6
Exercise_4_4_1_7
Exercise_4_1_2_34
Exercise_5_3_3_7
Exercise_4_6_1_5
Exercise_4_1_2_35
Exercise_4_5_1_14
Exercise_4_5_1_16
Exercise_4_2_4_3
Exercise_4_2_3_12
Exercise_3_3_2_4
Exercise_4_2_4_4
Exercise_3_5_2_4
Exercise_4_6_4_3


F

FEqualDep
FunctionProduct
Functor
FunctorCategory
FunctorIsomorphisms


G

Graph
GraphCategory
Grothendieck
Group
GroupCategory
Groupoid


H

Hausdorff
Hom
Homeomorphism


I

IndiscreteCategory
IndiscreteTopology
InitialTerminalCategory
Interior
Isomorphism


K

KleisliCategory
KleisliCategoryCoproducts
KleisliCategoryProducts


L

ListFunctor


M

Monad
Monoid
MonoidAdjunction
MonoidCategory
Morphism


N

NatCategory
NatFacts
NatOrders
NaturalEquivalence
NaturalNumbersMonoid
NaturalTransformation
Notations


O

OpenCover
OrderCoproduct
OrderProduct
Orders


P

Path
PathsCategory
PathsFunctor
PowerSetFunctor
PowerSetMonad
PreOrderCategory
Product
ProductCategory
ProductInducedFunctors
PropPreOrder


S

Schema
SchemaMorphism
SetCategory
SetCategoryFacts
Subcategory
SubspaceTopology
SwapExercise


T

TopologicalContinuity
Topology
TopologyCategory


U

UnderlyingGraph


Z

ZeroGroup



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 (2527 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 (101 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 (207 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 (70 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 (395 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 (273 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 (116 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 (106 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 (41 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 (30 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 (571 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 (33 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 (19 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 (406 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 (159 entries)

This page has been generated by coqdoc