| 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 | (463 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 | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 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 | (82 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 | (49 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 | (4 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 | (141 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 | (2 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 | (20 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 | (108 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 | (37 entries) |
Global Index
A
A [definition, in CT.Algebra.Lattice]Ab [definition, in CT.Instance.Algebra.Ab]
Ab [library]
AbelianGroup [record, in CT.Algebra.AbelianGroup]
AbelianGroup [library]
abelian_commutativity [projection, in CT.Algebra.AbelianGroup]
absorption_2 [projection, in CT.Algebra.Lattice]
absorption_1 [projection, in CT.Algebra.Lattice]
ab_e_is_ba_e [lemma, in CT.Algebra.Group]
ab_group_hom_id [definition, in CT.Algebra.AbelianGroup]
ab_group_hom_composition_assoc [definition, in CT.Algebra.AbelianGroup]
ab_group_hom_eq [definition, in CT.Algebra.AbelianGroup]
ab_group_hom_composition [definition, in CT.Algebra.AbelianGroup]
Algebra [library]
Algebra [library]
antisymmetric [projection, in CT.Order.PartiallyOrderedSet]
ArrowCategory [definition, in CT.Instance.Category.ArrowCategory]
ArrowCategory [section, in CT.Instance.Category.ArrowCategory]
ArrowCategory [library]
ArrowCategory.C [variable, in CT.Instance.Category.ArrowCategory]
assoc [projection, in CT.Category]
assoc_sym [projection, in CT.Category]
Automata [library]
Automata [library]
B
basepoint [projection, in CT.Algebra.PointedSet]Bifunctor [definition, in CT.Instance.Functor.Bifunctor]
Bifunctor [library]
bimap [definition, in CT.Instance.Functor.Bifunctor]
BinaryProduct [record, in CT.BinaryProduct]
BinaryProduct [library]
BinaryProduct [library]
bind [definition, in CT.Monad]
bin_prod_unique [projection, in CT.BinaryProduct]
bin_prod_comp2 [projection, in CT.BinaryProduct]
bin_prod_comp1 [projection, in CT.BinaryProduct]
bin_prod_mor [projection, in CT.BinaryProduct]
BooleanAlgebra [record, in CT.Algebra.BooleanAlgebra]
BooleanAlgebra [library]
C
Cat [definition, in CT.Instance.Category.Cat]Cat [library]
Category [record, in CT.Category]
Category [library]
Category [library]
Category [library]
Category [library]
Category [library]
CategoryEquivalence [section, in CT.Instance.Category.Equivalence]
CategoryEquivalence [record, in CT.Instance.Category.Equivalence]
CategoryEquivalenceReflexivity [definition, in CT.Instance.Category.Equivalence]
CategoryEquivalenceSymmetry [lemma, in CT.Instance.Category.Equivalence]
CategoryEquivalenceTransitivity [lemma, in CT.Instance.Category.Equivalence]
CategoryEquivalence.CategoryEquivalenceReflexivity [section, in CT.Instance.Category.Equivalence]
CategoryEquivalence.CategoryEquivalenceSymmetry [section, in CT.Instance.Category.Equivalence]
CategoryEquivalence.CategoryEquivalenceTransitivity [section, in CT.Instance.Category.Equivalence]
category_equiv_refl_nat_iso [definition, in CT.Instance.Category.Equivalence]
ceq_nat_iso2 [projection, in CT.Instance.Category.Equivalence]
ceq_nat_iso1 [projection, in CT.Instance.Category.Equivalence]
CommaCategory [section, in CT.Instance.Category.CommaCategory]
CommaCategory [library]
CommaCategoryMor [record, in CT.Instance.Category.CommaCategory]
CommaCategoryOb [record, in CT.Instance.Category.CommaCategory]
CommaCategory.C [variable, in CT.Instance.Category.CommaCategory]
CommaCategory.D [variable, in CT.Instance.Category.CommaCategory]
CommaCategory.E [variable, in CT.Instance.Category.CommaCategory]
CommaCategory.f [variable, in CT.Instance.Category.CommaCategory]
CommaCategory.g [variable, in CT.Instance.Category.CommaCategory]
comma_mor_law [projection, in CT.Instance.Category.CommaCategory]
comma_gamma [projection, in CT.Instance.Category.CommaCategory]
comma_beta [projection, in CT.Instance.Category.CommaCategory]
comma_a_b [projection, in CT.Instance.Category.CommaCategory]
comma_b [projection, in CT.Instance.Category.CommaCategory]
comma_a [projection, in CT.Instance.Category.CommaCategory]
comp [projection, in CT.Category]
ComposeFunctor [definition, in CT.Instance.Functor.ComposeFunctor]
ComposeFunctor [library]
Composition [library]
comp_identity_left [lemma, in CT.Instance.Functor.IdentityFunctor]
comp_identity_right [lemma, in CT.Instance.Functor.IdentityFunctor]
comp_identity_identity [lemma, in CT.Instance.Functor.IdentityFunctor]
condB [projection, in CT.Algebra.BooleanAlgebra]
ConstantFunctor [definition, in CT.Instance.Functor.ConstantFunctor]
ConstantFunctor [library]
ContravariantFunctor [definition, in CT.Instance.Functor.ContravariantFunctor]
ContravariantFunctor [library]
Coq [library]
CoqListEtaNT [definition, in CT.Instance.Coq.Monad]
CoqListFunctor [definition, in CT.Instance.Coq.Functor]
CoqListMonad [definition, in CT.Instance.Coq.Monad]
CoqListMonad [section, in CT.Instance.Coq.Monad]
CoqListMuNT [definition, in CT.Instance.Coq.Monad]
CoqOptionEtaNT [definition, in CT.Instance.Coq.Monad]
CoqOptionFunctor [definition, in CT.Instance.Coq.Functor]
CoqOptionMonad [definition, in CT.Instance.Coq.Monad]
CoqOptionMonad [section, in CT.Instance.Coq.Monad]
CoqOptionMuNT [definition, in CT.Instance.Coq.Monad]
CoqProp [definition, in CT.Instance.Coq.Category]
CoqProp_has_products [lemma, in CT.Instance.Coq.BinaryProduct]
CoqProp_product [definition, in CT.Instance.Coq.BinaryProduct]
CoqSet [definition, in CT.Instance.Coq.Category]
CoqSet_has_products [lemma, in CT.Instance.Coq.BinaryProduct]
CoqSet_product [definition, in CT.Instance.Coq.BinaryProduct]
CoqType [definition, in CT.Instance.Coq.Category]
CoqType_has_products [lemma, in CT.Instance.Coq.BinaryProduct]
CoqType_product [definition, in CT.Instance.Coq.BinaryProduct]
D
delta [projection, in CT.Automata.Moore]delta [projection, in CT.Automata.Mealy]
dEpsilon [constructor, in CT.Language.Dyck]
dInd [constructor, in CT.Language.Dyck]
Dyck [inductive, in CT.Language.Dyck]
Dyck [library]
dyck_must_start_l [lemma, in CT.Language.Dyck]
E
element [projection, in CT.Algebra.Lattice]Endofunctor [definition, in CT.Instance.Functor.Endofunctor]
Endofunctor [library]
EndofunctorCategory [definition, in CT.Instance.Category.FunctorCategory]
Equivalence [library]
eta [projection, in CT.Monad]
exist_injective [lemma, in CT.Instance.Category.ArrowCategory]
F
f [projection, in CT.Algebra.Lattice]F [projection, in CT.Instance.Category.Equivalence]
FaithfulFunctor [definition, in CT.Instance.Functor.FaithfulFunctor]
FaithfulFunctor [section, in CT.Instance.Functor.FaithfulFunctor]
FaithfulFunctor [library]
FaithfulFunctor.F [variable, in CT.Instance.Functor.FaithfulFunctor]
FAlgebra [record, in CT.Instance.Functor.FAlgebra]
FAlgebra [section, in CT.Instance.Functor.FAlgebra]
FAlgebra [library]
FA_alpha [projection, in CT.Instance.Functor.FAlgebra]
FA_ob [projection, in CT.Instance.Functor.FAlgebra]
from [projection, in CT.Isomorphism]
FullFunctor [definition, in CT.Instance.Functor.FullFunctor]
FullFunctor [section, in CT.Instance.Functor.FullFunctor]
FullFunctor [library]
FullFunctor.F [variable, in CT.Instance.Functor.FullFunctor]
FullyFaithfulFunctor [definition, in CT.Instance.Functor.FullyFaithfulFunctor]
FullyFaithfulFunctor [section, in CT.Instance.Functor.FullyFaithfulFunctor]
FullyFaithfulFunctor [library]
FullyFaithfulFunctor.F [variable, in CT.Instance.Functor.FullyFaithfulFunctor]
Functor [record, in CT.Functor]
Functor [library]
Functor [library]
Functor [library]
FunctorCategory [definition, in CT.Instance.Category.FunctorCategory]
FunctorCategory [library]
functor_pres_iso [lemma, in CT.Functor]
functor_comp_assoc [lemma, in CT.Instance.Functor.ComposeFunctor]
F_eq [lemma, in CT.Functor]
F_comp_law [projection, in CT.Functor]
F_id_law [projection, in CT.Functor]
F_mor [projection, in CT.Functor]
F_ob [projection, in CT.Functor]
f_Y [projection, in CT.Automata.Moore]
f_Sigma [projection, in CT.Automata.Moore]
f_Q [projection, in CT.Automata.Moore]
f_Y [projection, in CT.Automata.Mealy]
f_Sigma [projection, in CT.Automata.Mealy]
f_Q [projection, in CT.Automata.Mealy]
G
G [projection, in CT.Instance.Category.Equivalence]Geometry [record, in CT.Geometry.Projective]
Geometry [library]
geom_refl [projection, in CT.Geometry.Projective]
geom_symm [projection, in CT.Geometry.Projective]
geom_incidence [projection, in CT.Geometry.Projective]
geom_point [projection, in CT.Geometry.Projective]
group [projection, in CT.Algebra.Rng]
Group [record, in CT.Algebra.Group]
group [projection, in CT.Algebra.Ring]
group [projection, in CT.Algebra.AbelianGroup]
Group [library]
GroupCategory [definition, in CT.Instance.Category.GroupCategory]
GroupCategory [library]
GroupHomomorphism [definition, in CT.Algebra.Group]
group_hom_pres_inverse [lemma, in CT.Algebra.Group]
group_equals_one_implies_inverse [lemma, in CT.Algebra.Group]
group_commutative_one [lemma, in CT.Algebra.Group]
group_hom_pres_id [lemma, in CT.Algebra.Group]
group_hom_id [definition, in CT.Algebra.Group]
group_hom_composition_assoc [definition, in CT.Algebra.Group]
group_hom_eq [definition, in CT.Algebra.Group]
group_hom_composition [definition, in CT.Algebra.Group]
group_commutative_conj [lemma, in CT.Algebra.Group]
group_squared_identity [lemma, in CT.Algebra.Group]
group_cancel_right [lemma, in CT.Algebra.Group]
group_cancel_left [lemma, in CT.Algebra.Group]
group_inverse_of_product [lemma, in CT.Algebra.Group]
group_inverse_unique [lemma, in CT.Algebra.Group]
group_inverse_inverse [lemma, in CT.Algebra.Group]
group_identity_unique [lemma, in CT.Algebra.Group]
group_unique_unop [lemma, in CT.Algebra.Group]
Grp [definition, in CT.Instance.Algebra.Grp]
Grp [library]
gr_inverse_right [projection, in CT.Algebra.Group]
gr_inverse_left [projection, in CT.Algebra.Group]
H
has_products [definition, in CT.BinaryProduct]HCNaturalTransformation [definition, in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HCNaturalTransformation [section, in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HCNaturalTransformation [library]
HCNaturalTransformation.epsilon [variable, in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HCNaturalTransformation.JF [variable, in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HCNaturalTransformation.KG [variable, in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HCNaturalTransformation.mu [variable, in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HomFunctor [section, in CT.Instance.Functor.HomFunctor]
HomFunctor [library]
HomFunctor.F [variable, in CT.Instance.Functor.HomFunctor]
I
I [projection, in CT.Instance.Category.Monoidal]id [projection, in CT.Category]
IdentityFunctor [definition, in CT.Instance.Functor.IdentityFunctor]
IdentityFunctor [library]
IdentityIso [definition, in CT.Instance.Isomorphism]
IdentityNaturalTransformation [definition, in CT.Instance.NaturalTransformation.IdentityNaturalTransformation]
IdentityNaturalTransformation [library]
identity_is_full [lemma, in CT.Instance.Functor.IdentityFunctor]
identity_is_faithful [lemma, in CT.Instance.Functor.IdentityFunctor]
id_right [projection, in CT.Category]
id_left [projection, in CT.Category]
id1 [lemma, in CT.Algebra.PointedSet]
id2 [lemma, in CT.Algebra.PointedSet]
Instance [library]
inverse [projection, in CT.Algebra.Group]
InverseIso [definition, in CT.Instance.Isomorphism]
inv_right [projection, in CT.Isomorphism]
inv_left [projection, in CT.Isomorphism]
Isomorphism [record, in CT.Isomorphism]
Isomorphism [library]
Isomorphism [library]
iso_comp_iso [lemma, in CT.Instance.Isomorphism]
J
join [projection, in CT.Algebra.Lattice]join_lub [lemma, in CT.Algebra.Lattice]
join_consistency [projection, in CT.Algebra.Lattice]
join_assoc [projection, in CT.Algebra.Lattice]
join_comm [projection, in CT.Algebra.Lattice]
join_idem [projection, in CT.Algebra.Lattice]
L
L [projection, in CT.Algebra.BooleanAlgebra]l [constructor, in CT.Language.Dyck]
Language [library]
lat [definition, in CT.Algebra.Lattice]
Lat [definition, in CT.Instance.Algebra.Lat]
Lat [library]
Lattice [section, in CT.Algebra.Lattice]
lattice [projection, in CT.Algebra.Lattice]
Lattice [record, in CT.Algebra.Lattice]
Lattice [library]
LatticeHomomorphism [record, in CT.Algebra.Lattice]
lattice_hom_composition_assoc [definition, in CT.Algebra.Lattice]
lattice_hom_id [definition, in CT.Algebra.Lattice]
lattice_hom_eq [lemma, in CT.Algebra.Lattice]
lattice_hom_composition [definition, in CT.Algebra.Lattice]
lat_hom_pres_join [projection, in CT.Algebra.Lattice]
lat_hom_pres_meet [projection, in CT.Algebra.Lattice]
le [projection, in CT.Order.PartiallyOrderedSet]
LOSet [record, in CT.Algebra.Lattice]
l_r_ex [definition, in CT.Language.Dyck]
M
magma [projection, in CT.Algebra.Semigroup]Magma [record, in CT.Algebra.Magma]
Magma [library]
MagmaHomomorphism [record, in CT.Algebra.Magma]
magma_hom_id [definition, in CT.Algebra.Magma]
magma_hom_composition_assoc [definition, in CT.Algebra.Magma]
magma_hom_eq [lemma, in CT.Algebra.Magma]
magma_hom_composition [definition, in CT.Algebra.Magma]
magma_hom_law [projection, in CT.Algebra.Magma]
magma_hom [projection, in CT.Algebra.Magma]
Mealy [record, in CT.Automata.Mealy]
Mealy [section, in CT.Automata.Mealy]
Mealy [library]
Mealy [library]
MealyCategory [definition, in CT.Instance.Automata.Mealy.Category]
MealyMorphism [record, in CT.Automata.Mealy]
MealyMorphism_assoc [definition, in CT.Automata.Mealy]
MealyMorphism_eq [lemma, in CT.Automata.Mealy]
MealyMorphism_identity [definition, in CT.Automata.Mealy]
MealyMorphism_composition [definition, in CT.Automata.Mealy]
meet [projection, in CT.Algebra.Lattice]
meet_glb [lemma, in CT.Algebra.Lattice]
meet_consistency [projection, in CT.Algebra.Lattice]
meet_assoc [projection, in CT.Algebra.Lattice]
meet_comm [projection, in CT.Algebra.Lattice]
meet_idem [projection, in CT.Algebra.Lattice]
Mon [definition, in CT.Instance.Algebra.Monoid]
Monad [record, in CT.Monad]
Monad [library]
Monad [library]
monad_coherence_id_2 [projection, in CT.Monad]
monad_coherence_id_1 [projection, in CT.Monad]
monad_coherence_assoc [projection, in CT.Monad]
Monoid [record, in CT.Algebra.Monoid]
monoid [projection, in CT.Algebra.Group]
monoid [projection, in CT.Algebra.Ring]
Monoid [library]
Monoid [library]
Monoidal [library]
MonoidalCategory [record, in CT.Instance.Category.Monoidal]
MonoidCategory [definition, in CT.Instance.Category.MonoidCategory]
MonoidCategory [library]
MonoidHomomorphism [record, in CT.Algebra.Monoid]
monoid_hom_id [definition, in CT.Algebra.Monoid]
monoid_hom_composition_assoc [definition, in CT.Algebra.Monoid]
monoid_hom_eq [lemma, in CT.Algebra.Monoid]
monoid_hom_composition [definition, in CT.Algebra.Monoid]
monoid_hom_id_law [projection, in CT.Algebra.Monoid]
monoid_hom [projection, in CT.Algebra.Monoid]
monoid_identity_commutes [lemma, in CT.Algebra.Monoid]
monoid_identity_unique [lemma, in CT.Algebra.Monoid]
monoid_right_one [projection, in CT.Algebra.Monoid]
monoid_left_one [projection, in CT.Algebra.Monoid]
monoid_dist_over_group_r [projection, in CT.Algebra.Ring]
monoid_dist_over_group_l [projection, in CT.Algebra.Ring]
Moore [record, in CT.Automata.Moore]
Moore [section, in CT.Automata.Moore]
Moore [library]
Moore [library]
MooreCategory [definition, in CT.Instance.Automata.Moore.Category]
MooreMorphism [record, in CT.Automata.Moore]
MooreMorphism_assoc [definition, in CT.Automata.Moore]
MooreMorphism_eq [lemma, in CT.Automata.Moore]
MooreMorphism_identity [definition, in CT.Automata.Moore]
MooreMorphism_composition [definition, in CT.Automata.Moore]
mor [projection, in CT.Category]
Morphism [record, in CT.Morphism]
morphism [definition, in CT.Instance.Category.ArrowCategory]
Morphism [library]
mu [projection, in CT.Monad]
mu [projection, in CT.Algebra.Magma]
mu_power [definition, in CT.Algebra.Monoid]
M_mor [projection, in CT.Morphism]
M_cod [projection, in CT.Morphism]
M_dom [projection, in CT.Morphism]
N
NaturalIsomorphism [definition, in CT.Instance.NaturalTransformation.NaturalIsomorphism]NaturalIsomorphism [section, in CT.Instance.NaturalTransformation.NaturalIsomorphism]
NaturalIsomorphism [library]
NaturalTransformation [record, in CT.NaturalTransformation]
NaturalTransformation [library]
NaturalTransformation [library]
NaturalTransformationInterchange [lemma, in CT.Instance.NaturalTransformation.Composition]
NaturalTransformationInterchange [section, in CT.Instance.NaturalTransformation.Composition]
NaturalTransformationInterchange.l [variable, in CT.Instance.NaturalTransformation.Composition]
NaturalTransformationInterchange.r [variable, in CT.Instance.NaturalTransformation.Composition]
NonprimeToPrime [definition, in CT.Algebra.PointedSet]
notB [projection, in CT.Algebra.BooleanAlgebra]
nt_eq [lemma, in CT.NaturalTransformation]
nt_commutes_sym [projection, in CT.NaturalTransformation]
nt_commutes [projection, in CT.NaturalTransformation]
nt_components [projection, in CT.NaturalTransformation]
O
o [definition, in CT.Algebra.Lattice]ob [projection, in CT.Category]
one [projection, in CT.Algebra.Monoid]
Op [definition, in CT.Instance.Category.Opposite]
Opposite [library]
OppositeFunctor [definition, in CT.Instance.Functor.OppositeFunctor]
OppositeFunctor [library]
Order [library]
P
paren [inductive, in CT.Language.Dyck]PartiallyOrderedSet [record, in CT.Order.PartiallyOrderedSet]
PartiallyOrderedSet [library]
PointedSet [record, in CT.Algebra.PointedSet]
PointedSet [library]
PointedSetCategory [definition, in CT.Instance.Algebra.PointedSetCategory]
PointedSetCategory [library]
PointedSet' [definition, in CT.Algebra.PointedSet]
PointPreservingMap [record, in CT.Algebra.PointedSet]
point_pres_law [projection, in CT.Algebra.PointedSet]
point_pres_map [projection, in CT.Algebra.PointedSet]
poset [projection, in CT.Algebra.Lattice]
ppm_composition_assoc [definition, in CT.Algebra.PointedSet]
ppm_id [definition, in CT.Algebra.PointedSet]
ppm_composition [definition, in CT.Algebra.PointedSet]
ppm_eq [lemma, in CT.Algebra.PointedSet]
Presheaf [definition, in CT.Instance.Functor.Presheaf]
Presheaf [library]
pres_init_state [projection, in CT.Automata.Moore]
pres_outputs [projection, in CT.Automata.Moore]
pres_transition [projection, in CT.Automata.Moore]
pres_init_state [projection, in CT.Automata.Mealy]
pres_outputs [projection, in CT.Automata.Mealy]
pres_transition [projection, in CT.Automata.Mealy]
PrimeToNonprime [definition, in CT.Algebra.PointedSet]
ProductCategory [definition, in CT.Instance.Category.ProductCategory]
ProductCategory [library]
ProductCategory_p2 [definition, in CT.Instance.Category.ProductCategory]
ProductCategory_p1 [definition, in CT.Instance.Category.ProductCategory]
ProductFunctor [definition, in CT.Instance.Functor.ProductFunctor]
ProductFunctor [library]
Profunctor [definition, in CT.Instance.Functor.Profunctor]
Profunctor [library]
Projective [library]
p1 [projection, in CT.BinaryProduct]
p2 [projection, in CT.BinaryProduct]
Q
Q [projection, in CT.Automata.Moore]Q [projection, in CT.Automata.Mealy]
q0 [projection, in CT.Automata.Moore]
q0 [projection, in CT.Automata.Mealy]
R
r [constructor, in CT.Language.Dyck]reflexive [projection, in CT.Order.PartiallyOrderedSet]
Retract [record, in CT.Retract]
Retract [library]
retraction [projection, in CT.Retract]
retraction_law [projection, in CT.Retract]
Ring [record, in CT.Algebra.Ring]
Ring [library]
Ring [library]
RingCategory [definition, in CT.Instance.Algebra.Ring]
RingHomomorphism [record, in CT.Algebra.Ring]
ring_hom_id [definition, in CT.Algebra.Ring]
ring_hom_composition_assoc [definition, in CT.Algebra.Ring]
ring_hom_eq [lemma, in CT.Algebra.Ring]
ring_hom_composition [definition, in CT.Algebra.Ring]
ring_id_hom_law [projection, in CT.Algebra.Ring]
ring_group_hom_law [projection, in CT.Algebra.Ring]
ring_monoid_hom_law [projection, in CT.Algebra.Ring]
ring_hom [projection, in CT.Algebra.Ring]
Rng [record, in CT.Algebra.Rng]
Rng [library]
Rng [library]
RngCategory [definition, in CT.Instance.Algebra.Rng]
RngHomomorphism [record, in CT.Algebra.Rng]
rng_hom_id [definition, in CT.Algebra.Rng]
rng_hom_composition_assoc [definition, in CT.Algebra.Rng]
rng_hom_eq [lemma, in CT.Algebra.Rng]
rng_hom_composition [definition, in CT.Algebra.Rng]
rng_group_hom_law [projection, in CT.Algebra.Rng]
rng_monoid_hom_law [projection, in CT.Algebra.Rng]
rng_hom [projection, in CT.Algebra.Rng]
S
section [projection, in CT.Section]Section [record, in CT.Section]
Section [library]
section_law [projection, in CT.Section]
semigroup [projection, in CT.Algebra.Monoid]
semigroup [projection, in CT.Algebra.Rng]
Semigroup [record, in CT.Algebra.Semigroup]
Semigroup [library]
SemigroupHomomorphism [definition, in CT.Algebra.Semigroup]
semigroup_dist_over_group_r [projection, in CT.Algebra.Rng]
semigroup_dist_over_group_l [projection, in CT.Algebra.Rng]
semigroup_hom_id [definition, in CT.Algebra.Semigroup]
semigroup_hom_composition_assoc [definition, in CT.Algebra.Semigroup]
semigroup_hom_eq [definition, in CT.Algebra.Semigroup]
semigroup_hom_composition [definition, in CT.Algebra.Semigroup]
semigroup_assoc [projection, in CT.Algebra.Semigroup]
Sigma [projection, in CT.Automata.Moore]
Sigma [projection, in CT.Automata.Mealy]
T
T [projection, in CT.Monad]Tensor [definition, in CT.Instance.Functor.ProductFunctor]
tensor [projection, in CT.Instance.Category.Monoidal]
tensor_ [definition, in CT.Instance.Functor.ProductFunctor]
to [projection, in CT.Isomorphism]
transitive [projection, in CT.Order.PartiallyOrderedSet]
V
VCNaturalTransformation [definition, in CT.Instance.NaturalTransformation.VCNaturalTransformation]VCNaturalTransformation [section, in CT.Instance.NaturalTransformation.VCNaturalTransformation]
VCNaturalTransformation [library]
VCNaturalTransformation_id_right [lemma, in CT.Instance.NaturalTransformation.VCNaturalTransformation]
VCNaturalTransformation_id_left [lemma, in CT.Instance.NaturalTransformation.VCNaturalTransformation]
VCNaturalTransformation_assoc [lemma, in CT.Instance.NaturalTransformation.VCNaturalTransformation]
VCNaturalTransformation.epsilon [variable, in CT.Instance.NaturalTransformation.VCNaturalTransformation]
VCNaturalTransformation.eta [variable, in CT.Instance.NaturalTransformation.VCNaturalTransformation]
VCNaturalTransformation.X [variable, in CT.Instance.NaturalTransformation.VCNaturalTransformation]
W
word [definition, in CT.Language.Dyck]X
x1x2 [projection, in CT.BinaryProduct]Y
y [projection, in CT.Automata.Moore]Y [projection, in CT.Automata.Moore]
y [projection, in CT.Automata.Mealy]
Y [projection, in CT.Automata.Mealy]
_
_tensor [definition, in CT.Instance.Functor.ProductFunctor]other
_ ^op [notation, in CT.Instance.Category.Opposite]Notation Index
other
_ ^op [in CT.Instance.Category.Opposite]Variable Index
A
ArrowCategory.C [in CT.Instance.Category.ArrowCategory]C
CommaCategory.C [in CT.Instance.Category.CommaCategory]CommaCategory.D [in CT.Instance.Category.CommaCategory]
CommaCategory.E [in CT.Instance.Category.CommaCategory]
CommaCategory.f [in CT.Instance.Category.CommaCategory]
CommaCategory.g [in CT.Instance.Category.CommaCategory]
F
FaithfulFunctor.F [in CT.Instance.Functor.FaithfulFunctor]FullFunctor.F [in CT.Instance.Functor.FullFunctor]
FullyFaithfulFunctor.F [in CT.Instance.Functor.FullyFaithfulFunctor]
H
HCNaturalTransformation.epsilon [in CT.Instance.NaturalTransformation.HCNaturalTransformation]HCNaturalTransformation.JF [in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HCNaturalTransformation.KG [in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HCNaturalTransformation.mu [in CT.Instance.NaturalTransformation.HCNaturalTransformation]
HomFunctor.F [in CT.Instance.Functor.HomFunctor]
N
NaturalTransformationInterchange.l [in CT.Instance.NaturalTransformation.Composition]NaturalTransformationInterchange.r [in CT.Instance.NaturalTransformation.Composition]
V
VCNaturalTransformation.epsilon [in CT.Instance.NaturalTransformation.VCNaturalTransformation]VCNaturalTransformation.eta [in CT.Instance.NaturalTransformation.VCNaturalTransformation]
VCNaturalTransformation.X [in CT.Instance.NaturalTransformation.VCNaturalTransformation]
Library Index
A
AbAbelianGroup
Algebra
Algebra
ArrowCategory
Automata
Automata
B
BifunctorBinaryProduct
BinaryProduct
BooleanAlgebra
C
CatCategory
Category
Category
Category
Category
CommaCategory
ComposeFunctor
Composition
ConstantFunctor
ContravariantFunctor
Coq
D
DyckE
EndofunctorEquivalence
F
FaithfulFunctorFAlgebra
FullFunctor
FullyFaithfulFunctor
Functor
Functor
Functor
FunctorCategory
G
GeometryGroup
GroupCategory
Grp
H
HCNaturalTransformationHomFunctor
I
IdentityFunctorIdentityNaturalTransformation
Instance
Isomorphism
Isomorphism
L
LanguageLat
Lattice
M
MagmaMealy
Mealy
Monad
Monad
Monoid
Monoid
Monoidal
MonoidCategory
Moore
Moore
Morphism
N
NaturalIsomorphismNaturalTransformation
NaturalTransformation
O
OppositeOppositeFunctor
Order
P
PartiallyOrderedSetPointedSet
PointedSetCategory
Presheaf
ProductCategory
ProductFunctor
Profunctor
Projective
R
RetractRing
Ring
Rng
Rng
S
SectionSemigroup
V
VCNaturalTransformationLemma Index
A
ab_e_is_ba_e [in CT.Algebra.Group]C
CategoryEquivalenceSymmetry [in CT.Instance.Category.Equivalence]CategoryEquivalenceTransitivity [in CT.Instance.Category.Equivalence]
comp_identity_left [in CT.Instance.Functor.IdentityFunctor]
comp_identity_right [in CT.Instance.Functor.IdentityFunctor]
comp_identity_identity [in CT.Instance.Functor.IdentityFunctor]
CoqProp_has_products [in CT.Instance.Coq.BinaryProduct]
CoqSet_has_products [in CT.Instance.Coq.BinaryProduct]
CoqType_has_products [in CT.Instance.Coq.BinaryProduct]
D
dyck_must_start_l [in CT.Language.Dyck]E
exist_injective [in CT.Instance.Category.ArrowCategory]F
functor_pres_iso [in CT.Functor]functor_comp_assoc [in CT.Instance.Functor.ComposeFunctor]
F_eq [in CT.Functor]
G
group_hom_pres_inverse [in CT.Algebra.Group]group_equals_one_implies_inverse [in CT.Algebra.Group]
group_commutative_one [in CT.Algebra.Group]
group_hom_pres_id [in CT.Algebra.Group]
group_commutative_conj [in CT.Algebra.Group]
group_squared_identity [in CT.Algebra.Group]
group_cancel_right [in CT.Algebra.Group]
group_cancel_left [in CT.Algebra.Group]
group_inverse_of_product [in CT.Algebra.Group]
group_inverse_unique [in CT.Algebra.Group]
group_inverse_inverse [in CT.Algebra.Group]
group_identity_unique [in CT.Algebra.Group]
group_unique_unop [in CT.Algebra.Group]
I
identity_is_full [in CT.Instance.Functor.IdentityFunctor]identity_is_faithful [in CT.Instance.Functor.IdentityFunctor]
id1 [in CT.Algebra.PointedSet]
id2 [in CT.Algebra.PointedSet]
iso_comp_iso [in CT.Instance.Isomorphism]
J
join_lub [in CT.Algebra.Lattice]L
lattice_hom_eq [in CT.Algebra.Lattice]M
magma_hom_eq [in CT.Algebra.Magma]MealyMorphism_eq [in CT.Automata.Mealy]
meet_glb [in CT.Algebra.Lattice]
monoid_hom_eq [in CT.Algebra.Monoid]
monoid_identity_commutes [in CT.Algebra.Monoid]
monoid_identity_unique [in CT.Algebra.Monoid]
MooreMorphism_eq [in CT.Automata.Moore]
N
NaturalTransformationInterchange [in CT.Instance.NaturalTransformation.Composition]nt_eq [in CT.NaturalTransformation]
P
ppm_eq [in CT.Algebra.PointedSet]R
ring_hom_eq [in CT.Algebra.Ring]rng_hom_eq [in CT.Algebra.Rng]
V
VCNaturalTransformation_id_right [in CT.Instance.NaturalTransformation.VCNaturalTransformation]VCNaturalTransformation_id_left [in CT.Instance.NaturalTransformation.VCNaturalTransformation]
VCNaturalTransformation_assoc [in CT.Instance.NaturalTransformation.VCNaturalTransformation]
Constructor Index
D
dEpsilon [in CT.Language.Dyck]dInd [in CT.Language.Dyck]
L
l [in CT.Language.Dyck]R
r [in CT.Language.Dyck]Projection Index
A
abelian_commutativity [in CT.Algebra.AbelianGroup]absorption_2 [in CT.Algebra.Lattice]
absorption_1 [in CT.Algebra.Lattice]
antisymmetric [in CT.Order.PartiallyOrderedSet]
assoc [in CT.Category]
assoc_sym [in CT.Category]
B
basepoint [in CT.Algebra.PointedSet]bin_prod_unique [in CT.BinaryProduct]
bin_prod_comp2 [in CT.BinaryProduct]
bin_prod_comp1 [in CT.BinaryProduct]
bin_prod_mor [in CT.BinaryProduct]
C
ceq_nat_iso2 [in CT.Instance.Category.Equivalence]ceq_nat_iso1 [in CT.Instance.Category.Equivalence]
comma_mor_law [in CT.Instance.Category.CommaCategory]
comma_gamma [in CT.Instance.Category.CommaCategory]
comma_beta [in CT.Instance.Category.CommaCategory]
comma_a_b [in CT.Instance.Category.CommaCategory]
comma_b [in CT.Instance.Category.CommaCategory]
comma_a [in CT.Instance.Category.CommaCategory]
comp [in CT.Category]
condB [in CT.Algebra.BooleanAlgebra]
D
delta [in CT.Automata.Moore]delta [in CT.Automata.Mealy]
E
element [in CT.Algebra.Lattice]eta [in CT.Monad]
F
f [in CT.Algebra.Lattice]F [in CT.Instance.Category.Equivalence]
FA_alpha [in CT.Instance.Functor.FAlgebra]
FA_ob [in CT.Instance.Functor.FAlgebra]
from [in CT.Isomorphism]
F_comp_law [in CT.Functor]
F_id_law [in CT.Functor]
F_mor [in CT.Functor]
F_ob [in CT.Functor]
f_Y [in CT.Automata.Moore]
f_Sigma [in CT.Automata.Moore]
f_Q [in CT.Automata.Moore]
f_Y [in CT.Automata.Mealy]
f_Sigma [in CT.Automata.Mealy]
f_Q [in CT.Automata.Mealy]
G
G [in CT.Instance.Category.Equivalence]geom_refl [in CT.Geometry.Projective]
geom_symm [in CT.Geometry.Projective]
geom_incidence [in CT.Geometry.Projective]
geom_point [in CT.Geometry.Projective]
group [in CT.Algebra.Rng]
group [in CT.Algebra.Ring]
group [in CT.Algebra.AbelianGroup]
gr_inverse_right [in CT.Algebra.Group]
gr_inverse_left [in CT.Algebra.Group]
I
I [in CT.Instance.Category.Monoidal]id [in CT.Category]
id_right [in CT.Category]
id_left [in CT.Category]
inverse [in CT.Algebra.Group]
inv_right [in CT.Isomorphism]
inv_left [in CT.Isomorphism]
J
join [in CT.Algebra.Lattice]join_consistency [in CT.Algebra.Lattice]
join_assoc [in CT.Algebra.Lattice]
join_comm [in CT.Algebra.Lattice]
join_idem [in CT.Algebra.Lattice]
L
L [in CT.Algebra.BooleanAlgebra]lattice [in CT.Algebra.Lattice]
lat_hom_pres_join [in CT.Algebra.Lattice]
lat_hom_pres_meet [in CT.Algebra.Lattice]
le [in CT.Order.PartiallyOrderedSet]
M
magma [in CT.Algebra.Semigroup]magma_hom_law [in CT.Algebra.Magma]
magma_hom [in CT.Algebra.Magma]
meet [in CT.Algebra.Lattice]
meet_consistency [in CT.Algebra.Lattice]
meet_assoc [in CT.Algebra.Lattice]
meet_comm [in CT.Algebra.Lattice]
meet_idem [in CT.Algebra.Lattice]
monad_coherence_id_2 [in CT.Monad]
monad_coherence_id_1 [in CT.Monad]
monad_coherence_assoc [in CT.Monad]
monoid [in CT.Algebra.Group]
monoid [in CT.Algebra.Ring]
monoid_hom_id_law [in CT.Algebra.Monoid]
monoid_hom [in CT.Algebra.Monoid]
monoid_right_one [in CT.Algebra.Monoid]
monoid_left_one [in CT.Algebra.Monoid]
monoid_dist_over_group_r [in CT.Algebra.Ring]
monoid_dist_over_group_l [in CT.Algebra.Ring]
mor [in CT.Category]
mu [in CT.Monad]
mu [in CT.Algebra.Magma]
M_mor [in CT.Morphism]
M_cod [in CT.Morphism]
M_dom [in CT.Morphism]
N
notB [in CT.Algebra.BooleanAlgebra]nt_commutes_sym [in CT.NaturalTransformation]
nt_commutes [in CT.NaturalTransformation]
nt_components [in CT.NaturalTransformation]
O
ob [in CT.Category]one [in CT.Algebra.Monoid]
P
point_pres_law [in CT.Algebra.PointedSet]point_pres_map [in CT.Algebra.PointedSet]
poset [in CT.Algebra.Lattice]
pres_init_state [in CT.Automata.Moore]
pres_outputs [in CT.Automata.Moore]
pres_transition [in CT.Automata.Moore]
pres_init_state [in CT.Automata.Mealy]
pres_outputs [in CT.Automata.Mealy]
pres_transition [in CT.Automata.Mealy]
p1 [in CT.BinaryProduct]
p2 [in CT.BinaryProduct]
Q
Q [in CT.Automata.Moore]Q [in CT.Automata.Mealy]
q0 [in CT.Automata.Moore]
q0 [in CT.Automata.Mealy]
R
reflexive [in CT.Order.PartiallyOrderedSet]retraction [in CT.Retract]
retraction_law [in CT.Retract]
ring_id_hom_law [in CT.Algebra.Ring]
ring_group_hom_law [in CT.Algebra.Ring]
ring_monoid_hom_law [in CT.Algebra.Ring]
ring_hom [in CT.Algebra.Ring]
rng_group_hom_law [in CT.Algebra.Rng]
rng_monoid_hom_law [in CT.Algebra.Rng]
rng_hom [in CT.Algebra.Rng]
S
section [in CT.Section]section_law [in CT.Section]
semigroup [in CT.Algebra.Monoid]
semigroup [in CT.Algebra.Rng]
semigroup_dist_over_group_r [in CT.Algebra.Rng]
semigroup_dist_over_group_l [in CT.Algebra.Rng]
semigroup_assoc [in CT.Algebra.Semigroup]
Sigma [in CT.Automata.Moore]
Sigma [in CT.Automata.Mealy]
T
T [in CT.Monad]tensor [in CT.Instance.Category.Monoidal]
to [in CT.Isomorphism]
transitive [in CT.Order.PartiallyOrderedSet]
X
x1x2 [in CT.BinaryProduct]Y
y [in CT.Automata.Moore]Y [in CT.Automata.Moore]
y [in CT.Automata.Mealy]
Y [in CT.Automata.Mealy]
Inductive Index
D
Dyck [in CT.Language.Dyck]P
paren [in CT.Language.Dyck]Section Index
A
ArrowCategory [in CT.Instance.Category.ArrowCategory]C
CategoryEquivalence [in CT.Instance.Category.Equivalence]CategoryEquivalence.CategoryEquivalenceReflexivity [in CT.Instance.Category.Equivalence]
CategoryEquivalence.CategoryEquivalenceSymmetry [in CT.Instance.Category.Equivalence]
CategoryEquivalence.CategoryEquivalenceTransitivity [in CT.Instance.Category.Equivalence]
CommaCategory [in CT.Instance.Category.CommaCategory]
CoqListMonad [in CT.Instance.Coq.Monad]
CoqOptionMonad [in CT.Instance.Coq.Monad]
F
FaithfulFunctor [in CT.Instance.Functor.FaithfulFunctor]FAlgebra [in CT.Instance.Functor.FAlgebra]
FullFunctor [in CT.Instance.Functor.FullFunctor]
FullyFaithfulFunctor [in CT.Instance.Functor.FullyFaithfulFunctor]
H
HCNaturalTransformation [in CT.Instance.NaturalTransformation.HCNaturalTransformation]HomFunctor [in CT.Instance.Functor.HomFunctor]
L
Lattice [in CT.Algebra.Lattice]M
Mealy [in CT.Automata.Mealy]Moore [in CT.Automata.Moore]
N
NaturalIsomorphism [in CT.Instance.NaturalTransformation.NaturalIsomorphism]NaturalTransformationInterchange [in CT.Instance.NaturalTransformation.Composition]
V
VCNaturalTransformation [in CT.Instance.NaturalTransformation.VCNaturalTransformation]Definition Index
A
A [in CT.Algebra.Lattice]Ab [in CT.Instance.Algebra.Ab]
ab_group_hom_id [in CT.Algebra.AbelianGroup]
ab_group_hom_composition_assoc [in CT.Algebra.AbelianGroup]
ab_group_hom_eq [in CT.Algebra.AbelianGroup]
ab_group_hom_composition [in CT.Algebra.AbelianGroup]
ArrowCategory [in CT.Instance.Category.ArrowCategory]
B
Bifunctor [in CT.Instance.Functor.Bifunctor]bimap [in CT.Instance.Functor.Bifunctor]
bind [in CT.Monad]
C
Cat [in CT.Instance.Category.Cat]CategoryEquivalenceReflexivity [in CT.Instance.Category.Equivalence]
category_equiv_refl_nat_iso [in CT.Instance.Category.Equivalence]
ComposeFunctor [in CT.Instance.Functor.ComposeFunctor]
ConstantFunctor [in CT.Instance.Functor.ConstantFunctor]
ContravariantFunctor [in CT.Instance.Functor.ContravariantFunctor]
CoqListEtaNT [in CT.Instance.Coq.Monad]
CoqListFunctor [in CT.Instance.Coq.Functor]
CoqListMonad [in CT.Instance.Coq.Monad]
CoqListMuNT [in CT.Instance.Coq.Monad]
CoqOptionEtaNT [in CT.Instance.Coq.Monad]
CoqOptionFunctor [in CT.Instance.Coq.Functor]
CoqOptionMonad [in CT.Instance.Coq.Monad]
CoqOptionMuNT [in CT.Instance.Coq.Monad]
CoqProp [in CT.Instance.Coq.Category]
CoqProp_product [in CT.Instance.Coq.BinaryProduct]
CoqSet [in CT.Instance.Coq.Category]
CoqSet_product [in CT.Instance.Coq.BinaryProduct]
CoqType [in CT.Instance.Coq.Category]
CoqType_product [in CT.Instance.Coq.BinaryProduct]
E
Endofunctor [in CT.Instance.Functor.Endofunctor]EndofunctorCategory [in CT.Instance.Category.FunctorCategory]
F
FaithfulFunctor [in CT.Instance.Functor.FaithfulFunctor]FullFunctor [in CT.Instance.Functor.FullFunctor]
FullyFaithfulFunctor [in CT.Instance.Functor.FullyFaithfulFunctor]
FunctorCategory [in CT.Instance.Category.FunctorCategory]
G
GroupCategory [in CT.Instance.Category.GroupCategory]GroupHomomorphism [in CT.Algebra.Group]
group_hom_id [in CT.Algebra.Group]
group_hom_composition_assoc [in CT.Algebra.Group]
group_hom_eq [in CT.Algebra.Group]
group_hom_composition [in CT.Algebra.Group]
Grp [in CT.Instance.Algebra.Grp]
H
has_products [in CT.BinaryProduct]HCNaturalTransformation [in CT.Instance.NaturalTransformation.HCNaturalTransformation]
I
IdentityFunctor [in CT.Instance.Functor.IdentityFunctor]IdentityIso [in CT.Instance.Isomorphism]
IdentityNaturalTransformation [in CT.Instance.NaturalTransformation.IdentityNaturalTransformation]
InverseIso [in CT.Instance.Isomorphism]
L
lat [in CT.Algebra.Lattice]Lat [in CT.Instance.Algebra.Lat]
lattice_hom_composition_assoc [in CT.Algebra.Lattice]
lattice_hom_id [in CT.Algebra.Lattice]
lattice_hom_composition [in CT.Algebra.Lattice]
l_r_ex [in CT.Language.Dyck]
M
magma_hom_id [in CT.Algebra.Magma]magma_hom_composition_assoc [in CT.Algebra.Magma]
magma_hom_composition [in CT.Algebra.Magma]
MealyCategory [in CT.Instance.Automata.Mealy.Category]
MealyMorphism_assoc [in CT.Automata.Mealy]
MealyMorphism_identity [in CT.Automata.Mealy]
MealyMorphism_composition [in CT.Automata.Mealy]
Mon [in CT.Instance.Algebra.Monoid]
MonoidCategory [in CT.Instance.Category.MonoidCategory]
monoid_hom_id [in CT.Algebra.Monoid]
monoid_hom_composition_assoc [in CT.Algebra.Monoid]
monoid_hom_composition [in CT.Algebra.Monoid]
MooreCategory [in CT.Instance.Automata.Moore.Category]
MooreMorphism_assoc [in CT.Automata.Moore]
MooreMorphism_identity [in CT.Automata.Moore]
MooreMorphism_composition [in CT.Automata.Moore]
morphism [in CT.Instance.Category.ArrowCategory]
mu_power [in CT.Algebra.Monoid]
N
NaturalIsomorphism [in CT.Instance.NaturalTransformation.NaturalIsomorphism]NonprimeToPrime [in CT.Algebra.PointedSet]
O
o [in CT.Algebra.Lattice]Op [in CT.Instance.Category.Opposite]
OppositeFunctor [in CT.Instance.Functor.OppositeFunctor]
P
PointedSetCategory [in CT.Instance.Algebra.PointedSetCategory]PointedSet' [in CT.Algebra.PointedSet]
ppm_composition_assoc [in CT.Algebra.PointedSet]
ppm_id [in CT.Algebra.PointedSet]
ppm_composition [in CT.Algebra.PointedSet]
Presheaf [in CT.Instance.Functor.Presheaf]
PrimeToNonprime [in CT.Algebra.PointedSet]
ProductCategory [in CT.Instance.Category.ProductCategory]
ProductCategory_p2 [in CT.Instance.Category.ProductCategory]
ProductCategory_p1 [in CT.Instance.Category.ProductCategory]
ProductFunctor [in CT.Instance.Functor.ProductFunctor]
Profunctor [in CT.Instance.Functor.Profunctor]
R
RingCategory [in CT.Instance.Algebra.Ring]ring_hom_id [in CT.Algebra.Ring]
ring_hom_composition_assoc [in CT.Algebra.Ring]
ring_hom_composition [in CT.Algebra.Ring]
RngCategory [in CT.Instance.Algebra.Rng]
rng_hom_id [in CT.Algebra.Rng]
rng_hom_composition_assoc [in CT.Algebra.Rng]
rng_hom_composition [in CT.Algebra.Rng]
S
SemigroupHomomorphism [in CT.Algebra.Semigroup]semigroup_hom_id [in CT.Algebra.Semigroup]
semigroup_hom_composition_assoc [in CT.Algebra.Semigroup]
semigroup_hom_eq [in CT.Algebra.Semigroup]
semigroup_hom_composition [in CT.Algebra.Semigroup]
T
Tensor [in CT.Instance.Functor.ProductFunctor]tensor_ [in CT.Instance.Functor.ProductFunctor]
V
VCNaturalTransformation [in CT.Instance.NaturalTransformation.VCNaturalTransformation]W
word [in CT.Language.Dyck]_
_tensor [in CT.Instance.Functor.ProductFunctor]Record Index
A
AbelianGroup [in CT.Algebra.AbelianGroup]B
BinaryProduct [in CT.BinaryProduct]BooleanAlgebra [in CT.Algebra.BooleanAlgebra]
C
Category [in CT.Category]CategoryEquivalence [in CT.Instance.Category.Equivalence]
CommaCategoryMor [in CT.Instance.Category.CommaCategory]
CommaCategoryOb [in CT.Instance.Category.CommaCategory]
F
FAlgebra [in CT.Instance.Functor.FAlgebra]Functor [in CT.Functor]
G
Geometry [in CT.Geometry.Projective]Group [in CT.Algebra.Group]
I
Isomorphism [in CT.Isomorphism]L
Lattice [in CT.Algebra.Lattice]LatticeHomomorphism [in CT.Algebra.Lattice]
LOSet [in CT.Algebra.Lattice]
M
Magma [in CT.Algebra.Magma]MagmaHomomorphism [in CT.Algebra.Magma]
Mealy [in CT.Automata.Mealy]
MealyMorphism [in CT.Automata.Mealy]
Monad [in CT.Monad]
Monoid [in CT.Algebra.Monoid]
MonoidalCategory [in CT.Instance.Category.Monoidal]
MonoidHomomorphism [in CT.Algebra.Monoid]
Moore [in CT.Automata.Moore]
MooreMorphism [in CT.Automata.Moore]
Morphism [in CT.Morphism]
N
NaturalTransformation [in CT.NaturalTransformation]P
PartiallyOrderedSet [in CT.Order.PartiallyOrderedSet]PointedSet [in CT.Algebra.PointedSet]
PointPreservingMap [in CT.Algebra.PointedSet]
R
Retract [in CT.Retract]Ring [in CT.Algebra.Ring]
RingHomomorphism [in CT.Algebra.Ring]
Rng [in CT.Algebra.Rng]
RngHomomorphism [in CT.Algebra.Rng]
S
Section [in CT.Section]Semigroup [in CT.Algebra.Semigroup]
| 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 | (463 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 | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 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 | (82 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 | (49 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 | (4 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 | (141 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 | (2 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 | (20 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 | (108 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 | (37 entries) |
This page has been generated by coqdoc