| 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 |
_ |
(1140 entries) |
| Tactic 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 |
_ |
(3 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 |
_ |
(47 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 |
_ |
(526 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 |
_ |
(30 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 |
_ |
(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 |
_ |
(416 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 |
_ |
(88 entries) |
Global Index
A
A [definition, in make_small_cat]
A [definition, in make_small_cat_]
A [definition, in make_small_cat__]
abgroup [module]
abgroup_ [module]
abgroup_of_cgroup [definition, in abgroup]
abgroup_of_cgroup [definition, in abgroup_]
abgroup_quot [module]
abgroup_quot_ [module]
abmonoid [module]
abmonoid_ [module]
abmonoid_of_abgroup [definition, in abgroup_]
abmonoid_of_abgroup [definition, in abgroup]
abmonoid_of_cmonoid [definition, in abmonoid_]
abmonoid_of_cmonoid [definition, in abmonoid]
abmonoid_quot [module]
abmonoid_quot_ [module]
add_assoc [lemma, in abgroup_]
add_assoc [lemma, in cring]
add_assoc [lemma, in ring]
add_assoc [lemma, in abmonoid_]
add_assoc [lemma, in abgroup]
add_assoc [lemma, in abmonoid]
add_assoc [lemma, in ring_]
add_assoc [lemma, in cring_]
add_commut [lemma, in ring_]
add_commut [lemma, in abmonoid_]
add_commut [lemma, in abmonoid]
add_commut [lemma, in cring_]
add_commut [lemma, in cring]
add_commut [lemma, in ring]
add_commut [lemma, in abgroup]
add_commut [lemma, in abgroup_]
add_sx_cancel [lemma, in abgroup]
add_sx_cancel [lemma, in abgroup_]
algebra [module]
algebra_ [module]
amul [definition, in algebra_]
amul [definition, in algebra]
B
base [definition, in cat_over_]
base [definition, in cat_over]
base_change [definition, in fibprod_]
base_change [definition, in fibprod]
bijection_eq1 [lemma, in map]
bijection_eq1 [lemma, in map__]
bijection_eq1 [lemma, in map_]
bijection_eq1 [lemma, in map___]
bijection_eq2 [lemma, in map_]
bijection_eq2 [lemma, in map__]
bijection_eq2 [lemma, in map]
bijection_eq2 [lemma, in map___]
bijection_inverse [definition, in map_]
bijection_inverse [definition, in map__]
bijection_inverse [definition, in map___]
bijection_inverse [definition, in map]
C
cat [definition, in yoneda_]
cat [definition, in yoneda]
cat [module]
cat_ [module]
cat_over [definition, in cat_over]
cat_over [definition, in cat_over_]
cat_over [module]
cat_over_ [module]
cat_sig [module]
cat_sig_ [module]
cat_sig__ [module]
cat_sig___ [module]
cat_under [definition, in cat_over_]
cat_under [definition, in cat_over]
cat__ [module]
cat___ [module]
cgroup [module]
cgroup_ [module]
cgroup_of_abgroup [definition, in abgroup]
cgroup_of_abgroup [definition, in abgroup_]
cgroup_quot [module]
cgroup_quot_ [module]
class [axiom, in quot]
class [axiom, in quot_]
class_congr [lemma, in quot_]
class_congr [lemma, in quot]
class_eq [axiom, in quot_]
class_eq [axiom, in quot]
class_eq_Q [definition, in cmonoid_quot_]
class_eq_Q [definition, in abmonoid_quot]
class_eq_Q [definition, in cgroup_quot]
class_eq_Q [definition, in abgroup_quot]
class_eq_Q [definition, in cmonoid_quot]
class_eq_Q [definition, in monoid_quot_]
class_eq_Q [definition, in group_quot_]
class_eq_Q [definition, in group_quot]
class_eq_Q [definition, in abmonoid_quot_]
class_eq_Q [definition, in abgroup_quot_]
class_eq_Q [definition, in monoid_quot]
class_eq_Q [definition, in cgroup_quot_]
class_rel [axiom, in quot]
class_rel [axiom, in quot_]
class_surj [axiom, in quot]
class_surj [axiom, in quot_]
cmonoid [module]
cmonoid_ [module]
cmonoid_of_abmonoid [definition, in abmonoid]
cmonoid_of_abmonoid [definition, in abmonoid_]
cmonoid_quot [module]
cmonoid_quot_ [module]
Compatible [definition, in equiv_]
Compatible [definition, in equiv]
Compatible2 [definition, in quot]
Compatible2 [definition, in quot_]
compatible_compatible2 [lemma, in quot]
compatible_compatible2 [lemma, in quot_]
compatible_dx [lemma, in quot_]
compatible_dx [lemma, in quot]
Compatible_Monoid [definition, in abmonoid_quot]
Compatible_Monoid [definition, in abmonoid_quot_]
Compatible_Monoid [definition, in cmonoid_quot]
Compatible_Monoid [definition, in monoid_quot_]
Compatible_Monoid [definition, in monoid_quot]
Compatible_Monoid [definition, in cmonoid_quot_]
compatible_sx [lemma, in quot_]
compatible_sx [lemma, in quot]
congr [lemma, in misc]
congr [lemma, in misc___]
congr [lemma, in misc__]
congr [lemma, in misc_]
congr2 [lemma, in misc]
congr2 [lemma, in misc__]
congr2 [lemma, in misc___]
congr2 [lemma, in misc_]
cool [axiom, in cool]
cool [module]
cosection_comp [definition, in map___]
cosection_comp [definition, in map_]
cosection_comp [definition, in map__]
cosection_comp [definition, in map]
cosection_inj [lemma, in map]
cosection_inj [lemma, in map___]
cosection_inj [lemma, in map__]
cosection_inj [lemma, in map_]
cosection_of_inverse [definition, in map__]
cosection_of_inverse [definition, in map_]
cosection_of_inverse [definition, in map]
cosection_of_inverse [definition, in map___]
Cov [definition, in topology_]
cov [definition, in topology]
Cov [definition, in topology]
cov [definition, in topology_]
cov_obj_transport [lemma, in topology_]
cov_obj_transport [lemma, in topology]
cov_sieve_geq [lemma, in topology]
cov_sieve_geq [lemma, in topology_]
cring [module]
cring_ [module]
D
distrib_dx [lemma, in cring]
distrib_dx [lemma, in cring_]
distrib_dx [lemma, in ring_]
distrib_dx [lemma, in ring]
distrib_sx [lemma, in ring]
distrib_sx [lemma, in ring_]
distrib_sx [lemma, in cring_]
distrib_sx [lemma, in cring]
Dual_Cat [definition, in cat_]
Dual_Cat [definition, in cat__]
Dual_Cat [definition, in cat]
Dual_Cat [definition, in cat___]
E
embedding [definition, in cat__]
embedding [definition, in cat___]
embedding [definition, in cat_]
embedding [definition, in cat]
epi_of_inv [lemma, in universal_]
epi_of_inv [lemma, in universal]
epi_of_inv_dx [lemma, in universal_]
epi_of_inv_dx [lemma, in universal]
eqT_JMeq [lemma, in misc]
eqT_JMeq [lemma, in misc_]
eqT_JMeq [lemma, in misc__]
eqT_JMeq [lemma, in misc___]
eqT_rect_simpl [lemma, in misc]
eqT_rect_simpl [lemma, in misc_]
eqT_rect_simpl [lemma, in misc___]
eqT_rect_simpl [lemma, in misc__]
equiv [module]
equiv_ [module]
eqv_eqT [lemma, in equiv_]
eqv_eqT [lemma, in equiv]
eqv_refl [lemma, in equiv_]
eqv_refl [lemma, in equiv]
eqv_sym [lemma, in equiv_]
eqv_sym [lemma, in equiv]
eqv_trans [lemma, in equiv_]
eqv_trans [lemma, in equiv]
eq_fct [definition, in cat]
eq_fct [definition, in cat__]
eq_fct [definition, in cat___]
eq_fct [definition, in cat_]
eq_fct_obj [lemma, in cat___]
eq_fct_obj [lemma, in cat]
eq_fct_obj [lemma, in cat__]
eq_fct_obj [lemma, in cat_]
eq_fct_src [lemma, in cat__]
eq_fct_src [lemma, in cat_]
eq_fct_src [lemma, in cat___]
eq_fct_src [lemma, in cat]
eq_fct_trg [lemma, in cat]
eq_fct_trg [lemma, in cat_]
eq_fct_trg [lemma, in cat__]
eq_fct_trg [lemma, in cat___]
eq_from_inverse_eq [lemma, in map__]
eq_from_inverse_eq [lemma, in map_]
eq_from_inverse_eq [lemma, in map]
eq_from_inverse_eq [lemma, in map___]
eq_mor [inductive, in cat__]
eq_mor [inductive, in cat_]
eq_mor [inductive, in cat]
eq_mor [inductive, in cat___]
eq_mor_eqT [lemma, in cat_]
eq_mor_eqT [lemma, in cat___]
eq_mor_eqT [lemma, in cat__]
eq_mor_eqT [lemma, in cat]
eq_mor_refl [constructor, in cat]
eq_mor_refl [constructor, in cat__]
eq_mor_refl [constructor, in cat___]
eq_mor_refl [constructor, in cat_]
eq_mor_src [lemma, in cat__]
eq_mor_src [lemma, in cat_]
eq_mor_src [lemma, in cat]
eq_mor_src [lemma, in cat___]
eq_mor_sym [lemma, in cat___]
eq_mor_sym [lemma, in cat_]
eq_mor_sym [lemma, in cat]
eq_mor_sym [lemma, in cat__]
eq_mor_trans [lemma, in cat]
eq_mor_trans [lemma, in cat___]
eq_mor_trans [lemma, in cat__]
eq_mor_trans [lemma, in cat_]
eq_mor_trg [lemma, in cat_]
eq_mor_trg [lemma, in cat]
eq_mor_trg [lemma, in cat___]
eq_mor_trg [lemma, in cat__]
eq_presh [definition, in presheaf]
eq_presh [definition, in presheaf__]
eq_presh [definition, in presheaf_]
eq_presh_obj [lemma, in presheaf__]
eq_presh_obj [lemma, in presheaf_]
eq_presh_obj [lemma, in presheaf]
eq_presh_src [lemma, in presheaf__]
eq_presh_src [lemma, in presheaf]
eq_presh_src [lemma, in presheaf_]
eq_presh_trg [lemma, in presheaf__]
eq_presh_trg [lemma, in presheaf_]
eq_presh_trg [lemma, in presheaf]
extensionality [axiom, in misc___]
extensionality [axiom, in misc_]
extensionality [axiom, in misc__]
extensionality [axiom, in misc]
F
fact [axiom, in quot_]
fact [axiom, in quot]
fact2 [definition, in quot]
fact2 [definition, in quot_]
fact2_comm [lemma, in quot]
fact2_comm [lemma, in quot_]
fact2_eq [lemma, in quot]
fact2_eq [lemma, in quot_]
fact_comm [axiom, in quot_]
fact_comm [axiom, in quot]
fact_eq [lemma, in quot]
fact_eq [lemma, in quot_]
fct_ii [lemma, in cat__]
fct_ii [lemma, in cat___]
fct_ii [lemma, in cat_]
fct_ii [lemma, in cat]
fct_oo [lemma, in cat__]
fct_oo [lemma, in cat___]
fct_oo [lemma, in cat]
fct_oo [lemma, in cat_]
Fibprod [definition, in fibprod]
Fibprod [definition, in fibprod_]
fibprod [module]
fibprod_ [module]
final_eq [lemma, in universal_]
final_eq [lemma, in universal]
final_extens [lemma, in universal_]
final_extens [lemma, in universal]
final_f_eq_g [lemma, in universal_]
final_f_eq_g [lemma, in universal]
final_isom [definition, in universal]
final_isom [definition, in universal_]
final_isom_eq [lemma, in universal]
final_isom_eq [lemma, in universal_]
final_isom_inv [definition, in universal_]
final_isom_inv [definition, in universal]
final_of_zero [definition, in universal]
final_of_zero [definition, in universal_]
final_over [definition, in cat_over]
final_over [definition, in cat_over_]
Final_Theory [definition, in universal]
Final_Theory [definition, in universal_]
forget [definition, in misc___]
forget [definition, in misc__]
forget [definition, in misc_]
forget [definition, in misc]
functor_cat [module]
functor_cat_ [module]
functor_extens [lemma, in cat___]
functor_extens [lemma, in cat]
functor_extens [lemma, in cat__]
functor_extens [lemma, in cat_]
G
group [module]
group_ [module]
group_of_cgroup [definition, in cgroup]
group_of_cgroup [definition, in cgroup_]
group_quot [definition, in cgroup_quot]
group_quot [definition, in cgroup_quot_]
group_quot [definition, in group_quot]
group_quot [definition, in abgroup_quot]
group_quot [definition, in abgroup_quot_]
group_quot [definition, in group_quot_]
group_quot [module]
group_quot_ [module]
H
h [definition, in yoneda_]
h [definition, in yoneda]
has_fibprod [definition, in fibprod_]
has_fibprod [definition, in fibprod]
has_product [definition, in product]
has_product [definition, in product_]
h_theory [lemma, in yoneda]
h_theory [lemma, in yoneda_]
I
i [definition, in yoneda]
i [definition, in yoneda_]
ii_dx [lemma, in cat__]
ii_dx [lemma, in cat]
ii_dx [lemma, in cat___]
ii_dx [lemma, in cat_]
ii_over [definition, in cat_over_]
ii_over [definition, in cat_over]
ii_sx [lemma, in cat___]
ii_sx [lemma, in cat__]
ii_sx [lemma, in cat]
ii_sx [lemma, in cat_]
initial_eq [lemma, in universal_]
initial_eq [lemma, in universal]
initial_extens [lemma, in universal_]
initial_extens [lemma, in universal]
initial_f_eq_g [lemma, in universal_]
initial_f_eq_g [lemma, in universal]
initial_isom [definition, in universal]
initial_isom [definition, in universal_]
initial_isom_eq [lemma, in universal]
initial_isom_eq [lemma, in universal_]
initial_isom_inv [definition, in universal]
initial_isom_inv [definition, in universal_]
initial_of_zero [definition, in universal_]
initial_of_zero [definition, in universal]
initial_src_eq [lemma, in universal]
initial_src_eq [lemma, in universal_]
Initial_Theory [definition, in universal_]
Initial_Theory [definition, in universal]
inverse_comp [definition, in map___]
inverse_comp [definition, in map_]
inverse_comp [definition, in map__]
inverse_comp [definition, in map]
inverse_dx_eq [lemma, in map__]
inverse_dx_eq [lemma, in map]
inverse_dx_eq [lemma, in map_]
inverse_dx_eq [lemma, in map___]
inverse_eq [lemma, in map__]
inverse_eq [lemma, in map]
inverse_eq [lemma, in map___]
inverse_eq [lemma, in map_]
inverse_eq_dx [lemma, in cat___]
inverse_eq_dx [lemma, in cat_]
inverse_eq_dx [lemma, in cat]
inverse_eq_dx [lemma, in cat__]
inverse_eq_sx [lemma, in cat___]
inverse_eq_sx [lemma, in cat_]
inverse_eq_sx [lemma, in cat__]
inverse_eq_sx [lemma, in cat]
inverse_inverse [definition, in map__]
inverse_inverse [definition, in map___]
inverse_inverse [definition, in map_]
inverse_inverse [definition, in map]
inverse_inverse_eq [lemma, in map__]
inverse_inverse_eq [lemma, in map]
inverse_inverse_eq [lemma, in map_]
inverse_inverse_eq [lemma, in map___]
inverse_sx_eq [lemma, in map___]
inverse_sx_eq [lemma, in map_]
inverse_sx_eq [lemma, in map__]
inverse_sx_eq [lemma, in map]
inverse_transport [definition, in map__]
inverse_transport [definition, in map]
inverse_transport [definition, in map_]
inverse_transport [definition, in map___]
inverse_unique [lemma, in map]
inverse_unique [lemma, in map_]
inverse_unique [lemma, in map___]
inverse_unique [lemma, in map__]
inv_dx [lemma, in group]
inv_dx [lemma, in cgroup_]
inv_dx [lemma, in group_]
inv_dx [lemma, in cgroup]
inv_dx_of_inv [definition, in universal_]
inv_dx_of_inv [definition, in universal]
inv_dx_prop [lemma, in universal_]
inv_dx_prop [lemma, in universal]
inv_i [definition, in yoneda_]
inv_i [definition, in yoneda]
inv_prop_dx [lemma, in universal]
inv_prop_dx [lemma, in universal_]
inv_prop_sx [lemma, in universal]
inv_prop_sx [lemma, in universal_]
inv_sx [lemma, in cgroup_]
inv_sx [lemma, in cgroup]
inv_sx [lemma, in group]
inv_sx [lemma, in group_]
inv_sx_of_inv [definition, in universal]
inv_sx_of_inv [definition, in universal_]
inv_sx_prop [lemma, in universal_]
inv_sx_prop [lemma, in universal]
inv_unique [lemma, in universal]
inv_unique [lemma, in universal_]
is_epi [definition, in universal]
is_epi [definition, in universal_]
is_injective [definition, in map__]
is_injective [definition, in map_]
is_injective [definition, in map___]
is_injective [definition, in map]
is_inv_dx [definition, in universal]
is_inv_dx [definition, in universal_]
is_inv_sx [definition, in universal]
is_inv_sx [definition, in universal_]
is_maximal_sieve_ii [lemma, in sieve_]
is_maximal_sieve_ii [lemma, in sieve]
is_maximal_target [definition, in target_]
is_maximal_target [definition, in target]
is_mono [definition, in universal_]
is_mono [definition, in universal]
is_surjective [definition, in map]
is_surjective [definition, in map_]
is_surjective [definition, in map___]
is_surjective [definition, in map__]
i_eq_k [lemma, in yoneda_]
i_eq_k [lemma, in yoneda]
J
j [definition, in yoneda]
j [definition, in yoneda_]
JMeq [inductive, in misc___]
JMeq [inductive, in misc__]
JMeq [inductive, in misc_]
JMeq [inductive, in misc]
JMeq_eqT [lemma, in misc___]
JMeq_eqT [lemma, in misc]
JMeq_eqT [lemma, in misc_]
JMeq_eqT [lemma, in misc__]
JMeq_refl [constructor, in misc__]
JMeq_refl [constructor, in misc___]
JMeq_refl [constructor, in misc]
JMeq_refl [constructor, in misc_]
JMeq_sym [lemma, in misc__]
JMeq_sym [lemma, in misc___]
JMeq_sym [lemma, in misc]
JMeq_sym [lemma, in misc_]
JMeq_transport_eqT [lemma, in misc]
JMeq_transport_eqT [lemma, in misc__]
JMeq_transport_eqT [lemma, in misc_]
JMeq_transport_eqT [lemma, in misc___]
JMeq_trs [lemma, in misc]
JMeq_trs [lemma, in misc___]
JMeq_trs [lemma, in misc__]
JMeq_trs [lemma, in misc_]
JMeq_type_eqT [lemma, in misc]
JMeq_type_eqT [lemma, in misc_]
JMeq_type_eqT [lemma, in misc__]
JMeq_type_eqT [lemma, in misc___]
K
k [definition, in yoneda]
k [definition, in yoneda_]
L
Lift [tactic definition, in quot_]
Lift [tactic definition, in quot]
M
make_inverse [definition, in map_]
make_inverse [definition, in map__]
make_inverse [definition, in map]
make_inverse [definition, in map___]
make_over [definition, in cat_over_]
make_over [definition, in cat_over]
make_small_cat [module]
make_small_cat_ [module]
make_small_cat__ [module]
make_under [definition, in cat_over]
make_under [definition, in cat_over_]
map [module]
map_ [module]
map__ [module]
map___ [module]
maximal_sieve [definition, in sieve]
maximal_sieve [definition, in sieve_]
maximal_sieve_is_maximal [lemma, in sieve]
maximal_sieve_is_maximal [lemma, in sieve_]
misc [module]
misc_ [module]
misc__ [module]
misc___ [module]
module [module]
module_ [module]
monoid [module]
monoid_ [module]
monoid_of_cmonoid [definition, in cmonoid]
monoid_of_cmonoid [definition, in cmonoid_]
monoid_of_group [definition, in group_]
monoid_of_group [definition, in group]
monoid_quot [definition, in cmonoid_quot]
monoid_quot [definition, in cmonoid_quot_]
monoid_quot [definition, in abmonoid_quot_]
monoid_quot [definition, in monoid_quot_]
monoid_quot [definition, in abmonoid_quot]
monoid_quot [definition, in monoid_quot]
monoid_quot [module]
monoid_quot_ [module]
mono_of_inv [lemma, in universal_]
mono_of_inv [lemma, in universal]
mono_of_inv_sx [lemma, in universal_]
mono_of_inv_sx [lemma, in universal]
Morph [definition, in cmonoid]
Morph [definition, in module_]
Morph [definition, in cgroup]
Morph [definition, in presheaf__]
Morph [definition, in functor_cat]
Morph [definition, in cring_]
Morph [definition, in functor_cat_]
Morph [definition, in module]
Morph [definition, in set_cat]
Morph [definition, in cat__]
Morph [definition, in monoid_]
Morph [definition, in module_]
Morph [definition, in cat]
Morph [definition, in group_]
Morph [definition, in abgroup_]
Morph [definition, in presheaf_]
Morph [definition, in cgroup_]
Morph [definition, in ring_]
Morph [definition, in abmonoid]
Morph [definition, in abmonoid_]
Morph [definition, in cat_]
Morph [definition, in cmonoid_]
Morph [definition, in module]
Morph [definition, in monoid]
Morph [definition, in set_cat_]
Morph [definition, in abgroup]
Morph [definition, in cring]
Morph [definition, in presheaf]
Morph [definition, in cat___]
Morph [definition, in ring]
Morph [definition, in group]
morph_comp [definition, in group]
morph_comp [definition, in cat__]
morph_comp [definition, in cat___]
morph_comp [definition, in abmonoid_]
morph_comp [definition, in group_]
morph_comp [definition, in cmonoid_]
morph_comp [definition, in cat]
morph_comp [definition, in abgroup_]
morph_comp [definition, in algebra_]
morph_comp [definition, in cmonoid]
morph_comp [definition, in cring_]
morph_comp [definition, in module]
morph_comp [definition, in module_]
morph_comp [definition, in ring]
morph_comp [definition, in cat_]
morph_comp [definition, in functor_cat_]
morph_comp [definition, in cgroup]
morph_comp [definition, in algebra]
morph_comp [definition, in abmonoid]
morph_comp [definition, in cgroup_]
morph_comp [definition, in ring_]
morph_comp [definition, in monoid_]
morph_comp [definition, in module]
morph_comp [definition, in functor_cat]
morph_comp [definition, in set_cat_]
morph_comp [definition, in module_]
morph_comp [definition, in cring]
morph_comp [definition, in abgroup]
morph_comp [definition, in set_cat]
morph_comp [definition, in monoid]
morph_comp_assoc [lemma, in cgroup_]
morph_comp_assoc [lemma, in ring_]
morph_comp_assoc [lemma, in group]
morph_comp_assoc [definition, in functor_cat_]
morph_comp_assoc [lemma, in ring]
morph_comp_assoc [lemma, in module_]
morph_comp_assoc [lemma, in module_]
morph_comp_assoc [lemma, in abgroup_]
morph_comp_assoc [lemma, in group_]
morph_comp_assoc [lemma, in cat___]
morph_comp_assoc [axiom, in cat_sig_]
morph_comp_assoc [axiom, in cat_sig]
morph_comp_assoc [lemma, in abgroup]
morph_comp_assoc [axiom, in cat_sig___]
morph_comp_assoc [lemma, in cmonoid_]
morph_comp_assoc [definition, in functor_cat]
morph_comp_assoc [lemma, in abmonoid_]
morph_comp_assoc [lemma, in cmonoid]
morph_comp_assoc [lemma, in cat__]
morph_comp_assoc [lemma, in monoid]
morph_comp_assoc [lemma, in module]
morph_comp_assoc [lemma, in module]
morph_comp_assoc [axiom, in cat_sig__]
morph_comp_assoc [lemma, in cring_]
morph_comp_assoc [lemma, in set_cat_]
morph_comp_assoc [lemma, in cat]
morph_comp_assoc [lemma, in cat_]
morph_comp_assoc [lemma, in abmonoid]
morph_comp_assoc [lemma, in set_cat]
morph_comp_assoc [lemma, in cgroup]
morph_comp_assoc [lemma, in monoid_]
morph_comp_assoc [lemma, in cring]
morph_extens [lemma, in cgroup_]
morph_extens [lemma, in cmonoid_]
morph_extens [lemma, in module_]
morph_extens [lemma, in ring]
morph_extens [lemma, in abmonoid]
morph_extens [lemma, in monoid]
morph_extens [lemma, in cring]
morph_extens [lemma, in cmonoid]
morph_extens [lemma, in group]
morph_extens [lemma, in cring_]
morph_extens [lemma, in group_]
morph_extens [lemma, in abgroup]
morph_extens [lemma, in ring_]
morph_extens [lemma, in module]
morph_extens [lemma, in abgroup_]
morph_extens [lemma, in monoid_]
morph_extens [lemma, in abmonoid_]
morph_extens [lemma, in cgroup]
morph_id [definition, in group_]
morph_id [definition, in abgroup_]
morph_id [definition, in monoid]
morph_id [definition, in ring_]
morph_id [definition, in set_cat_]
morph_id [definition, in cat___]
morph_id [definition, in cat]
morph_id [definition, in abgroup]
morph_id [definition, in functor_cat]
morph_id [definition, in cring_]
morph_id [definition, in cmonoid_]
morph_id [definition, in cring]
morph_id [definition, in module]
morph_id [definition, in cgroup]
morph_id [definition, in ring]
morph_id [definition, in cmonoid]
morph_id [definition, in group]
morph_id [definition, in module]
morph_id [definition, in cat_]
morph_id [definition, in module_]
morph_id [definition, in abmonoid_]
morph_id [definition, in abmonoid]
morph_id [definition, in set_cat]
morph_id [definition, in cgroup_]
morph_id [definition, in functor_cat_]
morph_id [definition, in cat__]
morph_id [definition, in module_]
morph_id [definition, in monoid_]
morph_id_dx [lemma, in module_]
morph_id_dx [lemma, in ring]
morph_id_dx [lemma, in abgroup]
morph_id_dx [lemma, in monoid]
morph_id_dx [lemma, in cat_]
morph_id_dx [lemma, in cring]
morph_id_dx [lemma, in group_]
morph_id_dx [definition, in functor_cat_]
morph_id_dx [lemma, in group]
morph_id_dx [lemma, in cat__]
morph_id_dx [axiom, in cat_sig___]
morph_id_dx [definition, in set_cat_]
morph_id_dx [lemma, in module_]
morph_id_dx [lemma, in abmonoid_]
morph_id_dx [definition, in set_cat]
morph_id_dx [lemma, in cmonoid_]
morph_id_dx [lemma, in cgroup]
morph_id_dx [lemma, in cgroup_]
morph_id_dx [lemma, in module]
morph_id_dx [lemma, in monoid_]
morph_id_dx [lemma, in cring_]
morph_id_dx [lemma, in abgroup_]
morph_id_dx [definition, in functor_cat]
morph_id_dx [axiom, in cat_sig__]
morph_id_dx [axiom, in cat_sig]
morph_id_dx [lemma, in cat___]
morph_id_dx [lemma, in ring_]
morph_id_dx [axiom, in cat_sig_]
morph_id_dx [lemma, in cmonoid]
morph_id_dx [lemma, in module]
morph_id_dx [lemma, in cat]
morph_id_dx [lemma, in abmonoid]
morph_id_sx [lemma, in group]
morph_id_sx [lemma, in abmonoid]
morph_id_sx [lemma, in cgroup_]
morph_id_sx [lemma, in module]
morph_id_sx [lemma, in group_]
morph_id_sx [lemma, in cat__]
morph_id_sx [definition, in functor_cat_]
morph_id_sx [lemma, in monoid_]
morph_id_sx [lemma, in cat_]
morph_id_sx [lemma, in cmonoid]
morph_id_sx [lemma, in module_]
morph_id_sx [lemma, in abgroup]
morph_id_sx [lemma, in cat___]
morph_id_sx [definition, in set_cat]
morph_id_sx [lemma, in ring]
morph_id_sx [lemma, in module]
morph_id_sx [definition, in set_cat_]
morph_id_sx [axiom, in cat_sig_]
morph_id_sx [axiom, in cat_sig___]
morph_id_sx [lemma, in cat]
morph_id_sx [lemma, in abmonoid_]
morph_id_sx [lemma, in cring_]
morph_id_sx [axiom, in cat_sig]
morph_id_sx [axiom, in cat_sig__]
morph_id_sx [lemma, in module_]
morph_id_sx [lemma, in cmonoid_]
morph_id_sx [lemma, in cgroup]
morph_id_sx [lemma, in abgroup_]
morph_id_sx [lemma, in cring]
morph_id_sx [lemma, in ring_]
morph_id_sx [lemma, in monoid]
morph_id_sx [definition, in functor_cat]
Morph_Theory [definition, in algebra_]
Morph_Theory [definition, in algebra]
mor_of_mor_over [definition, in cat_over]
mor_of_mor_over [definition, in cat_over_]
mor_of_obj_over [definition, in cat_over]
mor_of_obj_over [definition, in cat_over_]
mor_over [inductive, in cat_over_]
mor_over [inductive, in cat_over]
mor_over_extens [lemma, in cat_over_]
mor_over_extens [lemma, in cat_over]
mor_over_intro [constructor, in cat_over]
mor_over_intro [constructor, in cat_over_]
mul_assoc [lemma, in cmonoid_]
mul_assoc [lemma, in group_]
mul_assoc [lemma, in monoid]
mul_assoc [lemma, in cgroup_]
mul_assoc [lemma, in ring_]
mul_assoc [lemma, in monoid_]
mul_assoc [lemma, in cgroup]
mul_assoc [lemma, in cring_]
mul_assoc [lemma, in ring]
mul_assoc [lemma, in cmonoid]
mul_assoc [lemma, in group]
mul_assoc [lemma, in cring]
mul_commut [lemma, in cmonoid]
mul_commut [lemma, in cgroup]
mul_commut [lemma, in cring_]
mul_commut [lemma, in cring]
mul_commut [lemma, in cgroup_]
mul_commut [lemma, in cmonoid_]
mul_sx_cancel [lemma, in cgroup_]
mul_sx_cancel [lemma, in cgroup]
mul_sx_cancel [lemma, in group]
mul_sx_cancel [lemma, in group_]
N
nondep_extensionality [lemma, in misc__]
nondep_extensionality [lemma, in misc___]
nondep_extensionality [lemma, in misc]
nondep_extensionality [lemma, in misc_]
non_empty [inductive, in misc__]
non_empty [inductive, in misc]
non_empty [inductive, in misc___]
non_empty [inductive, in misc_]
non_empty_intro [constructor, in misc_]
non_empty_intro [constructor, in misc]
non_empty_intro [constructor, in misc___]
non_empty_intro [constructor, in misc__]
nt [module]
nt'_comm [lemma, in presheaf]
nt'_comm [lemma, in presheaf_]
NT'_Comm [definition, in presheaf__]
NT'_Comm [definition, in presheaf]
NT'_Comm [definition, in presheaf_]
nt'_comm [lemma, in presheaf__]
nt'_comp [definition, in presheaf_]
nt'_comp [definition, in presheaf]
nt'_comp [definition, in presheaf__]
nt'_comp_assoc [lemma, in presheaf__]
nt'_comp_assoc [lemma, in presheaf_]
nt'_comp_assoc [lemma, in presheaf]
nt'_dx_id [lemma, in presheaf_]
nt'_dx_id [lemma, in presheaf__]
nt'_dx_id [lemma, in presheaf]
nt'_extens [lemma, in presheaf__]
nt'_extens [lemma, in presheaf]
nt'_extens [lemma, in presheaf_]
nt'_id [definition, in presheaf__]
nt'_id [definition, in presheaf_]
nt'_id [definition, in presheaf]
nt'_sx_id [lemma, in presheaf__]
nt'_sx_id [lemma, in presheaf]
nt'_sx_id [lemma, in presheaf_]
nt_ [module]
NT_Comm [definition, in nt__]
nt_comm [lemma, in nt]
nt_comm [lemma, in nt_]
nt_comm [lemma, in nt__]
NT_Comm [definition, in nt_]
NT_Comm [definition, in nt]
nt_comp [definition, in nt__]
nt_comp [definition, in nt_]
nt_comp [definition, in nt]
nt_comp_assoc [lemma, in nt__]
nt_comp_assoc [lemma, in nt]
nt_comp_assoc [lemma, in nt_]
nt_dx_id [lemma, in nt__]
nt_dx_id [lemma, in nt]
nt_dx_id [lemma, in nt_]
nt_extens [lemma, in nt__]
nt_extens [lemma, in nt_]
nt_extens [lemma, in nt]
nt_h [definition, in yoneda_]
nt_h [definition, in yoneda]
nt_id [definition, in nt]
nt_id [definition, in nt__]
nt_id [definition, in nt_]
nt_sx_id [lemma, in nt__]
nt_sx_id [lemma, in nt_]
nt_sx_id [lemma, in nt]
nt__ [module]
O
Obj [definition, in ring]
Obj [definition, in module]
Obj [definition, in cgroup]
Obj [definition, in cgroup_]
Obj [axiom, in cat_sig___]
Obj [definition, in module]
Obj [definition, in cmonoid]
Obj [definition, in group]
Obj [definition, in abmonoid_]
Obj [definition, in cat_]
Obj [axiom, in cat_sig__]
Obj [definition, in set_cat_]
Obj [definition, in monoid]
Obj [definition, in set_cat]
Obj [definition, in cat]
Obj [definition, in abgroup_]
Obj [definition, in cmonoid_]
Obj [definition, in abgroup]
Obj [axiom, in cat_sig_]
Obj [definition, in cring]
Obj [definition, in functor_cat]
Obj [definition, in ring_]
Obj [definition, in functor_cat_]
Obj [definition, in cat___]
Obj [definition, in module_]
Obj [axiom, in cat_sig]
Obj [definition, in monoid_]
Obj [definition, in module_]
Obj [definition, in abmonoid]
Obj [definition, in group_]
Obj [definition, in cring_]
Obj [definition, in cat__]
obj_of_obj_over [definition, in cat_over]
obj_of_obj_over [definition, in cat_over_]
obj_over [inductive, in cat_over_]
obj_over [inductive, in cat_over]
obj_over_intro [constructor, in cat_over_]
obj_over_intro [constructor, in cat_over]
one_dx [lemma, in monoid]
one_dx [lemma, in cgroup]
one_dx [lemma, in cmonoid_]
one_dx [lemma, in cgroup_]
one_dx [lemma, in group_]
one_dx [lemma, in monoid_]
one_dx [lemma, in ring]
one_dx [lemma, in group]
one_dx [lemma, in cmonoid]
one_dx [lemma, in ring_]
one_sx [lemma, in monoid]
one_sx [lemma, in ring]
one_sx [lemma, in cmonoid]
one_sx [lemma, in group]
one_sx [lemma, in cgroup]
one_sx [lemma, in monoid_]
one_sx [lemma, in cgroup_]
one_sx [lemma, in cmonoid_]
one_sx [lemma, in cring]
one_sx [lemma, in ring_]
one_sx [lemma, in cring_]
one_sx [lemma, in group_]
oo_assoc [lemma, in cat_]
oo_assoc [lemma, in cat]
oo_assoc [lemma, in cat__]
oo_assoc [lemma, in cat___]
oo_congr [lemma, in cat_]
oo_congr [lemma, in cat__]
oo_congr [lemma, in cat___]
oo_congr [lemma, in cat]
oo_over [definition, in cat_over]
oo_over [definition, in cat_over_]
opp_dx [lemma, in abgroup_]
opp_dx [lemma, in abgroup]
opp_sx [lemma, in ring]
opp_sx [lemma, in cring]
opp_sx [lemma, in abgroup]
opp_sx [lemma, in cring_]
opp_sx [lemma, in abgroup_]
opp_sx [lemma, in ring_]
P
plug [lemma, in misc___]
plug [lemma, in misc]
plug [lemma, in misc__]
plug [lemma, in misc_]
plug2 [lemma, in misc___]
plug2 [lemma, in misc]
plug2 [lemma, in misc_]
plug2 [lemma, in misc__]
plug2_dx [lemma, in misc]
plug2_dx [lemma, in misc___]
plug2_dx [lemma, in misc__]
plug2_dx [lemma, in misc_]
plug2_sx [lemma, in misc]
plug2_sx [lemma, in misc___]
plug2_sx [lemma, in misc__]
plug2_sx [lemma, in misc_]
presheaf [module]
presheaf_ [module]
Presheaf_Cat [definition, in presheaf__]
Presheaf_Cat [definition, in presheaf_]
Presheaf_Cat [definition, in presheaf]
presheaf_extens [lemma, in presheaf_]
presheaf_extens [lemma, in presheaf]
presheaf_extens [lemma, in presheaf__]
presheaf__ [module]
presh_ii [lemma, in presheaf_]
presh_ii [lemma, in presheaf]
presh_ii [lemma, in presheaf__]
presh_oo [lemma, in presheaf]
presh_oo [lemma, in presheaf__]
presh_oo [lemma, in presheaf_]
product [module]
product_ [module]
product_assoc [definition, in product]
product_assoc [definition, in product_]
product_assoc_inv [definition, in product]
product_assoc_inv [definition, in product_]
product_comm [definition, in product_]
product_comm [definition, in product]
product_comm_inv [definition, in product]
product_comm_inv [definition, in product_]
product_dx_eq [lemma, in product_]
product_dx_eq [lemma, in product]
product_eq [lemma, in product]
product_eq [lemma, in product_]
product_f_eq_g [lemma, in product_]
product_f_eq_g [lemma, in product]
product_isom [definition, in product_]
product_isom [definition, in product]
product_isom_eq [lemma, in product_]
product_isom_eq [lemma, in product]
product_isom_inv [definition, in product_]
product_isom_inv [definition, in product]
product_sx_eq [lemma, in product]
product_sx_eq [lemma, in product_]
proof_irrelevance [axiom, in misc]
proof_irrelevance [axiom, in misc_]
proof_irrelevance [axiom, in misc__]
proof_irrelevance [axiom, in misc___]
prop_of_type [inductive, in misc___]
prop_of_type [inductive, in misc__]
prop_of_type [inductive, in misc]
prop_of_type [inductive, in misc_]
prop_of_type_intro [constructor, in misc___]
prop_of_type_intro [constructor, in misc]
prop_of_type_intro [constructor, in misc_]
prop_of_type_intro [constructor, in misc__]
prop_uni [axiom, in misc__]
prop_uni [axiom, in misc___]
prop_uni [axiom, in misc_]
prop_uni [axiom, in misc]
pullback [definition, in fibprod]
pullback [definition, in fibprod_]
pullback_eq [lemma, in fibprod]
pullback_eq [lemma, in fibprod_]
pullback_mor [definition, in fibprod_]
pullback_mor [definition, in fibprod]
pullback_target [inductive, in target]
pullback_target [inductive, in target_]
pullback_target_intro [constructor, in target_]
pullback_target_intro [constructor, in target]
Q
quot [axiom, in quot_]
quot [axiom, in quot]
quot [module]
quot_ [module]
quot_fix_universe [definition, in quot_]
quot_fix_universe [definition, in quot]
quot_law [definition, in quot]
quot_law [definition, in quot_]
quot_law2 [definition, in quot]
quot_law2 [definition, in quot_]
R
R [definition, in small_ring]
R [definition, in small_ring_]
R [axiom, in module_]
R [axiom, in small_ring]
R [axiom, in small_ring_]
R [axiom, in module]
ring [module]
ring_ [module]
S
section_comp [definition, in map__]
section_comp [definition, in map]
section_comp [definition, in map___]
section_comp [definition, in map_]
section_eq_cosection [lemma, in map]
section_eq_cosection [lemma, in map___]
section_eq_cosection [lemma, in map__]
section_eq_cosection [lemma, in map_]
section_of_inverse [definition, in map]
section_of_inverse [definition, in map_]
section_of_inverse [definition, in map__]
section_of_inverse [definition, in map___]
section_surj [lemma, in map__]
section_surj [lemma, in map_]
section_surj [lemma, in map]
section_surj [lemma, in map___]
set [definition, in yoneda_]
set [definition, in yoneda]
set_cat [module]
set_cat_ [module]
Set_Of [inductive, in misc_]
Set_Of [inductive, in misc__]
Set_Of [inductive, in misc___]
Set_Of [inductive, in misc]
set_of_intro [constructor, in misc_]
set_of_intro [constructor, in misc___]
set_of_intro [constructor, in misc__]
set_of_intro [constructor, in misc]
sieve [module]
sieve_ [module]
sieve_comp [definition, in sieve_]
sieve_comp [definition, in sieve]
sieve_comp_prop [lemma, in sieve]
sieve_comp_prop [lemma, in sieve_]
sieve_extens [lemma, in sieve_]
sieve_extens [lemma, in sieve]
sieve_prop [lemma, in sieve]
sieve_prop [lemma, in sieve_]
sieve_set_prop [lemma, in sieve]
sieve_set_prop [lemma, in sieve_]
Sieve_Theory [definition, in sieve]
Sieve_Theory [definition, in sieve_]
sieve_transport [definition, in sieve_]
sieve_transport [definition, in sieve]
sieve_transport_trans [lemma, in sieve_]
sieve_transport_trans [lemma, in sieve]
Skip [tactic definition, in cool]
small_group [module]
small_group_ [module]
small_monoid [module]
small_monoid_ [module]
small_ring [module]
small_ring_ [module]
src [definition, in cat__]
src [definition, in cat_]
src [definition, in cat]
src [definition, in cat___]
T
Target [definition, in target]
Target [definition, in target_]
target [module]
target_ [module]
target_comp [inductive, in target]
target_comp [inductive, in target_]
target_comp_intro [constructor, in target_]
target_comp_intro [constructor, in target]
target_extens [lemma, in target]
target_extens [lemma, in target_]
target_of_mor [inductive, in target]
target_of_mor [inductive, in target_]
target_of_mor_intro [constructor, in target]
target_of_mor_intro [constructor, in target_]
target_sub [definition, in target_]
target_sub [definition, in target]
target_transport [definition, in target]
target_transport [definition, in target_]
target_transport_trans [lemma, in target]
target_transport_trans [lemma, in target_]
topology [module]
topology_ [module]
top_coerence [lemma, in topology]
top_coerence [lemma, in topology_]
top_comp [lemma, in topology_]
top_comp [lemma, in topology]
top_larger [lemma, in topology]
top_larger [lemma, in topology_]
top_maximal [lemma, in topology_]
top_maximal [lemma, in topology]
top_transitivity [lemma, in topology_]
top_transitivity [lemma, in topology]
top_transport [lemma, in topology]
top_transport [lemma, in topology_]
top_trans_arrow [lemma, in topology_]
top_trans_arrow [lemma, in topology]
transport [definition, in misc___]
transport [definition, in misc__]
transport [definition, in misc_]
transport [definition, in misc]
transport_eq [lemma, in misc_]
transport_eq [lemma, in misc__]
transport_eq [lemma, in misc]
transport_eq [lemma, in misc___]
transport_refl [lemma, in misc___]
transport_refl [lemma, in misc]
transport_refl [lemma, in misc_]
transport_refl [lemma, in misc__]
trg [definition, in cat]
trg [definition, in cat___]
trg [definition, in cat__]
trg [definition, in cat_]
TypeQ [definition, in quot]
TypeQ [definition, in quot_]
type_of [definition, in misc__]
type_of [definition, in misc___]
type_of [definition, in misc]
type_of [definition, in misc_]
U
universal [module]
universal_ [module]
Y
yoneda [definition, in yoneda]
yoneda [definition, in yoneda_]
yoneda [module]
yoneda_ [module]
yoneda_bij [definition, in yoneda]
yoneda_bij [definition, in yoneda_]
yoneda_bij_inv [definition, in yoneda_]
yoneda_bij_inv [definition, in yoneda]
yoneda_data [definition, in yoneda_]
yoneda_data [definition, in yoneda]
yoneda_embedding [definition, in yoneda]
yoneda_embedding [definition, in yoneda_]
Z
zero_dx [lemma, in abmonoid_]
zero_dx [lemma, in abgroup_]
zero_dx [lemma, in abgroup]
zero_dx [lemma, in abmonoid]
zero_sx [lemma, in abgroup]
zero_sx [lemma, in cring]
zero_sx [lemma, in abmonoid]
zero_sx [lemma, in ring]
zero_sx [lemma, in ring_]
zero_sx [lemma, in abmonoid_]
zero_sx [lemma, in abgroup_]
zero_sx [lemma, in cring_]
Tactic Index
L
Lift [in quot_]
Lift [in quot]
S
Skip [in cool]
Axiom Index
C
class [in quot]
class [in quot_]
class_eq [in quot_]
class_eq [in quot]
class_rel [in quot]
class_rel [in quot_]
class_surj [in quot]
class_surj [in quot_]
cool [in cool]
E
extensionality [in misc___]
extensionality [in misc_]
extensionality [in misc__]
extensionality [in misc]
F
fact [in quot_]
fact [in quot]
fact_comm [in quot_]
fact_comm [in quot]
M
morph_comp_assoc [in cat_sig_]
morph_comp_assoc [in cat_sig]
morph_comp_assoc [in cat_sig___]
morph_comp_assoc [in cat_sig__]
morph_id_dx [in cat_sig___]
morph_id_dx [in cat_sig__]
morph_id_dx [in cat_sig]
morph_id_dx [in cat_sig_]
morph_id_sx [in cat_sig_]
morph_id_sx [in cat_sig___]
morph_id_sx [in cat_sig]
morph_id_sx [in cat_sig__]
O
Obj [in cat_sig___]
Obj [in cat_sig__]
Obj [in cat_sig_]
Obj [in cat_sig]
P
proof_irrelevance [in misc]
proof_irrelevance [in misc_]
proof_irrelevance [in misc__]
proof_irrelevance [in misc___]
prop_uni [in misc__]
prop_uni [in misc___]
prop_uni [in misc_]
prop_uni [in misc]
Q
quot [in quot_]
quot [in quot]
R
R [in module_]
R [in small_ring]
R [in small_ring_]
R [in module]
Lemma Index
A
add_assoc [in abgroup_]
add_assoc [in cring]
add_assoc [in ring]
add_assoc [in abmonoid_]
add_assoc [in abgroup]
add_assoc [in abmonoid]
add_assoc [in ring_]
add_assoc [in cring_]
add_commut [in ring_]
add_commut [in abmonoid_]
add_commut [in abmonoid]
add_commut [in cring_]
add_commut [in cring]
add_commut [in ring]
add_commut [in abgroup]
add_commut [in abgroup_]
add_sx_cancel [in abgroup]
add_sx_cancel [in abgroup_]
B
bijection_eq1 [in map]
bijection_eq1 [in map__]
bijection_eq1 [in map_]
bijection_eq1 [in map___]
bijection_eq2 [in map_]
bijection_eq2 [in map__]
bijection_eq2 [in map]
bijection_eq2 [in map___]
C
class_congr [in quot_]
class_congr [in quot]
compatible_compatible2 [in quot]
compatible_compatible2 [in quot_]
compatible_dx [in quot_]
compatible_dx [in quot]
compatible_sx [in quot_]
compatible_sx [in quot]
congr [in misc]
congr [in misc___]
congr [in misc__]
congr [in misc_]
congr2 [in misc]
congr2 [in misc__]
congr2 [in misc___]
congr2 [in misc_]
cosection_inj [in map]
cosection_inj [in map___]
cosection_inj [in map__]
cosection_inj [in map_]
cov_obj_transport [in topology_]
cov_obj_transport [in topology]
cov_sieve_geq [in topology]
cov_sieve_geq [in topology_]
D
distrib_dx [in cring]
distrib_dx [in cring_]
distrib_dx [in ring_]
distrib_dx [in ring]
distrib_sx [in ring]
distrib_sx [in ring_]
distrib_sx [in cring_]
distrib_sx [in cring]
E
epi_of_inv [in universal_]
epi_of_inv [in universal]
epi_of_inv_dx [in universal_]
epi_of_inv_dx [in universal]
eqT_JMeq [in misc]
eqT_JMeq [in misc_]
eqT_JMeq [in misc__]
eqT_JMeq [in misc___]
eqT_rect_simpl [in misc]
eqT_rect_simpl [in misc_]
eqT_rect_simpl [in misc___]
eqT_rect_simpl [in misc__]
eqv_eqT [in equiv_]
eqv_eqT [in equiv]
eqv_refl [in equiv_]
eqv_refl [in equiv]
eqv_sym [in equiv_]
eqv_sym [in equiv]
eqv_trans [in equiv_]
eqv_trans [in equiv]
eq_fct_obj [in cat___]
eq_fct_obj [in cat]
eq_fct_obj [in cat__]
eq_fct_obj [in cat_]
eq_fct_src [in cat__]
eq_fct_src [in cat_]
eq_fct_src [in cat___]
eq_fct_src [in cat]
eq_fct_trg [in cat]
eq_fct_trg [in cat_]
eq_fct_trg [in cat__]
eq_fct_trg [in cat___]
eq_from_inverse_eq [in map__]
eq_from_inverse_eq [in map_]
eq_from_inverse_eq [in map]
eq_from_inverse_eq [in map___]
eq_mor_eqT [in cat_]
eq_mor_eqT [in cat___]
eq_mor_eqT [in cat__]
eq_mor_eqT [in cat]
eq_mor_src [in cat__]
eq_mor_src [in cat_]
eq_mor_src [in cat]
eq_mor_src [in cat___]
eq_mor_sym [in cat___]
eq_mor_sym [in cat_]
eq_mor_sym [in cat]
eq_mor_sym [in cat__]
eq_mor_trans [in cat]
eq_mor_trans [in cat___]
eq_mor_trans [in cat__]
eq_mor_trans [in cat_]
eq_mor_trg [in cat_]
eq_mor_trg [in cat]
eq_mor_trg [in cat___]
eq_mor_trg [in cat__]
eq_presh_obj [in presheaf__]
eq_presh_obj [in presheaf_]
eq_presh_obj [in presheaf]
eq_presh_src [in presheaf__]
eq_presh_src [in presheaf]
eq_presh_src [in presheaf_]
eq_presh_trg [in presheaf__]
eq_presh_trg [in presheaf_]
eq_presh_trg [in presheaf]
F
fact2_comm [in quot]
fact2_comm [in quot_]
fact2_eq [in quot]
fact2_eq [in quot_]
fact_eq [in quot]
fact_eq [in quot_]
fct_ii [in cat__]
fct_ii [in cat___]
fct_ii [in cat_]
fct_ii [in cat]
fct_oo [in cat__]
fct_oo [in cat___]
fct_oo [in cat]
fct_oo [in cat_]
final_eq [in universal_]
final_eq [in universal]
final_extens [in universal_]
final_extens [in universal]
final_f_eq_g [in universal_]
final_f_eq_g [in universal]
final_isom_eq [in universal]
final_isom_eq [in universal_]
functor_extens [in cat___]
functor_extens [in cat]
functor_extens [in cat__]
functor_extens [in cat_]
H
h_theory [in yoneda]
h_theory [in yoneda_]
I
ii_dx [in cat__]
ii_dx [in cat]
ii_dx [in cat___]
ii_dx [in cat_]
ii_sx [in cat___]
ii_sx [in cat__]
ii_sx [in cat]
ii_sx [in cat_]
initial_eq [in universal_]
initial_eq [in universal]
initial_extens [in universal_]
initial_extens [in universal]
initial_f_eq_g [in universal_]
initial_f_eq_g [in universal]
initial_isom_eq [in universal]
initial_isom_eq [in universal_]
initial_src_eq [in universal]
initial_src_eq [in universal_]
inverse_dx_eq [in map__]
inverse_dx_eq [in map]
inverse_dx_eq [in map_]
inverse_dx_eq [in map___]
inverse_eq [in map__]
inverse_eq [in map]
inverse_eq [in map___]
inverse_eq [in map_]
inverse_eq_dx [in cat___]
inverse_eq_dx [in cat_]
inverse_eq_dx [in cat]
inverse_eq_dx [in cat__]
inverse_eq_sx [in cat___]
inverse_eq_sx [in cat_]
inverse_eq_sx [in cat__]
inverse_eq_sx [in cat]
inverse_inverse_eq [in map__]
inverse_inverse_eq [in map]
inverse_inverse_eq [in map_]
inverse_inverse_eq [in map___]
inverse_sx_eq [in map___]
inverse_sx_eq [in map_]
inverse_sx_eq [in map__]
inverse_sx_eq [in map]
inverse_unique [in map]
inverse_unique [in map_]
inverse_unique [in map___]
inverse_unique [in map__]
inv_dx [in group]
inv_dx [in cgroup_]
inv_dx [in group_]
inv_dx [in cgroup]
inv_dx_prop [in universal_]
inv_dx_prop [in universal]
inv_prop_dx [in universal]
inv_prop_dx [in universal_]
inv_prop_sx [in universal]
inv_prop_sx [in universal_]
inv_sx [in cgroup_]
inv_sx [in cgroup]
inv_sx [in group]
inv_sx [in group_]
inv_sx_prop [in universal_]
inv_sx_prop [in universal]
inv_unique [in universal]
inv_unique [in universal_]
is_maximal_sieve_ii [in sieve_]
is_maximal_sieve_ii [in sieve]
i_eq_k [in yoneda_]
i_eq_k [in yoneda]
J
JMeq_eqT [in misc___]
JMeq_eqT [in misc]
JMeq_eqT [in misc_]
JMeq_eqT [in misc__]
JMeq_sym [in misc__]
JMeq_sym [in misc___]
JMeq_sym [in misc]
JMeq_sym [in misc_]
JMeq_transport_eqT [in misc]
JMeq_transport_eqT [in misc__]
JMeq_transport_eqT [in misc_]
JMeq_transport_eqT [in misc___]
JMeq_trs [in misc]
JMeq_trs [in misc___]
JMeq_trs [in misc__]
JMeq_trs [in misc_]
JMeq_type_eqT [in misc]
JMeq_type_eqT [in misc_]
JMeq_type_eqT [in misc__]
JMeq_type_eqT [in misc___]
M
maximal_sieve_is_maximal [in sieve]
maximal_sieve_is_maximal [in sieve_]
mono_of_inv [in universal_]
mono_of_inv [in universal]
mono_of_inv_sx [in universal_]
mono_of_inv_sx [in universal]
morph_comp_assoc [in cgroup_]
morph_comp_assoc [in ring_]
morph_comp_assoc [in group]
morph_comp_assoc [in ring]
morph_comp_assoc [in module_]
morph_comp_assoc [in module_]
morph_comp_assoc [in abgroup_]
morph_comp_assoc [in group_]
morph_comp_assoc [in cat___]
morph_comp_assoc [in abgroup]
morph_comp_assoc [in cmonoid_]
morph_comp_assoc [in abmonoid_]
morph_comp_assoc [in cmonoid]
morph_comp_assoc [in cat__]
morph_comp_assoc [in monoid]
morph_comp_assoc [in module]
morph_comp_assoc [in module]
morph_comp_assoc [in cring_]
morph_comp_assoc [in set_cat_]
morph_comp_assoc [in cat]
morph_comp_assoc [in cat_]
morph_comp_assoc [in abmonoid]
morph_comp_assoc [in set_cat]
morph_comp_assoc [in cgroup]
morph_comp_assoc [in monoid_]
morph_comp_assoc [in cring]
morph_extens [in cgroup_]
morph_extens [in cmonoid_]
morph_extens [in module_]
morph_extens [in ring]
morph_extens [in abmonoid]
morph_extens [in monoid]
morph_extens [in cring]
morph_extens [in cmonoid]
morph_extens [in group]
morph_extens [in cring_]
morph_extens [in group_]
morph_extens [in abgroup]
morph_extens [in ring_]
morph_extens [in module]
morph_extens [in abgroup_]
morph_extens [in monoid_]
morph_extens [in abmonoid_]
morph_extens [in cgroup]
morph_id_dx [in module_]
morph_id_dx [in ring]
morph_id_dx [in abgroup]
morph_id_dx [in monoid]
morph_id_dx [in cat_]
morph_id_dx [in cring]
morph_id_dx [in group_]
morph_id_dx [in group]
morph_id_dx [in cat__]
morph_id_dx [in module_]
morph_id_dx [in abmonoid_]
morph_id_dx [in cmonoid_]
morph_id_dx [in cgroup]
morph_id_dx [in cgroup_]
morph_id_dx [in module]
morph_id_dx [in monoid_]
morph_id_dx [in cring_]
morph_id_dx [in abgroup_]
morph_id_dx [in cat___]
morph_id_dx [in ring_]
morph_id_dx [in cmonoid]
morph_id_dx [in module]
morph_id_dx [in cat]
morph_id_dx [in abmonoid]
morph_id_sx [in group]
morph_id_sx [in abmonoid]
morph_id_sx [in cgroup_]
morph_id_sx [in module]
morph_id_sx [in group_]
morph_id_sx [in cat__]
morph_id_sx [in monoid_]
morph_id_sx [in cat_]
morph_id_sx [in cmonoid]
morph_id_sx [in module_]
morph_id_sx [in abgroup]
morph_id_sx [in cat___]
morph_id_sx [in ring]
morph_id_sx [in module]
morph_id_sx [in cat]
morph_id_sx [in abmonoid_]
morph_id_sx [in cring_]
morph_id_sx [in module_]
morph_id_sx [in cmonoid_]
morph_id_sx [in cgroup]
morph_id_sx [in abgroup_]
morph_id_sx [in cring]
morph_id_sx [in ring_]
morph_id_sx [in monoid]
mor_over_extens [in cat_over_]
mor_over_extens [in cat_over]
mul_assoc [in cmonoid_]
mul_assoc [in group_]
mul_assoc [in monoid]
mul_assoc [in cgroup_]
mul_assoc [in ring_]
mul_assoc [in monoid_]
mul_assoc [in cgroup]
mul_assoc [in cring_]
mul_assoc [in ring]
mul_assoc [in cmonoid]
mul_assoc [in group]
mul_assoc [in cring]
mul_commut [in cmonoid]
mul_commut [in cgroup]
mul_commut [in cring_]
mul_commut [in cring]
mul_commut [in cgroup_]
mul_commut [in cmonoid_]
mul_sx_cancel [in cgroup_]
mul_sx_cancel [in cgroup]
mul_sx_cancel [in group]
mul_sx_cancel [in group_]
N
nondep_extensionality [in misc__]
nondep_extensionality [in misc___]
nondep_extensionality [in misc]
nondep_extensionality [in misc_]
nt'_comm [in presheaf]
nt'_comm [in presheaf_]
nt'_comm [in presheaf__]
nt'_comp_assoc [in presheaf__]
nt'_comp_assoc [in presheaf_]
nt'_comp_assoc [in presheaf]
nt'_dx_id [in presheaf_]
nt'_dx_id [in presheaf__]
nt'_dx_id [in presheaf]
nt'_extens [in presheaf__]
nt'_extens [in presheaf]
nt'_extens [in presheaf_]
nt'_sx_id [in presheaf__]
nt'_sx_id [in presheaf]
nt'_sx_id [in presheaf_]
nt_comm [in nt]
nt_comm [in nt_]
nt_comm [in nt__]
nt_comp_assoc [in nt__]
nt_comp_assoc [in nt]
nt_comp_assoc [in nt_]
nt_dx_id [in nt__]
nt_dx_id [in nt]
nt_dx_id [in nt_]
nt_extens [in nt__]
nt_extens [in nt_]
nt_extens [in nt]
nt_sx_id [in nt__]
nt_sx_id [in nt_]
nt_sx_id [in nt]
O
one_dx [in monoid]
one_dx [in cgroup]
one_dx [in cmonoid_]
one_dx [in cgroup_]
one_dx [in group_]
one_dx [in monoid_]
one_dx [in ring]
one_dx [in group]
one_dx [in cmonoid]
one_dx [in ring_]
one_sx [in monoid]
one_sx [in ring]
one_sx [in cmonoid]
one_sx [in group]
one_sx [in cgroup]
one_sx [in monoid_]
one_sx [in cgroup_]
one_sx [in cmonoid_]
one_sx [in cring]
one_sx [in ring_]
one_sx [in cring_]
one_sx [in group_]
oo_assoc [in cat_]
oo_assoc [in cat]
oo_assoc [in cat__]
oo_assoc [in cat___]
oo_congr [in cat_]
oo_congr [in cat__]
oo_congr [in cat___]
oo_congr [in cat]
opp_dx [in abgroup_]
opp_dx [in abgroup]
opp_sx [in ring]
opp_sx [in cring]
opp_sx [in abgroup]
opp_sx [in cring_]
opp_sx [in abgroup_]
opp_sx [in ring_]
P
plug [in misc___]
plug [in misc]
plug [in misc__]
plug [in misc_]
plug2 [in misc___]
plug2 [in misc]
plug2 [in misc_]
plug2 [in misc__]
plug2_dx [in misc]
plug2_dx [in misc___]
plug2_dx [in misc__]
plug2_dx [in misc_]
plug2_sx [in misc]
plug2_sx [in misc___]
plug2_sx [in misc__]
plug2_sx [in misc_]
presheaf_extens [in presheaf_]
presheaf_extens [in presheaf]
presheaf_extens [in presheaf__]
presh_ii [in presheaf_]
presh_ii [in presheaf]
presh_ii [in presheaf__]
presh_oo [in presheaf]
presh_oo [in presheaf__]
presh_oo [in presheaf_]
product_dx_eq [in product_]
product_dx_eq [in product]
product_eq [in product]
product_eq [in product_]
product_f_eq_g [in product_]
product_f_eq_g [in product]
product_isom_eq [in product_]
product_isom_eq [in product]
product_sx_eq [in product]
product_sx_eq [in product_]
pullback_eq [in fibprod]
pullback_eq [in fibprod_]
S
section_eq_cosection [in map]
section_eq_cosection [in map___]
section_eq_cosection [in map__]
section_eq_cosection [in map_]
section_surj [in map__]
section_surj [in map_]
section_surj [in map]
section_surj [in map___]
sieve_comp_prop [in sieve]
sieve_comp_prop [in sieve_]
sieve_extens [in sieve_]
sieve_extens [in sieve]
sieve_prop [in sieve]
sieve_prop [in sieve_]
sieve_set_prop [in sieve]
sieve_set_prop [in sieve_]
sieve_transport_trans [in sieve_]
sieve_transport_trans [in sieve]
T
target_extens [in target]
target_extens [in target_]
target_transport_trans [in target]
target_transport_trans [in target_]
top_coerence [in topology]
top_coerence [in topology_]
top_comp [in topology_]
top_comp [in topology]
top_larger [in topology]
top_larger [in topology_]
top_maximal [in topology_]
top_maximal [in topology]
top_transitivity [in topology_]
top_transitivity [in topology]
top_transport [in topology]
top_transport [in topology_]
top_trans_arrow [in topology_]
top_trans_arrow [in topology]
transport_eq [in misc_]
transport_eq [in misc__]
transport_eq [in misc]
transport_eq [in misc___]
transport_refl [in misc___]
transport_refl [in misc]
transport_refl [in misc_]
transport_refl [in misc__]
Z
zero_dx [in abmonoid_]
zero_dx [in abgroup_]
zero_dx [in abgroup]
zero_dx [in abmonoid]
zero_sx [in abgroup]
zero_sx [in cring]
zero_sx [in abmonoid]
zero_sx [in ring]
zero_sx [in ring_]
zero_sx [in abmonoid_]
zero_sx [in abgroup_]
zero_sx [in cring_]
Constructor Index
E
eq_mor_refl [in cat]
eq_mor_refl [in cat__]
eq_mor_refl [in cat___]
eq_mor_refl [in cat_]
J
JMeq_refl [in misc__]
JMeq_refl [in misc___]
JMeq_refl [in misc]
JMeq_refl [in misc_]
M
mor_over_intro [in cat_over]
mor_over_intro [in cat_over_]
N
non_empty_intro [in misc_]
non_empty_intro [in misc]
non_empty_intro [in misc___]
non_empty_intro [in misc__]
O
obj_over_intro [in cat_over_]
obj_over_intro [in cat_over]
P
prop_of_type_intro [in misc___]
prop_of_type_intro [in misc]
prop_of_type_intro [in misc_]
prop_of_type_intro [in misc__]
pullback_target_intro [in target_]
pullback_target_intro [in target]
S
set_of_intro [in misc_]
set_of_intro [in misc___]
set_of_intro [in misc__]
set_of_intro [in misc]
T
target_comp_intro [in target_]
target_comp_intro [in target]
target_of_mor_intro [in target]
target_of_mor_intro [in target_]
Inductive Index
E
eq_mor [in cat__]
eq_mor [in cat_]
eq_mor [in cat]
eq_mor [in cat___]
J
JMeq [in misc___]
JMeq [in misc__]
JMeq [in misc_]
JMeq [in misc]
M
mor_over [in cat_over_]
mor_over [in cat_over]
N
non_empty [in misc__]
non_empty [in misc]
non_empty [in misc___]
non_empty [in misc_]
O
obj_over [in cat_over_]
obj_over [in cat_over]
P
prop_of_type [in misc___]
prop_of_type [in misc__]
prop_of_type [in misc]
prop_of_type [in misc_]
pullback_target [in target]
pullback_target [in target_]
S
Set_Of [in misc_]
Set_Of [in misc__]
Set_Of [in misc___]
Set_Of [in misc]
T
target_comp [in target]
target_comp [in target_]
target_of_mor [in target]
target_of_mor [in target_]
Definition Index
A
A [in make_small_cat]
A [in make_small_cat_]
A [in make_small_cat__]
abgroup_of_cgroup [in abgroup]
abgroup_of_cgroup [in abgroup_]
abmonoid_of_abgroup [in abgroup_]
abmonoid_of_abgroup [in abgroup]
abmonoid_of_cmonoid [in abmonoid_]
abmonoid_of_cmonoid [in abmonoid]
amul [in algebra_]
amul [in algebra]
B
base [in cat_over_]
base [in cat_over]
base_change [in fibprod_]
base_change [in fibprod]
bijection_inverse [in map_]
bijection_inverse [in map__]
bijection_inverse [in map___]
bijection_inverse [in map]
C
cat [in yoneda_]
cat [in yoneda]
cat_over [in cat_over]
cat_over [in cat_over_]
cat_under [in cat_over_]
cat_under [in cat_over]
cgroup_of_abgroup [in abgroup]
cgroup_of_abgroup [in abgroup_]
class_eq_Q [in cmonoid_quot_]
class_eq_Q [in abmonoid_quot]
class_eq_Q [in cgroup_quot]
class_eq_Q [in abgroup_quot]
class_eq_Q [in cmonoid_quot]
class_eq_Q [in monoid_quot_]
class_eq_Q [in group_quot_]
class_eq_Q [in group_quot]
class_eq_Q [in abmonoid_quot_]
class_eq_Q [in abgroup_quot_]
class_eq_Q [in monoid_quot]
class_eq_Q [in cgroup_quot_]
cmonoid_of_abmonoid [in abmonoid]
cmonoid_of_abmonoid [in abmonoid_]
Compatible [in equiv_]
Compatible [in equiv]
Compatible2 [in quot]
Compatible2 [in quot_]
Compatible_Monoid [in abmonoid_quot]
Compatible_Monoid [in abmonoid_quot_]
Compatible_Monoid [in cmonoid_quot]
Compatible_Monoid [in monoid_quot_]
Compatible_Monoid [in monoid_quot]
Compatible_Monoid [in cmonoid_quot_]
cosection_comp [in map___]
cosection_comp [in map_]
cosection_comp [in map__]
cosection_comp [in map]
cosection_of_inverse [in map__]
cosection_of_inverse [in map_]
cosection_of_inverse [in map]
cosection_of_inverse [in map___]
Cov [in topology_]
cov [in topology]
Cov [in topology]
cov [in topology_]
D
Dual_Cat [in cat_]
Dual_Cat [in cat__]
Dual_Cat [in cat]
Dual_Cat [in cat___]
E
embedding [in cat__]
embedding [in cat___]
embedding [in cat_]
embedding [in cat]
eq_fct [in cat]
eq_fct [in cat__]
eq_fct [in cat___]
eq_fct [in cat_]
eq_presh [in presheaf]
eq_presh [in presheaf__]
eq_presh [in presheaf_]
F
fact2 [in quot]
fact2 [in quot_]
Fibprod [in fibprod]
Fibprod [in fibprod_]
final_isom [in universal]
final_isom [in universal_]
final_isom_inv [in universal_]
final_isom_inv [in universal]
final_of_zero [in universal]
final_of_zero [in universal_]
final_over [in cat_over]
final_over [in cat_over_]
Final_Theory [in universal]
Final_Theory [in universal_]
forget [in misc___]
forget [in misc__]
forget [in misc_]
forget [in misc]
G
group_of_cgroup [in cgroup]
group_of_cgroup [in cgroup_]
group_quot [in cgroup_quot]
group_quot [in cgroup_quot_]
group_quot [in group_quot]
group_quot [in abgroup_quot]
group_quot [in abgroup_quot_]
group_quot [in group_quot_]
H
h [in yoneda_]
h [in yoneda]
has_fibprod [in fibprod_]
has_fibprod [in fibprod]
has_product [in product]
has_product [in product_]
I
i [in yoneda]
i [in yoneda_]
ii_over [in cat_over_]
ii_over [in cat_over]
initial_isom [in universal]
initial_isom [in universal_]
initial_isom_inv [in universal]
initial_isom_inv [in universal_]
initial_of_zero [in universal_]
initial_of_zero [in universal]
Initial_Theory [in universal_]
Initial_Theory [in universal]
inverse_comp [in map___]
inverse_comp [in map_]
inverse_comp [in map__]
inverse_comp [in map]
inverse_inverse [in map__]
inverse_inverse [in map___]
inverse_inverse [in map_]
inverse_inverse [in map]
inverse_transport [in map__]
inverse_transport [in map]
inverse_transport [in map_]
inverse_transport [in map___]
inv_dx_of_inv [in universal_]
inv_dx_of_inv [in universal]
inv_i [in yoneda_]
inv_i [in yoneda]
inv_sx_of_inv [in universal]
inv_sx_of_inv [in universal_]
is_epi [in universal]
is_epi [in universal_]
is_injective [in map__]
is_injective [in map_]
is_injective [in map___]
is_injective [in map]
is_inv_dx [in universal]
is_inv_dx [in universal_]
is_inv_sx [in universal]
is_inv_sx [in universal_]
is_maximal_target [in target_]
is_maximal_target [in target]
is_mono [in universal_]
is_mono [in universal]
is_surjective [in map]
is_surjective [in map_]
is_surjective [in map___]
is_surjective [in map__]
J
j [in yoneda]
j [in yoneda_]
K
k [in yoneda]
k [in yoneda_]
M
make_inverse [in map_]
make_inverse [in map__]
make_inverse [in map]
make_inverse [in map___]
make_over [in cat_over_]
make_over [in cat_over]
make_under [in cat_over]
make_under [in cat_over_]
maximal_sieve [in sieve]
maximal_sieve [in sieve_]
monoid_of_cmonoid [in cmonoid]
monoid_of_cmonoid [in cmonoid_]
monoid_of_group [in group_]
monoid_of_group [in group]
monoid_quot [in cmonoid_quot]
monoid_quot [in cmonoid_quot_]
monoid_quot [in abmonoid_quot_]
monoid_quot [in monoid_quot_]
monoid_quot [in abmonoid_quot]
monoid_quot [in monoid_quot]
Morph [in cmonoid]
Morph [in module_]
Morph [in cgroup]
Morph [in presheaf__]
Morph [in functor_cat]
Morph [in cring_]
Morph [in functor_cat_]
Morph [in module]
Morph [in set_cat]
Morph [in cat__]
Morph [in monoid_]
Morph [in module_]
Morph [in cat]
Morph [in group_]
Morph [in abgroup_]
Morph [in presheaf_]
Morph [in cgroup_]
Morph [in ring_]
Morph [in abmonoid]
Morph [in abmonoid_]
Morph [in cat_]
Morph [in cmonoid_]
Morph [in module]
Morph [in monoid]
Morph [in set_cat_]
Morph [in abgroup]
Morph [in cring]
Morph [in presheaf]
Morph [in cat___]
Morph [in ring]
Morph [in group]
morph_comp [in group]
morph_comp [in cat__]
morph_comp [in cat___]
morph_comp [in abmonoid_]
morph_comp [in group_]
morph_comp [in cmonoid_]
morph_comp [in cat]
morph_comp [in abgroup_]
morph_comp [in algebra_]
morph_comp [in cmonoid]
morph_comp [in cring_]
morph_comp [in module]
morph_comp [in module_]
morph_comp [in ring]
morph_comp [in cat_]
morph_comp [in functor_cat_]
morph_comp [in cgroup]
morph_comp [in algebra]
morph_comp [in abmonoid]
morph_comp [in cgroup_]
morph_comp [in ring_]
morph_comp [in monoid_]
morph_comp [in module]
morph_comp [in functor_cat]
morph_comp [in set_cat_]
morph_comp [in module_]
morph_comp [in cring]
morph_comp [in abgroup]
morph_comp [in set_cat]
morph_comp [in monoid]
morph_comp_assoc [in functor_cat_]
morph_comp_assoc [in functor_cat]
morph_id [in group_]
morph_id [in abgroup_]
morph_id [in monoid]
morph_id [in ring_]
morph_id [in set_cat_]
morph_id [in cat___]
morph_id [in cat]
morph_id [in abgroup]
morph_id [in functor_cat]
morph_id [in cring_]
morph_id [in cmonoid_]
morph_id [in cring]
morph_id [in module]
morph_id [in cgroup]
morph_id [in ring]
morph_id [in cmonoid]
morph_id [in group]
morph_id [in module]
morph_id [in cat_]
morph_id [in module_]
morph_id [in abmonoid_]
morph_id [in abmonoid]
morph_id [in set_cat]
morph_id [in cgroup_]
morph_id [in functor_cat_]
morph_id [in cat__]
morph_id [in module_]
morph_id [in monoid_]
morph_id_dx [in functor_cat_]
morph_id_dx [in set_cat_]
morph_id_dx [in set_cat]
morph_id_dx [in functor_cat]
morph_id_sx [in functor_cat_]
morph_id_sx [in set_cat]
morph_id_sx [in set_cat_]
morph_id_sx [in functor_cat]
Morph_Theory [in algebra_]
Morph_Theory [in algebra]
mor_of_mor_over [in cat_over]
mor_of_mor_over [in cat_over_]
mor_of_obj_over [in cat_over]
mor_of_obj_over [in cat_over_]
N
NT'_Comm [in presheaf__]
NT'_Comm [in presheaf]
NT'_Comm [in presheaf_]
nt'_comp [in presheaf_]
nt'_comp [in presheaf]
nt'_comp [in presheaf__]
nt'_id [in presheaf__]
nt'_id [in presheaf_]
nt'_id [in presheaf]
NT_Comm [in nt__]
NT_Comm [in nt_]
NT_Comm [in nt]
nt_comp [in nt__]
nt_comp [in nt_]
nt_comp [in nt]
nt_h [in yoneda_]
nt_h [in yoneda]
nt_id [in nt]
nt_id [in nt__]
nt_id [in nt_]
O
Obj [in ring]
Obj [in module]
Obj [in cgroup]
Obj [in cgroup_]
Obj [in module]
Obj [in cmonoid]
Obj [in group]
Obj [in abmonoid_]
Obj [in cat_]
Obj [in set_cat_]
Obj [in monoid]
Obj [in set_cat]
Obj [in cat]
Obj [in abgroup_]
Obj [in cmonoid_]
Obj [in abgroup]
Obj [in cring]
Obj [in functor_cat]
Obj [in ring_]
Obj [in functor_cat_]
Obj [in cat___]
Obj [in module_]
Obj [in monoid_]
Obj [in module_]
Obj [in abmonoid]
Obj [in group_]
Obj [in cring_]
Obj [in cat__]
obj_of_obj_over [in cat_over]
obj_of_obj_over [in cat_over_]
oo_over [in cat_over]
oo_over [in cat_over_]
P
Presheaf_Cat [in presheaf__]
Presheaf_Cat [in presheaf_]
Presheaf_Cat [in presheaf]
product_assoc [in product]
product_assoc [in product_]
product_assoc_inv [in product]
product_assoc_inv [in product_]
product_comm [in product_]
product_comm [in product]
product_comm_inv [in product]
product_comm_inv [in product_]
product_isom [in product_]
product_isom [in product]
product_isom_inv [in product_]
product_isom_inv [in product]
pullback [in fibprod]
pullback [in fibprod_]
pullback_mor [in fibprod_]
pullback_mor [in fibprod]
Q
quot_fix_universe [in quot_]
quot_fix_universe [in quot]
quot_law [in quot]
quot_law [in quot_]
quot_law2 [in quot]
quot_law2 [in quot_]
R
R [in small_ring]
R [in small_ring_]
S
section_comp [in map__]
section_comp [in map]
section_comp [in map___]
section_comp [in map_]
section_of_inverse [in map]
section_of_inverse [in map_]
section_of_inverse [in map__]
section_of_inverse [in map___]
set [in yoneda_]
set [in yoneda]
sieve_comp [in sieve_]
sieve_comp [in sieve]
Sieve_Theory [in sieve]
Sieve_Theory [in sieve_]
sieve_transport [in sieve_]
sieve_transport [in sieve]
src [in cat__]
src [in cat_]
src [in cat]
src [in cat___]
T
Target [in target]
Target [in target_]
target_sub [in target_]
target_sub [in target]
target_transport [in target]
target_transport [in target_]
transport [in misc___]
transport [in misc__]
transport [in misc_]
transport [in misc]
trg [in cat]
trg [in cat___]
trg [in cat__]
trg [in cat_]
TypeQ [in quot]
TypeQ [in quot_]
type_of [in misc__]
type_of [in misc___]
type_of [in misc]
type_of [in misc_]
Y
yoneda [in yoneda]
yoneda [in yoneda_]
yoneda_bij [in yoneda]
yoneda_bij [in yoneda_]
yoneda_bij_inv [in yoneda_]
yoneda_bij_inv [in yoneda]
yoneda_data [in yoneda_]
yoneda_data [in yoneda]
yoneda_embedding [in yoneda]
yoneda_embedding [in yoneda_]
Module Index
A
abgroup
abgroup_
abgroup_quot
abgroup_quot_
abmonoid
abmonoid_
abmonoid_quot
abmonoid_quot_
algebra
algebra_
C
cat
cat_
cat_over
cat_over_
cat_sig
cat_sig_
cat_sig__
cat_sig___
cat__
cat___
cgroup
cgroup_
cgroup_quot
cgroup_quot_
cmonoid
cmonoid_
cmonoid_quot
cmonoid_quot_
cool
cring
cring_
E
equiv
equiv_
F
fibprod
fibprod_
functor_cat
functor_cat_
G
group
group_
group_quot
group_quot_
M
make_small_cat
make_small_cat_
make_small_cat__
map
map_
map__
map___
misc
misc_
misc__
misc___
module
module_
monoid
monoid_
monoid_quot
monoid_quot_
N
nt
nt_
nt__
P
presheaf
presheaf_
presheaf__
product
product_
Q
quot
quot_
R
ring
ring_
S
set_cat
set_cat_
sieve
sieve_
small_group
small_group_
small_monoid
small_monoid_
small_ring
small_ring_
T
target
target_
topology
topology_
U
universal
universal_
Y
yoneda
yoneda_
| 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 |
_ |
(1140 entries) |
| Tactic 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 |
_ |
(3 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 |
_ |
(47 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 |
_ |
(526 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 |
_ |
(30 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 |
_ |
(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 |
_ |
(416 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 |
_ |
(88 entries) |
This page has been generated by coqdoc