| 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 | (1579 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 | (2 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 | (1 entry) |
| 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 | (642 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 | (13 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 | (3 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 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 | (1 entry) |
| 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 | (884 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (9 entries) |
Global Index
A
abgr [definition, in algebra1]abgrconstr [definition, in algebra1]
abgrdirprod [definition, in algebra1]
abgrfrac [definition, in algebra1]
abgrfraccarrier [definition, in algebra1]
abgrfracinv [definition, in algebra1]
abgrfracinvcomp [lemma, in algebra1]
abgrfracinvint [definition, in algebra1]
abgrfracisinv [lemma, in algebra1]
abgrhz [definition, in hz]
abgrpair [definition, in algebra1]
abgrquot [definition, in algebra1]
abgrtoabmonoid [definition, in algebra1]
abgrtogr [definition, in algebra1]
abmonoid [definition, in algebra1]
abmonoidconstr [definition, in algebra1]
abmonoiddirprod [definition, in algebra1]
abmonoidfrac [definition, in algebra1]
abmonoidfracop [definition, in algebra1]
abmonoidfracopint [definition, in algebra1]
abmonoidoprer [lemma, in algebra1]
abmonoidpair [definition, in algebra1]
abmonoidquot [definition, in algebra1]
abmonoidtomonoid [definition, in algebra1]
absvalhz [definition, in hz]
absvalhzint [definition, in hz]
absvalhzintcomp [lemma, in hz]
addabgr [definition, in algebra1]
addabgreqrel [definition, in algebra1]
addabmonoidnat [definition, in hnat]
addsubgr [definition, in algebra1]
adjev [definition, in uu0]
adjev2 [definition, in uu0]
algebra1 [library]
assocax [definition, in algebra1]
assocax_is [definition, in algebra1]
B
bandfmap [definition, in uu0]bhfiber [definition, in uu0]
binop [definition, in algebra1]
binopeqrel [definition, in algebra1]
binopeqrelabgrfrac [definition, in algebra1]
binopeqrelabmonoidfrac [definition, in algebra1]
binopeqrelpair [definition, in algebra1]
binopfun [definition, in algebra1]
binopfuncomp [definition, in algebra1]
binopfunpair [definition, in algebra1]
binophrel [definition, in algebra1]
binophrelpair [definition, in algebra1]
binopincltobinopfun [definition, in algebra1]
binopiso [definition, in algebra1]
binopisocomp [definition, in algebra1]
binopisopair [definition, in algebra1]
binopisotobinopmono [definition, in algebra1]
binopmono [definition, in algebra1]
binopmonocomp [definition, in algebra1]
binopmonopair [definition, in algebra1]
binoppo [definition, in algebra1]
binoppopair [definition, in algebra1]
binop1fun [definition, in algebra1]
binop1iso [definition, in algebra1]
binop1mono [definition, in algebra1]
binop2fun [definition, in algebra1]
binop2iso [definition, in algebra1]
binop2mono [definition, in algebra1]
boolascoprod [definition, in uu0]
boolchoice [definition, in uu0]
booleq [definition, in uu0]
booleq [definition, in hz]
boolset [definition, in hSet]
boolsumfun [definition, in uu0]
boolsumtocoprod [definition, in uu0]
C
carrier [definition, in hSet]carrierofasubabgr [definition, in algebra1]
carrierofasubcommrng [definition, in algebra1]
carrierofasubgr [definition, in algebra1]
carrierofasubrng [definition, in algebra1]
carrierofasubsetwithbinop [definition, in algebra1]
carrierofpo [definition, in hSet]
carrierofposet [definition, in hSet]
carrierofposetmorphism [definition, in hSet]
carrierofsubabmonoid [definition, in algebra1]
carrierofsubmonoid [definition, in algebra1]
carrierofsubsetwith2binop [definition, in algebra1]
carrierpair [definition, in hSet]
centralfiber [lemma, in uu0]
coconusf [definition, in uu0]
coconusfromt [definition, in uu0]
coconusfromtpair [definition, in uu0]
coconusfromtpr21 [definition, in uu0]
coconustot [definition, in uu0]
coconustotpair [definition, in uu0]
coconustotpr21 [definition, in uu0]
commax [definition, in algebra1]
commax_is [definition, in algebra1]
commhfp [definition, in uu0]
commrng [definition, in algebra1]
commrngconstr [definition, in algebra1]
commrngdirprod [definition, in algebra1]
commrngfrac [definition, in algebra1]
commrngfracinv1 [definition, in algebra1]
commrngfracinv1comp [lemma, in algebra1]
commrngfracinv1int [definition, in algebra1]
commrngfracisinv1 [lemma, in algebra1]
commrngfracl1 [lemma, in algebra1]
commrngfracl2 [lemma, in algebra1]
commrngfracl3 [lemma, in algebra1]
commrngfracl4 [definition, in algebra1]
commrngfracl4l [lemma, in algebra1]
commrngfracl4r [lemma, in algebra1]
commrngfracl5 [lemma, in algebra1]
commrngfracl6 [lemma, in algebra1]
commrngfracl7l [lemma, in algebra1]
commrngfracl7r [lemma, in algebra1]
commrngfracop1 [definition, in algebra1]
commrngfracop1comp [lemma, in algebra1]
commrngfracop1int [definition, in algebra1]
commrngfracop2 [definition, in algebra1]
commrngfracop2int [definition, in algebra1]
commrngfracunel1 [definition, in algebra1]
commrngfracunel1int [definition, in algebra1]
commrngfracunel2 [definition, in algebra1]
commrngfracunel2int [definition, in algebra1]
commrngop2axs [definition, in algebra1]
commrngpair [definition, in algebra1]
commrngquot [definition, in algebra1]
commrngtorng [definition, in algebra1]
commsqstr [definition, in uu0]
commsqstrtocomplxstr [lemma, in uu0]
commsqZtohfp [definition, in uu0]
commsqZtohfphomot [definition, in uu0]
commsqZtohfphomot' [definition, in uu0]
compevmap [definition, in hSet]
compfun [definition, in hSet]
compfunpair [definition, in hSet]
compl [definition, in uu0]
complpair [definition, in uu0]
complxstr [definition, in uu0]
complxstrtocommsqstr [lemma, in uu0]
connectedcoconusfromt [lemma, in uu0]
connectedcoconustot [lemma, in uu0]
constr1 [definition, in uu0]
constr2 [lemma, in uu0]
coprod [abbreviation, in uuu]
coprodasstol [definition, in uu0]
coprodasstor [definition, in uu0]
coprodcomm [definition, in uu0]
coprodf [definition, in uu0]
coprodofhfiberstohfiber [lemma, in uu0]
coprodtobool [definition, in uu0]
coprodtoboolsum [definition, in uu0]
curry [definition, in uu0]
cutonweq [definition, in uu0]
D
ddualand [definition, in uu0]deltap [definition, in uu0]
di [definition, in hnat]
diaglemma2 [lemma, in uu0]
dirprod [definition, in uu0]
dirprodadj [definition, in uu0]
dirprodf [definition, in uu0]
dirprodpair [definition, in uu0]
dirprodtosetquot [definition, in hSet]
disjointl1 [lemma, in uu0]
distraxs_is [definition, in algebra1]
dneg [definition, in uu0]
dneganddnegimpldneg [definition, in uu0]
dneganddnegl1 [lemma, in uu0]
dnegf [definition, in uu0]
dnegnegtoneg [definition, in uu0]
dni [definition, in stnfsets]
dnicommsq [lemma, in stnfsets]
dnihfsq [lemma, in stnfsets]
dnitocompl [definition, in stnfsets]
d1 [definition, in uu0]
d1g [definition, in uu0]
d2 [definition, in uu0]
d2g [definition, in uu0]
d3g [definition, in uu0]
E
empty [abbreviation, in uuu]eqax0 [definition, in hSet]
eqax1 [definition, in hSet]
eqax2 [definition, in hSet]
eqbhz [definition, in hz]
eqbnat [definition, in hnat]
eqbx [definition, in uu0]
eqfromdnegeq [lemma, in uu0]
eqh [definition, in hnat]
eqhtopaths [definition, in hnat]
eqhz [definition, in hz]
eqnat [definition, in hnat]
eqrel [definition, in hSet]
eqrelabgrfrac [definition, in algebra1]
eqrelabmonoidfrac [definition, in algebra1]
eqrelcommrngfrac [definition, in algebra1]
eqrelconstr [definition, in hSet]
eqreldirprod [definition, in hSet]
eqrelpair [definition, in hSet]
eqrelrefl [definition, in hSet]
eqrelsymm [definition, in hSet]
eqreltrans [definition, in hSet]
eqset [definition, in hSet]
eqweqmaphProp [definition, in hProp]
etacor [definition, in uu0]
etacoronpaths [lemma, in uu0]
etacorrection [axiom, in uu0]
etacorrectiononpaths [lemma, in uu0]
ezmap [definition, in uu0]
ezmaphf [definition, in uu0]
ezmappr21 [definition, in uu0]
ezmap1 [definition, in uu0]
ezweq [definition, in uu0]
ezweqg [definition, in uu0]
ezweqhf [definition, in uu0]
ezweqpr21 [definition, in uu0]
ezweq1 [definition, in uu0]
ezweq1g [definition, in uu0]
ezweq1pr21 [definition, in uu0]
ezweq2 [definition, in uu0]
ezweq2g [definition, in uu0]
ezweq3g [definition, in uu0]
F
factorial [definition, in hnat]falsetonegtrue [definition, in uu0]
ffgg [definition, in uu0]
fibseqg [definition, in uu0]
fibseqhf [definition, in uu0]
fibseqpr21 [definition, in uu0]
fibseqstr [definition, in uu0]
fibseqstrpair [definition, in uu0]
fibseqstrtocomplxstr [definition, in uu0]
fibseqstrtohfsqstr [lemma, in uu0]
fibseq1 [definition, in uu0]
fibseq1g [definition, in uu0]
fibseq2 [definition, in uu0]
fibseq2g [definition, in uu0]
fibseq3g [definition, in uu0]
fincard [definition, in finitesets]
finitesets [library]
finstruct [definition, in finitesets]
finstructonbool [definition, in finitesets]
finstructoncompl [definition, in finitesets]
finstructoncontr [definition, in finitesets]
finstructoncoprod [definition, in finitesets]
finstructoncoprodwithunit [definition, in finitesets]
finstructondecsubset [definition, in finitesets]
finstructondirprod [definition, in finitesets]
finstructonempty [definition, in finitesets]
finstructonempty2 [definition, in finitesets]
finstructonforall [definition, in finitesets]
finstructonfun [definition, in finitesets]
finstructonstn [definition, in finitesets]
finstructontotal2 [definition, in finitesets]
finstructonunit [definition, in finitesets]
finstructonweq [definition, in finitesets]
finstructweqb [definition, in finitesets]
finstructweqf [definition, in finitesets]
fintructpair [definition, in finitesets]
foralltohfiber [definition, in uu0]
foralltototal [definition, in uu0]
foralltototaltoforall [definition, in uu0]
fpmap [definition, in uu0]
fromcoconusf [definition, in uu0]
fromcompltodisjoint [definition, in uu0]
fromcompltoii1x [definition, in uu0]
fromcompltoii2y [definition, in uu0]
fromdsubtypesdirprodcarrier [definition, in hSet]
fromempty [definition, in uu0]
fromtotal2overcoprod [definition, in uu0]
fromtotal2overunit [definition, in uu0]
funcomp [definition, in uu0]
funcontr [lemma, in uu0]
funcontrtwice [lemma, in uu0]
functtransportf [lemma, in uu0]
funextempty [axiom, in uu0]
funextfun [definition, in uu0]
funextfunax [axiom, in uu0]
funextsec [definition, in uu0]
funextweql1 [lemma, in uu0]
funfromcoprodtoprod [definition, in uu0]
funtoprodtoprod [definition, in uu0]
funtranspos [definition, in uu0]
funtranspos0 [definition, in uu0]
G
geh [definition, in hnat]gehdinn [lemma, in hnat]
gehgthtrans [lemma, in hnat]
gehpo [definition, in hnat]
gehsnimplgth [lemma, in hnat]
gehtrans [lemma, in hnat]
gr [definition, in algebra1]
gradth [lemma, in uu0]
grconstr [definition, in algebra1]
grdirprod [definition, in algebra1]
grinv [definition, in algebra1]
grinv_is [definition, in algebra1]
grlinvax [definition, in algebra1]
grlinvax_is [definition, in algebra1]
grpair [definition, in algebra1]
grquot [definition, in algebra1]
grquotinvcomp [lemma, in algebra1]
grrinvax [definition, in algebra1]
grrinvax_is [definition, in algebra1]
grtomonoid [definition, in algebra1]
gth [definition, in hnat]
gthandplusl [lemma, in hnat]
gthandpluslinv [lemma, in hnat]
gthandplusr [lemma, in hnat]
gthandplusrinv [lemma, in hnat]
gthasymm [lemma, in hnat]
gthchoice [lemma, in hnat]
gthgehtrans [lemma, in hnat]
gthimplgeh [lemma, in hnat]
gthimplgehsn [lemma, in hnat]
gthimplgths [lemma, in hnat]
gthsnn [lemma, in hnat]
gthtrans [lemma, in hnat]
H
hconj [definition, in hProp]hconjtohdisj [lemma, in hProp]
hdisj [definition, in hProp]
hexists [definition, in hProp]
hfalse [definition, in hProp]
hffpmap2 [definition, in uu0]
hfiber [definition, in uu0]
hfiberfpmap [definition, in uu0]
hfiberpair [definition, in uu0]
hfiberpr21 [definition, in uu0]
hfibersftogf [definition, in uu0]
hfibersgftog [definition, in uu0]
hfibersgtof' [definition, in uu0]
hfibersg'tof [definition, in uu0]
hfibershomotftog [lemma, in uu0]
hfibershomotgtof [lemma, in uu0]
hfibertocoprodofhfibers [lemma, in uu0]
hfibertoforall [definition, in uu0]
hfibertohfp [definition, in uu0]
hfibertosec [definition, in uu0]
hfibertriangle1 [lemma, in uu0]
hfibertriangle1inv0 [lemma, in uu0]
hfibertriangle2 [lemma, in uu0]
hforall [definition, in hProp]
hfp [definition, in uu0]
hfpg [definition, in uu0]
hfpg' [definition, in uu0]
hfpoverX [definition, in uu0]
hfpoverX' [definition, in uu0]
hfptohfiber [definition, in uu0]
hfsqstr [definition, in uu0]
hfsqstrpair [definition, in uu0]
hfsqstrtocommsqstr [definition, in uu0]
hfsqstrtofibseqstr [lemma, in uu0]
himpl [definition, in hProp]
hinhand [definition, in hProp]
hinhcoprod [lemma, in hProp]
hinhfun [definition, in hProp]
hinhfun2 [definition, in hProp]
hinhimplinhdneg [definition, in hProp]
hinhpr [definition, in hProp]
hinhprinv [abbreviation, in hProp]
hinhuniv [definition, in hProp]
hinhunivcor1 [definition, in hProp]
hinhuniv2 [definition, in hProp]
hlevelntosn [lemma, in uu0]
hlevelretract [lemma, in uu0]
hnat [library]
hneg [definition, in hProp]
homot [definition, in uu0]
homotcoprodfcomp [definition, in uu0]
homotcoprodfhomot [definition, in uu0]
homotd3g [lemma, in uu0]
homotffggid [definition, in uu0]
homotfuntranspos2 [lemma, in uu0]
homotinvweqweq [definition, in uu0]
homotinvweqweq0 [definition, in uu0]
homotrecomplfcomp [definition, in uu0]
homotrecomplfhomot [definition, in uu0]
homotrecomplfidfun [definition, in uu0]
homotrecomplnat [lemma, in uu0]
homottranspost2t1t1t2 [definition, in uu0]
homottranspos0t2t1t1t2 [definition, in uu0]
homotweqinvweq [definition, in uu0]
homotweqinvweqweq [definition, in uu0]
homotweqoncomplcomp [definition, in uu0]
hProp [definition, in hProp]
hProp [library]
hProppair [definition, in hProp]
hProppr21 [definition, in hProp]
hrel [definition, in hSet]
hrelabgrfrac [definition, in algebra1]
hrelabgrfrac' [definition, in algebra1]
hrelabmonoidfrac [definition, in algebra1]
hrelabmonoidfrac_l [lemma, in algebra1]
hrelcommrngfrac0 [definition, in algebra1]
hreldirprod [definition, in hSet]
hrel0abmonoidfrac [definition, in algebra1]
hSet [definition, in hSet]
hSet [library]
hSetpair [definition, in hSet]
hsubtypes [definition, in hSet]
htrue [definition, in hProp]
hz [definition, in hz]
hz [library]
hzminus [definition, in hz]
hzplus [definition, in hz]
hzplusassoc [lemma, in hz]
hzpluscomm [lemma, in hz]
hzplusl0 [lemma, in hz]
hzplusr0 [lemma, in hz]
hzsign [definition, in hz]
hzzero [definition, in hz]
I
idfun [definition, in uu0]idisweq [lemma, in uu0]
idpath [abbreviation, in uuu]
idweq [definition, in uu0]
ifcontrthenunitl0 [lemma, in uu0]
ii1 [abbreviation, in uuu]
ii1fun [abbreviation, in uuu]
ii2 [abbreviation, in uuu]
ii2fun [abbreviation, in uuu]
image [definition, in hSet]
imagepair [definition, in hSet]
impred [lemma, in uu0]
impredfun [lemma, in uu0]
impredtech1 [lemma, in uu0]
impredtwice [lemma, in uu0]
incl [definition, in uu0]
inclcomp [definition, in algebra1]
inclcomp [definition, in uu0]
inclpair [definition, in uu0]
inhdnegand [definition, in hProp]
inhdnegfun [definition, in hProp]
inhdnegpr [definition, in hProp]
inhdneguniv [definition, in hProp]
invbinopiso [definition, in algebra1]
invcutonweq [definition, in uu0]
invertibilityinabmonoidfrac [lemma, in algebra1]
invertibilityincommrngfrac [lemma, in algebra1]
invezmaphf [definition, in uu0]
invezmappr21 [definition, in uu0]
invezmap1 [definition, in uu0]
invimpl [definition, in uu0]
invinv [lemma, in uu0]
invmap [definition, in uu0]
invmaponpathsincl [definition, in uu0]
invmaponpathsS [lemma, in hnat]
invmaponpathsweq [definition, in uu0]
invmaponpathsweqid [definition, in uu0]
invmonoidiso [definition, in algebra1]
invongrquot [definition, in algebra1]
invproofirrelevance [lemma, in uu0]
invrecompl [definition, in uu0]
invstruct [definition, in algebra1]
invtwobinopiso [definition, in algebra1]
invweq [definition, in uu0]
isabgrcarrier [lemma, in algebra1]
isabgrdirprod [lemma, in algebra1]
isabgroupop [definition, in algebra1]
isabgroupopisob [definition, in algebra1]
isabgroupopisof [definition, in algebra1]
isabgroupoptoisabmonoidop [definition, in algebra1]
isabgrquot [lemma, in algebra1]
isabmonoidcarrier [lemma, in algebra1]
isabmonoiddirprod [lemma, in algebra1]
isabmonoidop [definition, in algebra1]
isabmonoidopisob [definition, in algebra1]
isabmonoidopisof [definition, in algebra1]
isabmonoidquot [lemma, in algebra1]
isaninvprop [definition, in uu0]
isaninvpropneg [lemma, in uu0]
isaninv1 [lemma, in uu0]
isaposetmorphism [definition, in hSet]
isaprop [definition, in uu0]
isapropaninvprop [lemma, in uu0]
isapropdec [lemma, in uu0]
isapropdneg [lemma, in uu0]
isapropempty [lemma, in uu0]
isapropempty2 [lemma, in uu0]
isapropifcontr [lemma, in uu0]
isapropifnegtrue [lemma, in uu0]
isapropimeqclass [lemma, in hSet]
isapropimpl [lemma, in uu0]
isapropinclb [definition, in uu0]
isapropinvstruct [lemma, in algebra1]
isapropisabgroupop [lemma, in algebra1]
isapropisabmonoidop [lemma, in algebra1]
isapropisaprop [lemma, in uu0]
isapropisaset [lemma, in uu0]
isapropisassoc [lemma, in algebra1]
isapropisbinopfun [lemma, in algebra1]
isapropisbinophrel [lemma, in algebra1]
isapropischoicebase [lemma, in hSet]
isapropiscomm [lemma, in algebra1]
isapropiscommrng [lemma, in algebra1]
isapropiscontr [lemma, in uu0]
isapropisdeceq [lemma, in uu0]
isapropisdecprop [definition, in uu0]
isapropisdistr [lemma, in algebra1]
isapropiseqclass [lemma, in hSet]
isapropisgroupop [lemma, in algebra1]
isapropishinh [lemma, in hProp]
isapropisincl [definition, in uu0]
isapropisinv [lemma, in algebra1]
isapropisisolated [lemma, in uu0]
isapropisldistr [lemma, in algebra1]
isapropislinv [lemma, in algebra1]
isapropislunit [lemma, in algebra1]
isapropismonoidfun [lemma, in algebra1]
isapropismonoidop [lemma, in algebra1]
isapropisofhlevel [lemma, in uu0]
isapropisofhlevelf [lemma, in uu0]
isapropisrdistr [lemma, in algebra1]
isapropisrinv [lemma, in algebra1]
isapropisrngops [lemma, in algebra1]
isapropisrunit [lemma, in algebra1]
isapropissubgr [lemma, in algebra1]
isapropissubmonoid [lemma, in algebra1]
isapropissubrng [lemma, in algebra1]
isapropissubsetwithbinop [lemma, in algebra1]
isapropissubsetwith2binop [lemma, in algebra1]
isapropissurjective [lemma, in hSet]
isapropistwobinopfun [lemma, in algebra1]
isapropisunital [lemma, in algebra1]
isapropisweq [lemma, in uu0]
isapropis2binophrel [lemma, in algebra1]
isaprople [lemma, in hnat]
isapropneg [lemma, in uu0]
isapropneg2 [lemma, in uu0]
isaproppathsfromisolated [lemma, in uu0]
isaproppathstoisolated [lemma, in uu0]
isapropsubtype [lemma, in hSet]
isapropunit [abbreviation, in uu0]
isapropweqfromcontr [lemma, in uu0]
isapropweqfromempty [lemma, in uu0]
isapropweqfromempty2 [lemma, in uu0]
isapropweqfromprop [lemma, in uu0]
isapropweqfromunit [lemma, in uu0]
isapropweqtocontr [lemma, in uu0]
isapropweqtoempty [lemma, in uu0]
isapropweqtoempty2 [lemma, in uu0]
isapropweqtoprop [lemma, in uu0]
isapropweqtounit [lemma, in uu0]
isaset [definition, in uu0]
isasetbinopfun [lemma, in algebra1]
isasetbool [lemma, in uu0]
isasetcoprod [lemma, in uu0]
isasetdirprod [lemma, in uu0]
isasetempty [lemma, in uu0]
isasethProp [lemma, in hProp]
isasethsubtypes [lemma, in hSet]
isasethz [lemma, in hz]
isasetifdeceq [lemma, in uu0]
isasetifiscontrloops [lemma, in uu0]
isasetmonoidfun [lemma, in algebra1]
isasetnat [lemma, in hnat]
isasetsetquot [lemma, in hSet]
isasetsetquot2 [lemma, in hSet]
isasetstn [lemma, in stnfsets]
isasetsubset [lemma, in uu0]
isasettwobinopfun [lemma, in algebra1]
isasetunit [lemma, in uu0]
isasetweqfromset [lemma, in uu0]
isasetweqtoset [lemma, in uu0]
isassoc [definition, in algebra1]
isassocdirprod [lemma, in algebra1]
isassocisob [abbreviation, in algebra1]
isassocisof [lemma, in algebra1]
isassocmonob [lemma, in algebra1]
isassocquot [lemma, in algebra1]
isbinopfun [definition, in algebra1]
isbinopfuncomp [lemma, in algebra1]
isbinopfuninvmap [lemma, in algebra1]
isbinophrel [definition, in algebra1]
isbinophrelabgrfrac [lemma, in algebra1]
isbinophrelabmonoidfrac [lemma, in algebra1]
isbinoptransrel [lemma, in algebra1]
iscancellable [definition, in algebra1]
iscancellableisob [abbreviation, in algebra1]
iscancellablemonob [lemma, in algebra1]
ischoicebase [definition, in hSet]
ischoicebasecontr [lemma, in hSet]
ischoicebasecoprod [lemma, in hSet]
ischoicebaseempty [lemma, in hSet]
ischoicebaseempty2 [lemma, in hSet]
ischoicebasefiniteset [lemma, in finitesets]
ischoicebasestn [lemma, in stnfsets]
ischoicebaseunit [lemma, in hSet]
ischoicebaseweqb [lemma, in hSet]
ischoicebaseweqf [lemma, in hSet]
ischoicebase_uu1 [definition, in hSet]
iscomm [definition, in algebra1]
iscommisob [abbreviation, in algebra1]
iscommisof [lemma, in algebra1]
iscommmonob [lemma, in algebra1]
iscommop2_is [definition, in algebra1]
iscommrng [definition, in algebra1]
iscommrngcarrier [lemma, in algebra1]
iscommrngdirprod [lemma, in algebra1]
iscommrngops [definition, in algebra1]
iscommrngopsisob [definition, in algebra1]
iscommrngopsisof [definition, in algebra1]
iscommrngquot [lemma, in algebra1]
iscomprelfun [definition, in hSet]
iscomprelfun2 [definition, in hSet]
iscomprelrelfun [definition, in hSet]
iscomprelrelfun2 [definition, in hSet]
iscompsetquotpr [lemma, in hSet]
iscompsetquot2pr [lemma, in hSet]
iscontr [definition, in uu0]
iscontraprop1 [lemma, in uu0]
iscontraprop1inv [lemma, in uu0]
iscontrcoconusfromt [lemma, in uu0]
iscontrcoconustot [lemma, in uu0]
iscontrfunfromempty [lemma, in uu0]
iscontrfunfromempty2 [lemma, in uu0]
iscontrfuntocontr [lemma, in uu0]
iscontrfuntounit [lemma, in uu0]
iscontrhfiberdi [lemma, in hnat]
iscontrhfiberdni [lemma, in stnfsets]
iscontrhfibereqbx [lemma, in uu0]
iscontrhfiberii1x [lemma, in uu0]
iscontrhfiberii2y [lemma, in uu0]
iscontrhfiberl1 [lemma, in uu0]
iscontrhfiberl2 [lemma, in uu0]
iscontrhfiberofincl [lemma, in uu0]
iscontrhfiberplusn [lemma, in hnat]
iscontrhfiberstntonat [lemma, in stnfsets]
iscontrifweqtounit [lemma, in uu0]
iscontriscontr [lemma, in uu0]
iscontrloopsifisaset [lemma, in uu0]
iscontrpair [definition, in uu0]
iscontrpathsinunit [lemma, in uu0]
iscontrpr21 [definition, in uu0]
iscontrretract [lemma, in uu0]
iscontrsecoverempty [definition, in uu0]
iscontrsecoverempty2 [definition, in uu0]
iscontrstn1 [lemma, in stnfsets]
iscontrunit [lemma, in uu0]
iscontrweqb [lemma, in uu0]
iscontrweqf [lemma, in uu0]
iscoproj [definition, in uu0]
iscoprojfromisdecincl [lemma, in uu0]
isdeceq [definition, in uu0]
isdeceqabgrfrac [lemma, in algebra1]
isdeceqabmonoidfrac [lemma, in algebra1]
isdeceqbool [lemma, in uu0]
isdeceqcommrngfrac [lemma, in algebra1]
isdeceqhz [lemma, in hz]
isdeceqif [lemma, in uu0]
isdeceqifisaprop [lemma, in uu0]
isdeceqinclb [lemma, in uu0]
isdeceqnat [lemma, in hnat]
isdeceqsetquot [definition, in hSet]
isdeceqsetquot_non_constr [lemma, in hSet]
isdeceqstn [lemma, in stnfsets]
isdeceqweqb [lemma, in uu0]
isdeceqweqf [lemma, in uu0]
isdecincl [definition, in uu0]
isdecinclcomp [lemma, in uu0]
isdecincldi [lemma, in hnat]
isdecincldni [lemma, in stnfsets]
isdecinclf [lemma, in uu0]
isdecinclfromiscoproj [lemma, in uu0]
isdecinclfromisweq [lemma, in uu0]
isdecinclg [lemma, in uu0]
isdecinclhomot [lemma, in uu0]
isdecinclii1 [lemma, in uu0]
isdecinclii2 [lemma, in uu0]
isdecinclplusn [lemma, in hnat]
isdecinclpr21 [lemma, in uu0]
isdecinclS [lemma, in hnat]
isdecinclstntonat [lemma, in stnfsets]
isdecincltoisincl [lemma, in uu0]
isdecprop [definition, in uu0]
isdecpropdirprod [lemma, in uu0]
isdecpropempty [lemma, in uu0]
isdecpropeqh [lemma, in hnat]
isdecpropfibseq0 [lemma, in uu0]
isdecpropfibseq1 [lemma, in uu0]
isdecpropfromdecincl [lemma, in uu0]
isdecpropfromiscontr [lemma, in uu0]
isdecpropfromneg [lemma, in uu0]
isdecpropgth [lemma, in hnat]
isdecpropif [lemma, in uu0]
isdecprople [lemma, in hnat]
isdecpropleh [lemma, in hnat]
isdecproppaths [lemma, in uu0]
isdecproppathsfromisolated [lemma, in uu0]
isdecproppathstoisolated [lemma, in uu0]
isdecproptoisaprop [lemma, in uu0]
isdecpropweqb [lemma, in uu0]
isdecpropweqf [lemma, in uu0]
isdistr [definition, in algebra1]
isdistrisob [abbreviation, in algebra1]
isdistrisof [lemma, in algebra1]
isdistrmonob [definition, in algebra1]
iseqclass [definition, in hSet]
iseqclassconstr [definition, in hSet]
iseqclassdirprod [lemma, in hSet]
iseqrel [definition, in hSet]
iseqrelabgrfrac [lemma, in algebra1]
iseqrelabmonoidfrac [lemma, in algebra1]
iseqrelconstr [definition, in hSet]
isfibseq [definition, in uu0]
isfibseqg [lemma, in uu0]
isfibseqpr21 [lemma, in uu0]
isfinite [definition, in finitesets]
isfinitebool [definition, in finitesets]
isfinitecompl [definition, in finitesets]
isfinitecontr [definition, in finitesets]
isfinitecoprod [definition, in finitesets]
isfinitecoprodwithunit [definition, in finitesets]
isfinitedecsubset [definition, in finitesets]
isfinitedirprod [definition, in finitesets]
isfiniteempty [definition, in finitesets]
isfiniteempty2 [definition, in finitesets]
isfiniteforall [definition, in finitesets]
isfinitefun [definition, in finitesets]
isfinitestn [definition, in finitesets]
isfinitetotal2 [definition, in finitesets]
isfiniteunit [definition, in finitesets]
isfiniteweq [definition, in finitesets]
isfiniteweqb [definition, in finitesets]
isfiniteweqf [definition, in finitesets]
isgrcarrier [definition, in algebra1]
isgrdirprod [lemma, in algebra1]
isgroupop [definition, in algebra1]
isgroupopif [lemma, in algebra1]
isgroupopisob [definition, in algebra1]
isgroupopisof [definition, in algebra1]
isgroupoppair [definition, in algebra1]
isgrquot [definition, in algebra1]
ishfsq [definition, in uu0]
ishfsqweqhfibersgtof' [lemma, in uu0]
ishfsqweqhfibersg'tof [lemma, in uu0]
ishinh [definition, in hProp]
ishinhsubtypesdirprod [lemma, in hSet]
ishinh_UU [definition, in hProp]
ishomotinclrecomplf [lemma, in uu0]
isincl [definition, in uu0]
isinclbetweensets [lemma, in uu0]
isinclcomp [lemma, in algebra1]
isinclcomp [lemma, in uu0]
isincldi [lemma, in hnat]
isincldni [lemma, in stnfsets]
isinclfromcoprodwithnegimage [lemma, in uu0]
isinclfromhfiber [lemma, in uu0]
isinclfromstn1 [lemma, in stnfsets]
isinclfromunit [lemma, in uu0]
isinclgtogw [lemma, in uu0]
isinclgwtog [lemma, in uu0]
isinclhomot [lemma, in uu0]
isinclii1 [lemma, in uu0]
isinclii2 [lemma, in uu0]
isinclplusn [lemma, in hnat]
isinclprabgrfrac [lemma, in algebra1]
isinclprabmonoidfrac [lemma, in algebra1]
isinclprcommrngfrac [lemma, in algebra1]
isinclpr21 [definition, in uu0]
isinclpr21carrier [lemma, in hSet]
isinclpr21compl [lemma, in uu0]
isinclpr21image [lemma, in hSet]
isinclpr21isolated [lemma, in uu0]
isinclpr21setquot [lemma, in hSet]
isinclpr21weq [lemma, in uu0]
isinclS [lemma, in hnat]
isinclsetquotfun [lemma, in hSet]
isinclstntonat [lemma, in stnfsets]
isincltwooutof3a [lemma, in uu0]
isincltwooutof3a [lemma, in algebra1]
isinclweq [lemma, in uu0]
isinclweqonpaths [lemma, in uu0]
isinhdneg [definition, in hProp]
isinv [definition, in algebra1]
isinvertible [definition, in algebra1]
isinvertiblemonob [lemma, in algebra1]
isinvertiblemonof [lemma, in algebra1]
isinvisob [lemma, in algebra1]
isinvisof [lemma, in algebra1]
isinvoncarrier [lemma, in algebra1]
isinvongrquot [lemma, in algebra1]
isisolated [definition, in uu0]
isisolateddecinclf [lemma, in uu0]
isisolatedinclb [lemma, in uu0]
isisolatedinstn [lemma, in stnfsets]
isisolatedn [lemma, in hnat]
isisolatedweqf [lemma, in uu0]
islcancellable [definition, in algebra1]
islcancellableisob [abbreviation, in algebra1]
islcancellablemonob [lemma, in algebra1]
isldistr [definition, in algebra1]
isldistrisob [abbreviation, in algebra1]
isldistrisof [lemma, in algebra1]
isldistrmonob [lemma, in algebra1]
islinv [definition, in algebra1]
islinvertible [definition, in algebra1]
islinvertibleisob [lemma, in algebra1]
islinvertibleisof [definition, in algebra1]
islinvmultwithminus1_is_l [lemma, in algebra1]
islunit [definition, in algebra1]
isminusmultwithminus1_is_l [lemma, in algebra1]
ismonoidcarrier [lemma, in algebra1]
ismonoiddirprod [definition, in algebra1]
ismonoidfun [definition, in algebra1]
ismonoidfuncomp [lemma, in algebra1]
ismonoidfuninvmap [lemma, in algebra1]
ismonoidop [definition, in algebra1]
ismonoidopisob [definition, in algebra1]
ismonoidopisof [definition, in algebra1]
ismonoidquot [definition, in algebra1]
isofhlevel [definition, in uu0]
isofhlevelcontr [lemma, in uu0]
isofhleveldirprod [lemma, in uu0]
isofhlevelf [definition, in uu0]
isofhlevelfcoprodf [lemma, in uu0]
isofhlevelff [lemma, in uu0]
isofhlevelfffromZ [lemma, in uu0]
isofhlevelffib [lemma, in uu0]
isofhlevelffromXY [lemma, in uu0]
isofhlevelfgf [lemma, in uu0]
isofhlevelfgtogw [lemma, in uu0]
isofhlevelfgwtog [lemma, in uu0]
isofhlevelfhfiberpr21 [lemma, in uu0]
isofhlevelfhfiberpr21y [lemma, in uu0]
isofhlevelfhomot [lemma, in uu0]
isofhlevelfhomot2 [lemma, in uu0]
isofhlevelfonpaths [lemma, in uu0]
isofhlevelfpmap [lemma, in uu0]
isofhlevelfpr21 [lemma, in uu0]
isofhlevelfromfun [lemma, in uu0]
isofhlevelfsn [lemma, in uu0]
isofhlevelfsnfib [lemma, in uu0]
isofhlevelfsnhfiberpr21 [lemma, in uu0]
isofhlevelfsnincl [lemma, in uu0]
isofhlevelfssn [lemma, in uu0]
isofhlevelfssnsumofmaps [lemma, in uu0]
isofhlevelfsumofmapsnoi [lemma, in uu0]
isofhlevelfweq [lemma, in uu0]
isofhlevelsn [lemma, in uu0]
isofhlevelsninclb [definition, in uu0]
isofhlevelsnprop [lemma, in uu0]
isofhlevelsnsummand1 [lemma, in uu0]
isofhlevelsnsummand2 [lemma, in uu0]
isofhlevelsnweqfromhlevelsn [lemma, in uu0]
isofhlevelsnweqtohlevelsn [lemma, in uu0]
isofhlevelssn [lemma, in uu0]
isofhlevelssncoprod [lemma, in uu0]
isofhlevelssnset [lemma, in uu0]
isofhleveltofun [lemma, in uu0]
isofhleveltotal2 [lemma, in uu0]
isofhlevelweqb [lemma, in uu0]
isofhlevelweqf [lemma, in uu0]
isofhlevelXfromfY [lemma, in uu0]
isofhlevelXfromg [lemma, in uu0]
isofnel [definition, in finitesets]
isofnelbool [definition, in finitesets]
isofnelcompl [definition, in finitesets]
isofnelcontr [definition, in finitesets]
isofnelcoprod [definition, in finitesets]
isofnelcoprodwithunit [definition, in finitesets]
isofnelempty [definition, in finitesets]
isofnelempty2 [definition, in finitesets]
isofnelondirprod [definition, in finitesets]
isofnelonfun [definition, in finitesets]
isofnelonweq [definition, in finitesets]
isofnelstn [definition, in finitesets]
isofnelunit [definition, in finitesets]
isofneluniv [lemma, in finitesets]
isofnelweqb [definition, in finitesets]
isofnelweqf [definition, in finitesets]
isolated [definition, in uu0]
isolatedpair [definition, in uu0]
isolatedtoisolatedii1 [lemma, in uu0]
isolatedtoisolatedii2 [lemma, in uu0]
ispo [definition, in hSet]
isrcancellable [definition, in algebra1]
isrcancellableisob [abbreviation, in algebra1]
isrcancellablemonob [lemma, in algebra1]
isrdistr [definition, in algebra1]
isrdistrisob [abbreviation, in algebra1]
isrdistrisof [lemma, in algebra1]
isrdistrmonob [lemma, in algebra1]
isrefl [definition, in hSet]
isrefldirprod [definition, in hSet]
isrefleqh [lemma, in hnat]
isreflpathshrel [definition, in hSet]
isrigops [definition, in algebra1]
isrinv [definition, in algebra1]
isrinvertible [definition, in algebra1]
isrinvertibleisob [lemma, in algebra1]
isrinvertibleisof [definition, in algebra1]
isrinvmultwithminus1_is_l [lemma, in algebra1]
isrng [definition, in algebra1]
isrngcarrier [lemma, in algebra1]
isrngdirprod [lemma, in algebra1]
isrngops [definition, in algebra1]
isrngopsif [lemma, in algebra1]
isrngopsisob [definition, in algebra1]
isrngopsisof [definition, in algebra1]
isrngquot [lemma, in algebra1]
isrunit [definition, in algebra1]
issubgr [definition, in algebra1]
issubmonoid [definition, in algebra1]
issubrng [definition, in algebra1]
issubsetwithbinop [definition, in algebra1]
issubsetwith2binop [definition, in algebra1]
issurjcomp [lemma, in hSet]
issurjective [definition, in hSet]
issurjprtoimage [lemma, in hSet]
issurjsetquotfun [lemma, in hSet]
issurjsetquotpr [lemma, in hSet]
issurjsetquot2pr [lemma, in hSet]
issurjtwooutof3b [lemma, in hSet]
issurjtwooutof3c [abbreviation, in hSet]
issymm [definition, in hSet]
issymmdirprod [definition, in hSet]
issymmpathshrel [definition, in hSet]
istrans [definition, in hSet]
istransdirprod [definition, in hSet]
istranspathshrel [definition, in hSet]
istwobinopfun [definition, in algebra1]
istwobinopfuncomp [lemma, in algebra1]
istwobinopfuninvmap [lemma, in algebra1]
isunit [definition, in algebra1]
isunital [definition, in algebra1]
isunitalisob [definition, in algebra1]
isunitalisof [definition, in algebra1]
isunitalpair [definition, in algebra1]
isunitindirprod [lemma, in algebra1]
isunitisob [lemma, in algebra1]
isunitisof [lemma, in algebra1]
isunitquot [lemma, in algebra1]
isweq [definition, in uu0]
isweqbandfmap [lemma, in uu0]
isweqboolsumtocoprod [lemma, in uu0]
isweqcontrcontr [lemma, in uu0]
isweqcontrtounit [lemma, in uu0]
isweqcoprodasstol [lemma, in uu0]
isweqcoprodasstor [lemma, in uu0]
isweqcoprodcomm [lemma, in uu0]
isweqcoprodf [lemma, in uu0]
isweqcoprodtoboolsum [lemma, in uu0]
isweqdeltap [lemma, in uu0]
isweqdirprodf [lemma, in uu0]
isweqdnitocompl [lemma, in stnfsets]
isweqetacorrection [lemma, in uu0]
isweqezmaphf [lemma, in uu0]
isweqezmappr21 [definition, in uu0]
isweqezmap1 [lemma, in uu0]
isweqfibtototal [lemma, in uu0]
isweqfinfibseq [lemma, in uu0]
isweqforalltohfiber [lemma, in uu0]
isweqforalltototal [lemma, in uu0]
isweqfpmap [lemma, in uu0]
isweqfromcoconusf [lemma, in uu0]
isweqfromcompltodisjoint [lemma, in uu0]
isweqfunextsec [lemma, in uu0]
isweqhff [lemma, in uu0]
isweqhfiberfp [lemma, in uu0]
isweqhfibersgtof' [lemma, in uu0]
isweqhfibersg'tof [lemma, in uu0]
isweqhfibertoforall [lemma, in uu0]
isweqhomot [lemma, in uu0]
isweqii1withneg [lemma, in uu0]
isweqii2withneg [lemma, in uu0]
isweqimplimpl [lemma, in uu0]
isweqinclandsurj [lemma, in hSet]
isweqinvezmaphf [definition, in uu0]
isweqinvmap [lemma, in uu0]
isweqlcompwithweq [lemma, in uu0]
isweqleFtototal2withnat [lemma, in hnat]
isweqletoleh [lemma, in hnat]
isweqlmultingr_is [lemma, in algebra1]
isweql3 [lemma, in uu0]
isweqmaponcompl [lemma, in uu0]
isweqmaponpaths [lemma, in uu0]
isweqmaponsec [lemma, in uu0]
isweqmaponsec1 [lemma, in uu0]
isweqonpathsincl [lemma, in uu0]
isweqpathscomp0r [lemma, in uu0]
isweqpathsinv0 [lemma, in uu0]
isweqpr21 [lemma, in uu0]
isweqpr21pr21 [lemma, in uu0]
isweqrcompwithweq [lemma, in uu0]
isweqrdistrtocoprod [lemma, in uu0]
isweqrdistrtoprod [lemma, in uu0]
isweqrecompl [lemma, in uu0]
isweqrmultingr_is [lemma, in algebra1]
isweqtococonusf [lemma, in uu0]
isweqtocompltodisjoint [lemma, in uu0]
isweqtocompltoii1x [lemma, in uu0]
isweqtocompltoii2y [lemma, in uu0]
isweqtoempty [definition, in uu0]
isweqtoempty2 [lemma, in uu0]
isweqtoforallpaths [lemma, in uu0]
isweqtotaltofib [lemma, in uu0]
isweqtotaltoforall [lemma, in uu0]
isweqtransportb [lemma, in uu0]
isweqtransportf [lemma, in uu0]
is2binophrel [definition, in algebra1]
is2binoptransrel [lemma, in algebra1]
iteration [definition, in uu0]
L
lastelement [definition, in stnfsets]ldistrax_is [definition, in algebra1]
le [definition, in hnat]
leb [definition, in hnat]
leF [inductive, in hnat]
leFiter [lemma, in hnat]
leFtototal2withnat [lemma, in hnat]
leFtototal2withnat_l0 [lemma, in hnat]
leF_O [constructor, in hnat]
leF_S [constructor, in hnat]
leh [definition, in hnat]
lehandmultl [lemma, in hnat]
lehandmultlinv [lemma, in hnat]
lehandmultr [lemma, in hnat]
lehandmultrinv [lemma, in hnat]
lehandplusl [lemma, in hnat]
lehandpluslinv [lemma, in hnat]
lehandplusr [lemma, in hnat]
lehandplusrinv [lemma, in hnat]
lehchoice [lemma, in hnat]
lehdinsn [lemma, in hnat]
lehimpllehs [lemma, in hnat]
lehlthtrans [lemma, in hnat]
lehmplusnm [lemma, in hnat]
lehmultnatdiv [lemma, in hnat]
lehnplusnm [lemma, in hnat]
lehnsn [lemma, in hnat]
lehpo [definition, in hnat]
lehrefl [lemma, in hnat]
lehsimplleh [lemma, in hnat]
lehsnimpllth [lemma, in hnat]
lehtole [lemma, in hnat]
lehtrans [lemma, in hnat]
leh0implis0 [lemma, in hnat]
lemmaeta1 [lemma, in uu0]
letoleh [lemma, in hnat]
le_n [definition, in hnat]
le_S [definition, in hnat]
lth [definition, in hnat]
lthandmultl [lemma, in hnat]
lthandmultlinv [lemma, in hnat]
lthandmultr [lemma, in hnat]
lthandmultrinv [lemma, in hnat]
lthimpllehsn [lemma, in hnat]
lthlehtrans [lemma, in hnat]
lthnatrem [lemma, in hnat]
lthtrans [lemma, in hnat]
lth1implis0 [lemma, in hnat]
lunax [definition, in algebra1]
lunax_is [definition, in algebra1]
M
maponcomplincl [definition, in uu0]maponcomplweq [definition, in uu0]
maponpaths [definition, in uu0]
maponpathscomp [lemma, in uu0]
maponpathscomp0 [definition, in uu0]
maponpathshomidinv [definition, in uu0]
maponpathshomid1 [lemma, in uu0]
maponpathshomid12 [lemma, in uu0]
maponpathshomid2 [lemma, in uu0]
maponpathsidfun [lemma, in uu0]
maponpathsinv0 [definition, in uu0]
maponsec [definition, in uu0]
maponsec1 [definition, in uu0]
maponsec1l0 [definition, in uu0]
maponsec1l1 [lemma, in uu0]
maponsec1l2 [lemma, in uu0]
minus1_is_l [definition, in algebra1]
monoid [definition, in algebra1]
monoidconstr [definition, in algebra1]
monoiddirprod [definition, in algebra1]
monoidfun [definition, in algebra1]
monoidfuncomp [definition, in algebra1]
monoidfuninvtoinv [lemma, in algebra1]
monoidfunpair [definition, in algebra1]
monoidfuntobinopfun [definition, in algebra1]
monoidincltomonoidfun [definition, in algebra1]
monoidiso [definition, in algebra1]
monoidisopair [definition, in algebra1]
monoidisotobinopiso [definition, in algebra1]
monoidisotomonoidmono [definition, in algebra1]
monoidmono [definition, in algebra1]
monoidmonocomp [definition, in algebra1]
monoidmonopair [definition, in algebra1]
monoidmonotobinopmono [definition, in algebra1]
monoidpair [definition, in algebra1]
monoidquot [definition, in algebra1]
multabmonoid [definition, in algebra1]
multabmonoidnat [definition, in hnat]
multmonoid [definition, in algebra1]
multmonoideqrel [definition, in algebra1]
multnsm [lemma, in hnat]
multn0 [lemma, in hnat]
multsnm [lemma, in hnat]
multsubmonoid [definition, in algebra1]
multx0_is_l [lemma, in algebra1]
mult0x_is_l [lemma, in algebra1]
N
natdiv [definition, in hnat]natdivrem [definition, in hnat]
natdivremrule [lemma, in hnat]
natdivremunique [lemma, in hnat]
natldistr [lemma, in hnat]
natmultassoc [lemma, in hnat]
natmultcomm [lemma, in hnat]
natmultl1 [lemma, in hnat]
natmultr1 [lemma, in hnat]
natnattohz [definition, in hz]
natplusassoc [lemma, in hnat]
natpluscomm [lemma, in hnat]
natplusl0 [lemma, in hnat]
natplusr0 [lemma, in hnat]
natpower [definition, in hnat]
natrdistr [lemma, in hnat]
natrem [definition, in hnat]
natset [definition, in hnat]
neg [definition, in uu0]
negf [definition, in uu0]
neggthmplusnm [lemma, in hnat]
neggthnn [lemma, in hnat]
neggthnplusnm [lemma, in hnat]
neggth0n [lemma, in hnat]
neghfiberdi [lemma, in hnat]
neghfiberdni [lemma, in stnfsets]
neghfiberii1y [lemma, in uu0]
neghfiberii2x [lemma, in uu0]
neghfiberplusn [lemma, in hnat]
neghfiberstntonat [lemma, in stnfsets]
negimage [definition, in uu0]
negimagepair [definition, in uu0]
negintersectii1ii2 [lemma, in uu0]
neglehgth [lemma, in hnat]
neglehsnn [lemma, in hnat]
neglehsn0 [lemma, in hnat]
negpathsii1ii2 [lemma, in uu0]
negpathsii2ii1 [lemma, in uu0]
negstn0 [definition, in stnfsets]
negweqstnsn0 [lemma, in stnfsets]
negweqstn0sn [lemma, in stnfsets]
nelstruct [definition, in finitesets]
nelstructonbool [definition, in finitesets]
nelstructoncompl [definition, in finitesets]
nelstructoncontr [definition, in finitesets]
nelstructoncoprod [definition, in finitesets]
nelstructoncoprodwithunit [definition, in finitesets]
nelstructondirprod [definition, in finitesets]
nelstructonempty [definition, in finitesets]
nelstructonempty2 [definition, in finitesets]
nelstructonforall [definition, in finitesets]
nelstructonfun [definition, in finitesets]
nelstructonstn [definition, in finitesets]
nelstructontotal2 [definition, in finitesets]
nelstructonunit [definition, in finitesets]
nelstructonweq [definition, in finitesets]
nelstructweqb [definition, in finitesets]
nelstructweqf [definition, in finitesets]
neqh [definition, in hnat]
neqhtonegpaths [lemma, in hnat]
noeqinjS [lemma, in hnat]
noil1 [lemma, in uu0]
nopathsfalsetotrue [lemma, in uu0]
nopathsOtoSx [lemma, in hnat]
nopathsSxtoO [lemma, in hnat]
nopathstruetofalse [lemma, in uu0]
O
onefiber [lemma, in uu0]op [definition, in algebra1]
op1 [definition, in algebra1]
op1axs_is [definition, in algebra1]
op2 [definition, in algebra1]
op2axs_is [definition, in algebra1]
P
paths [abbreviation, in uuu]pathscomp0 [definition, in uu0]
pathscomp0rid [definition, in uu0]
pathsdirprod [definition, in uu0]
pathseqrel [definition, in hSet]
pathsfuntransposofnet1t2 [lemma, in uu0]
pathsfuntransposoft1 [lemma, in uu0]
pathsfuntransposoft2 [lemma, in uu0]
pathshrel [definition, in hSet]
pathsinvcuntonweqoft [lemma, in uu0]
pathsinv0 [definition, in uu0]
pathsinv0inv0 [definition, in uu0]
pathsinv0l [definition, in uu0]
pathsinv0r [definition, in uu0]
pathsitertoplus [lemma, in hnat]
pathsrecomplfxtoy [lemma, in uu0]
pathssec1 [definition, in uu0]
pathssec2 [definition, in uu0]
pathssec2id [definition, in uu0]
pathssec3 [definition, in uu0]
pathsspace [definition, in uu0]
pathsspacetriple [definition, in uu0]
pathsspace' [definition, in uu0]
pathstoeqh [definition, in hnat]
pathsweq1 [definition, in uu0]
pathsweq1' [definition, in uu0]
pathsweq3 [definition, in uu0]
pathsweq4 [definition, in uu0]
pi0 [definition, in hSet]
pi0pr [definition, in hSet]
plusminusnmm [lemma, in hnat]
plusnsm [lemma, in hnat]
po [definition, in hSet]
popair [definition, in hSet]
Poset [definition, in hSet]
posetmorphism [definition, in hSet]
posetmorphismpair [definition, in hSet]
Posetpair [definition, in hSet]
prabgrfrac [definition, in algebra1]
prabmonoidfrac [definition, in algebra1]
prcommrngfrac [definition, in algebra1]
prodtofunfromcoprod [definition, in uu0]
prodtofuntoprod [definition, in uu0]
prodtosecovercoprod [definition, in uu0]
proofirrelevance [lemma, in uu0]
proofirrelevancecontr [lemma, in uu0]
prtoimage [definition, in hSet]
pr21 [definition, in uuu]
pr21binopeqrel [definition, in algebra1]
pr21binopfun [definition, in algebra1]
pr21binophrel [definition, in algebra1]
pr21binopiso [definition, in algebra1]
pr21binopmono [definition, in algebra1]
pr21binoppo [definition, in algebra1]
pr21carrier [definition, in hSet]
pr21compl [definition, in uu0]
pr21eqrel [definition, in hSet]
pr21hSet [definition, in hSet]
pr21image [definition, in hSet]
pr21incl [definition, in uu0]
pr21isabgroupop [definition, in algebra1]
pr21isabmonoidop [definition, in algebra1]
pr21iscommrngops [definition, in algebra1]
pr21isgroupop [definition, in algebra1]
pr21isolated [definition, in uu0]
pr21monoid [definition, in algebra1]
pr21monoidfun [definition, in algebra1]
pr21monoidiso [definition, in algebra1]
pr21monoidmono [definition, in algebra1]
pr21rng [definition, in algebra1]
pr21setquot [definition, in hSet]
pr21setwithbinop [definition, in algebra1]
pr21setwith2binop [definition, in algebra1]
pr21submonoids [definition, in algebra1]
pr21subrng [definition, in algebra1]
pr21subsetswithbinop [definition, in algebra1]
pr21subsetswith2binop [definition, in algebra1]
pr21twobinopeqrel [definition, in algebra1]
pr21twobinopfun [definition, in algebra1]
pr21twobinophrel [definition, in algebra1]
pr21twobinopiso [definition, in algebra1]
pr21twobinopmono [definition, in algebra1]
pr21twobinoppo [definition, in algebra1]
pr21weq [definition, in uu0]
pr21_c [projection, in uuu]
pr22 [definition, in uuu]
pr22_c [projection, in uuu]
R
rdistrax_is [definition, in algebra1]rdistrtocoprod [definition, in uu0]
rdistrtoprod [definition, in uu0]
recompl [definition, in uu0]
recomplf [definition, in uu0]
rng [definition, in algebra1]
rngassoc1 [definition, in algebra1]
rngassoc2 [definition, in algebra1]
rngaxs [definition, in algebra1]
rngcomm1 [definition, in algebra1]
rngcomm2 [definition, in algebra1]
rngconstr [definition, in algebra1]
rngdirprod [definition, in algebra1]
rngdistraxs [definition, in algebra1]
rngeqrel [definition, in algebra1]
rnginv1 [definition, in algebra1]
rngldistrax [definition, in algebra1]
rnglinvax1 [definition, in algebra1]
rnglunax1 [definition, in algebra1]
rnglunax2 [definition, in algebra1]
rngminus1 [definition, in algebra1]
rngminus1_is [definition, in algebra1]
rngmultwithminus1 [definition, in algebra1]
rngmultwithminus1_is [definition, in algebra1]
rngmultx0 [definition, in algebra1]
rngmultx0_is [definition, in algebra1]
rngmult0x [definition, in algebra1]
rngmult0x_is [definition, in algebra1]
rngop1axs [definition, in algebra1]
rngop2axs [definition, in algebra1]
rngpair [definition, in algebra1]
rngquot [definition, in algebra1]
rngrdistrax [definition, in algebra1]
rngrinvax1 [definition, in algebra1]
rngrunax1 [definition, in algebra1]
rngrunax2 [definition, in algebra1]
rngunel1 [definition, in algebra1]
rngunel2 [definition, in algebra1]
runax [definition, in algebra1]
runax_is [definition, in algebra1]
S
samehfibers [lemma, in uu0]secovercoprodtoprod [definition, in uu0]
sectohfiber [definition, in uu0]
sectohfibertosec [definition, in uu0]
setdirprod [definition, in hSet]
setproperty [definition, in hSet]
setquot [definition, in hSet]
setquotbooleq [definition, in hSet]
setquotbooleqint [definition, in hSet]
setquotbooleqintcomp [lemma, in hSet]
setquotbooleqtopaths [lemma, in hSet]
setquotfun [definition, in hSet]
setquotfuncomm [definition, in hSet]
setquotfun2 [definition, in hSet]
setquotfun2comm [lemma, in hSet]
setquotincl [definition, in hSet]
setquotinset [definition, in hSet]
setquotl0 [lemma, in hSet]
setquotpair [definition, in hSet]
setquotpathstobooleq [lemma, in hSet]
setquotpr [lemma, in hSet]
setquottodirprod [definition, in hSet]
setquottosetquot2 [definition, in hSet]
setquottouu0 [definition, in hSet]
setquotuniv [lemma, in hSet]
setquotunivcomm [lemma, in hSet]
setquotunivprop [lemma, in hSet]
setquotuniv2 [definition, in hSet]
setquotuniv2comm [lemma, in hSet]
setquotuniv2prop [lemma, in hSet]
setquotuniv3prop [lemma, in hSet]
setquot2 [definition, in hSet]
setquot2pr [definition, in hSet]
setquot2univ [definition, in hSet]
setquot2univcomm [lemma, in hSet]
setwithbinop [definition, in algebra1]
setwithbinopdirprod [definition, in algebra1]
setwithbinoppair [definition, in algebra1]
setwithbinopquot [definition, in algebra1]
setwithbinop1 [definition, in algebra1]
setwithbinop2 [definition, in algebra1]
setwith2binop [definition, in algebra1]
setwith2binopdirprod [definition, in algebra1]
setwith2binoppair [definition, in algebra1]
setwith2binopquot [definition, in algebra1]
stn [definition, in stnfsets]
stnfsets [library]
stnmtostnn [definition, in stnfsets]
stnpair [definition, in stnfsets]
stnprod [definition, in stnfsets]
stnsdnegweqtoeq [lemma, in stnfsets]
stnsum [definition, in stnfsets]
stntonat [definition, in stnfsets]
subabgrs [definition, in algebra1]
subabmonoids [definition, in algebra1]
subgrconstr [definition, in algebra1]
subgrpair [definition, in algebra1]
subgrs [definition, in algebra1]
subgrstosubmonoids [definition, in algebra1]
submonoidconstr [definition, in algebra1]
submonoidpair [definition, in algebra1]
submonoids [definition, in algebra1]
submonoidstosubsetswithbinop [definition, in algebra1]
subrngpair [definition, in algebra1]
subrngs [definition, in algebra1]
subrngtosubsetswith2binop [definition, in algebra1]
subsetsplit [definition, in uu0]
subsetsplitinv [definition, in uu0]
subsetswithbinop [definition, in algebra1]
subsetswithbinopconstr [definition, in algebra1]
subsetswithbinoppair [definition, in algebra1]
subsetswith2binop [definition, in algebra1]
subsetswith2binopconstr [definition, in algebra1]
subsetswith2binoppair [definition, in algebra1]
subtypesdirprod [definition, in hSet]
sumofmaps [definition, in uu0]
surjectionisepitosets [lemma, in hSet]
T
termfun [definition, in uu0]tococonusf [definition, in uu0]
tocompltodisjoint [definition, in uu0]
tocompltoii1x [definition, in uu0]
tocompltoii2y [definition, in uu0]
todneg [definition, in uu0]
toforallpaths [definition, in uu0]
tosecovertotal2 [definition, in uu0]
tosecoverunit [definition, in uu0]
tosubtypesdirprodcarrier [definition, in hSet]
totalfun [definition, in uu0]
totalsubmonoid [definition, in algebra1]
totalsubsetwithbinop [definition, in algebra1]
totalsubsetwith2binop [definition, in algebra1]
totalsubtype [definition, in hSet]
totaltoforall [definition, in uu0]
totaltoforalltototal [definition, in uu0]
total2 [record, in uuu]
total2asstol [lemma, in uu0]
total2asstor [lemma, in uu0]
total2withnattoleF [lemma, in hnat]
tototal2overcoprod [definition, in uu0]
tototal2overunit [definition, in uu0]
tounit [definition, in uu0]
tpair [constructor, in uuu]
tppr [definition, in uu0]
transportb [definition, in uu0]
transportf [definition, in uu0]
transposcommsqstr [definition, in uu0]
transposhfpsqstr [lemma, in uu0]
truetonegfalse [definition, in uu0]
twobinopeqrel [definition, in algebra1]
twobinopeqrelpair [definition, in algebra1]
twobinopfun [definition, in algebra1]
twobinopfuncomp [definition, in algebra1]
twobinopfunpair [definition, in algebra1]
twobinophrel [definition, in algebra1]
twobinophrelpair [definition, in algebra1]
twobinopincltotwobinopfun [definition, in algebra1]
twobinopiso [definition, in algebra1]
twobinopisocomp [definition, in algebra1]
twobinopisopair [definition, in algebra1]
twobinopisototwobinopmono [definition, in algebra1]
twobinopmono [definition, in algebra1]
twobinopmonocomp [definition, in algebra1]
twobinopmonopair [definition, in algebra1]
twobinoppo [definition, in algebra1]
twobinoppopair [definition, in algebra1]
twooutof3a [lemma, in uu0]
twooutof3b [lemma, in uu0]
twooutof3c [lemma, in uu0]
U
uahp [axiom, in hProp]uip [lemma, in uu0]
unel [definition, in algebra1]
unel_is [definition, in algebra1]
unitl0 [lemma, in uu0]
unitl1 [lemma, in uu0]
unitl2 [lemma, in uu0]
unitl3 [lemma, in uu0]
univfromtwoaxiomshProp [lemma, in hProp]
UU [definition, in uu0]
UUU [abbreviation, in uuu]
uuu [library]
UU0 [definition, in hProp]
uu0 [library]
W
weq [definition, in uu0]weqabgrfrac [definition, in algebra1]
weqbandf [definition, in uu0]
weqbfun [definition, in uu0]
weqboolsumtocoprod [definition, in uu0]
weqbweq [lemma, in uu0]
weqcomp [definition, in uu0]
weqcontrcontr [definition, in uu0]
weqcontrtounit [definition, in uu0]
weqcoprodasstol [definition, in uu0]
weqcoprodasstor [definition, in uu0]
weqcoprodcomm [definition, in uu0]
weqcoprodf [definition, in uu0]
weqcoprodsplit [definition, in uu0]
weqcoprodtoboolsum [definition, in uu0]
weqcoproj [definition, in uu0]
weqcutforstn [lemma, in stnfsets]
weqcutonweq [definition, in uu0]
weqdirprodasstol [definition, in uu0]
weqdirprodasstor [definition, in uu0]
weqdirprodcomm [definition, in uu0]
weqdirprodf [definition, in uu0]
weqdnicompl [definition, in stnfsets]
weqdnicoprod [definition, in stnfsets]
weqeqhtopaths [definition, in hnat]
weqeqweqhProp [definition, in hProp]
weqeta [definition, in uu0]
weqffun [definition, in uu0]
weqfibtototal [definition, in uu0]
weqforalltohfiber [definition, in uu0]
weqforalltototal [definition, in uu0]
weqfp [definition, in uu0]
weqfromcoconusf [definition, in uu0]
weqfromcoprodofstn [lemma, in stnfsets]
weqfromdecsubsetofstn [lemma, in stnfsets]
weqfromfunstntostn [lemma, in stnfsets]
weqfromhfiberfromstn [lemma, in stnfsets]
weqfromprodofstn [lemma, in stnfsets]
weqfromweqstntostn [lemma, in stnfsets]
weqfunextsec [definition, in uu0]
weqfunfromcontr [definition, in uu0]
weqfunfromcoprodtoprod [lemma, in uu0]
weqfunfromdirprod [definition, in uu0]
weqfunfromtotal2 [definition, in uu0]
weqfunfromunit [definition, in uu0]
weqfuntoprodtoprod [lemma, in uu0]
weqfuntototaltototal [definition, in uu0]
weqfweq [lemma, in uu0]
weqgradth [definition, in uu0]
weqhfibercoprodf1 [lemma, in uu0]
weqhfibercoprodf2 [lemma, in uu0]
weqhfiberdnihfiberdi [lemma, in stnfsets]
weqhfibernoi1 [lemma, in uu0]
weqhfibernoi2 [lemma, in uu0]
weqhfibersgtof' [definition, in uu0]
weqhfibersgwtog [lemma, in uu0]
weqhfibersg'tof [definition, in uu0]
weqhfibershomot [lemma, in uu0]
weqhfibersofsumofmaps [lemma, in uu0]
weqhfibertobhfiber [lemma, in uu0]
weqhfibertocontr [lemma, in uu0]
weqhfibertoforall [definition, in uu0]
weqhfibertohfp [lemma, in uu0]
weqhfibertounit [lemma, in uu0]
weqhfpcomm [lemma, in uu0]
weqhfptohfpoverX [definition, in uu0]
weqhfptohfpoverX' [definition, in uu0]
weqhrelhrel0abmonoidfrac [lemma, in algebra1]
weqhrelhrel0commrngfrac [lemma, in algebra1]
weqii1withneg [definition, in uu0]
weqii2withneg [definition, in uu0]
weqimplimpl [definition, in uu0]
weqinvweq [lemma, in uu0]
weqisolatedstntostn [definition, in stnfsets]
weqlcancellablercancellable [lemma, in algebra1]
weqldistrrdistr [lemma, in algebra1]
weqleFtototalwithnat [definition, in hnat]
weqletoleh [definition, in hnat]
weqlinvertiblerinvertible [lemma, in algebra1]
weqlinvrinv [lemma, in algebra1]
weqlunitrunit [lemma, in algebra1]
weqoncompl [definition, in uu0]
weqonpaths [definition, in uu0]
weqonpathsincl [definition, in uu0]
weqonsecbase [definition, in uu0]
weqonseqfibers [definition, in uu0]
weqpair [definition, in uu0]
weqpathsinsetquot [lemma, in hSet]
weqpathsinv0 [definition, in uu0]
weqpathsweqhProp [definition, in hProp]
weqpr21 [definition, in uu0]
weqrdistrtocoprod [definition, in uu0]
weqrdistrtoprod [definition, in uu0]
weqrecompl [definition, in uu0]
weqrecomplf [definition, in uu0]
weqsecovercontr [definition, in uu0]
weqsecovercoprodtoprod [definition, in uu0]
weqsecovertotal2 [definition, in uu0]
weqsecoverunit [definition, in uu0]
weqsetquotsurj [definition, in hSet]
weqsetquottodirprod [lemma, in hSet]
weqsetquotweq [definition, in hSet]
weqstnprod [lemma, in stnfsets]
weqstnsum [lemma, in stnfsets]
weqstnsum2 [lemma, in stnfsets]
weqstn0toempty [definition, in stnfsets]
weqstn1tounit [definition, in stnfsets]
weqstn2tobool [definition, in stnfsets]
weqsubsetsplit [lemma, in uu0]
weqsubtypesdirprod [lemma, in hSet]
weqtococonusf [definition, in uu0]
weqtocompltodisjoint [definition, in uu0]
weqtodirprodwithunit [definition, in uu0]
weqtoempty [definition, in uu0]
weqtoempty2 [definition, in uu0]
weqtoeqstn [lemma, in stnfsets]
weqtoforallpaths [lemma, in uu0]
weqtoincl [definition, in uu0]
weqtopathshProp [definition, in hProp]
weqtotalsubtype [definition, in hSet]
weqtotaltofib [definition, in uu0]
weqtotaltoforall [definition, in uu0]
weqtotal2asstol [definition, in uu0]
weqtotal2asstor [lemma, in uu0]
weqtotal2overcoprod [lemma, in uu0]
weqtotal2overunit [lemma, in uu0]
weqtranspos [lemma, in uu0]
weqtranspos0 [definition, in uu0]
wequnittocontr [definition, in uu0]
weqweqstnsn [lemma, in stnfsets]
weqZtohfp [definition, in uu0]
wittohexists [definition, in hProp]
other
_ + _ (addoperation_scope) [notation, in algebra1]- _ (hz_scope) [notation, in hz]
_ - _ (hz_scope) [notation, in hz]
_ + _ (hz_scope) [notation, in hz]
0 (hz_scope) [notation, in hz]
_ * _ (multoperation_scope) [notation, in algebra1]
_ * _ (rng_scope) [notation, in algebra1]
0 (rng_scope) [notation, in algebra1]
_ + _ (rng_scope) [notation, in algebra1]
-1 (rng_scope) [notation, in algebra1]
1 (rng_scope) [notation, in algebra1]
_ * _ (twobinops_scope) [notation, in algebra1]
_ + _ (twobinops_scope) [notation, in algebra1]
Projection Index
P
pr21_c [in uuu]pr22_c [in uuu]
Record Index
T
total2 [in uuu]Lemma Index
A
abgrfracinvcomp [in algebra1]abgrfracisinv [in algebra1]
abmonoidoprer [in algebra1]
absvalhzintcomp [in hz]
C
centralfiber [in uu0]commrngfracinv1comp [in algebra1]
commrngfracisinv1 [in algebra1]
commrngfracl1 [in algebra1]
commrngfracl2 [in algebra1]
commrngfracl3 [in algebra1]
commrngfracl4l [in algebra1]
commrngfracl4r [in algebra1]
commrngfracl5 [in algebra1]
commrngfracl6 [in algebra1]
commrngfracl7l [in algebra1]
commrngfracl7r [in algebra1]
commrngfracop1comp [in algebra1]
commsqstrtocomplxstr [in uu0]
complxstrtocommsqstr [in uu0]
connectedcoconusfromt [in uu0]
connectedcoconustot [in uu0]
constr2 [in uu0]
coprodofhfiberstohfiber [in uu0]
D
diaglemma2 [in uu0]disjointl1 [in uu0]
dneganddnegl1 [in uu0]
dnicommsq [in stnfsets]
dnihfsq [in stnfsets]
E
eqfromdnegeq [in uu0]etacoronpaths [in uu0]
etacorrectiononpaths [in uu0]
F
fibseqstrtohfsqstr [in uu0]funcontr [in uu0]
funcontrtwice [in uu0]
functtransportf [in uu0]
funextweql1 [in uu0]
G
gehdinn [in hnat]gehgthtrans [in hnat]
gehsnimplgth [in hnat]
gehtrans [in hnat]
gradth [in uu0]
grquotinvcomp [in algebra1]
gthandplusl [in hnat]
gthandpluslinv [in hnat]
gthandplusr [in hnat]
gthandplusrinv [in hnat]
gthasymm [in hnat]
gthchoice [in hnat]
gthgehtrans [in hnat]
gthimplgeh [in hnat]
gthimplgehsn [in hnat]
gthimplgths [in hnat]
gthsnn [in hnat]
gthtrans [in hnat]
H
hconjtohdisj [in hProp]hfibershomotftog [in uu0]
hfibershomotgtof [in uu0]
hfibertocoprodofhfibers [in uu0]
hfibertriangle1 [in uu0]
hfibertriangle1inv0 [in uu0]
hfibertriangle2 [in uu0]
hfsqstrtofibseqstr [in uu0]
hinhcoprod [in hProp]
hlevelntosn [in uu0]
hlevelretract [in uu0]
homotd3g [in uu0]
homotfuntranspos2 [in uu0]
homotrecomplnat [in uu0]
hrelabmonoidfrac_l [in algebra1]
hzplusassoc [in hz]
hzpluscomm [in hz]
hzplusl0 [in hz]
hzplusr0 [in hz]
I
idisweq [in uu0]ifcontrthenunitl0 [in uu0]
impred [in uu0]
impredfun [in uu0]
impredtech1 [in uu0]
impredtwice [in uu0]
invertibilityinabmonoidfrac [in algebra1]
invertibilityincommrngfrac [in algebra1]
invinv [in uu0]
invmaponpathsS [in hnat]
invproofirrelevance [in uu0]
isabgrcarrier [in algebra1]
isabgrdirprod [in algebra1]
isabgrquot [in algebra1]
isabmonoidcarrier [in algebra1]
isabmonoiddirprod [in algebra1]
isabmonoidquot [in algebra1]
isaninvpropneg [in uu0]
isaninv1 [in uu0]
isapropaninvprop [in uu0]
isapropdec [in uu0]
isapropdneg [in uu0]
isapropempty [in uu0]
isapropempty2 [in uu0]
isapropifcontr [in uu0]
isapropifnegtrue [in uu0]
isapropimeqclass [in hSet]
isapropimpl [in uu0]
isapropinvstruct [in algebra1]
isapropisabgroupop [in algebra1]
isapropisabmonoidop [in algebra1]
isapropisaprop [in uu0]
isapropisaset [in uu0]
isapropisassoc [in algebra1]
isapropisbinopfun [in algebra1]
isapropisbinophrel [in algebra1]
isapropischoicebase [in hSet]
isapropiscomm [in algebra1]
isapropiscommrng [in algebra1]
isapropiscontr [in uu0]
isapropisdeceq [in uu0]
isapropisdistr [in algebra1]
isapropiseqclass [in hSet]
isapropisgroupop [in algebra1]
isapropishinh [in hProp]
isapropisinv [in algebra1]
isapropisisolated [in uu0]
isapropisldistr [in algebra1]
isapropislinv [in algebra1]
isapropislunit [in algebra1]
isapropismonoidfun [in algebra1]
isapropismonoidop [in algebra1]
isapropisofhlevel [in uu0]
isapropisofhlevelf [in uu0]
isapropisrdistr [in algebra1]
isapropisrinv [in algebra1]
isapropisrngops [in algebra1]
isapropisrunit [in algebra1]
isapropissubgr [in algebra1]
isapropissubmonoid [in algebra1]
isapropissubrng [in algebra1]
isapropissubsetwithbinop [in algebra1]
isapropissubsetwith2binop [in algebra1]
isapropissurjective [in hSet]
isapropistwobinopfun [in algebra1]
isapropisunital [in algebra1]
isapropisweq [in uu0]
isapropis2binophrel [in algebra1]
isaprople [in hnat]
isapropneg [in uu0]
isapropneg2 [in uu0]
isaproppathsfromisolated [in uu0]
isaproppathstoisolated [in uu0]
isapropsubtype [in hSet]
isapropweqfromcontr [in uu0]
isapropweqfromempty [in uu0]
isapropweqfromempty2 [in uu0]
isapropweqfromprop [in uu0]
isapropweqfromunit [in uu0]
isapropweqtocontr [in uu0]
isapropweqtoempty [in uu0]
isapropweqtoempty2 [in uu0]
isapropweqtoprop [in uu0]
isapropweqtounit [in uu0]
isasetbinopfun [in algebra1]
isasetbool [in uu0]
isasetcoprod [in uu0]
isasetdirprod [in uu0]
isasetempty [in uu0]
isasethProp [in hProp]
isasethsubtypes [in hSet]
isasethz [in hz]
isasetifdeceq [in uu0]
isasetifiscontrloops [in uu0]
isasetmonoidfun [in algebra1]
isasetnat [in hnat]
isasetsetquot [in hSet]
isasetsetquot2 [in hSet]
isasetstn [in stnfsets]
isasetsubset [in uu0]
isasettwobinopfun [in algebra1]
isasetunit [in uu0]
isasetweqfromset [in uu0]
isasetweqtoset [in uu0]
isassocdirprod [in algebra1]
isassocisof [in algebra1]
isassocmonob [in algebra1]
isassocquot [in algebra1]
isbinopfuncomp [in algebra1]
isbinopfuninvmap [in algebra1]
isbinophrelabgrfrac [in algebra1]
isbinophrelabmonoidfrac [in algebra1]
isbinoptransrel [in algebra1]
iscancellablemonob [in algebra1]
ischoicebasecontr [in hSet]
ischoicebasecoprod [in hSet]
ischoicebaseempty [in hSet]
ischoicebaseempty2 [in hSet]
ischoicebasefiniteset [in finitesets]
ischoicebasestn [in stnfsets]
ischoicebaseunit [in hSet]
ischoicebaseweqb [in hSet]
ischoicebaseweqf [in hSet]
iscommisof [in algebra1]
iscommmonob [in algebra1]
iscommrngcarrier [in algebra1]
iscommrngdirprod [in algebra1]
iscommrngquot [in algebra1]
iscompsetquotpr [in hSet]
iscompsetquot2pr [in hSet]
iscontraprop1 [in uu0]
iscontraprop1inv [in uu0]
iscontrcoconusfromt [in uu0]
iscontrcoconustot [in uu0]
iscontrfunfromempty [in uu0]
iscontrfunfromempty2 [in uu0]
iscontrfuntocontr [in uu0]
iscontrfuntounit [in uu0]
iscontrhfiberdi [in hnat]
iscontrhfiberdni [in stnfsets]
iscontrhfibereqbx [in uu0]
iscontrhfiberii1x [in uu0]
iscontrhfiberii2y [in uu0]
iscontrhfiberl1 [in uu0]
iscontrhfiberl2 [in uu0]
iscontrhfiberofincl [in uu0]
iscontrhfiberplusn [in hnat]
iscontrhfiberstntonat [in stnfsets]
iscontrifweqtounit [in uu0]
iscontriscontr [in uu0]
iscontrloopsifisaset [in uu0]
iscontrpathsinunit [in uu0]
iscontrretract [in uu0]
iscontrstn1 [in stnfsets]
iscontrunit [in uu0]
iscontrweqb [in uu0]
iscontrweqf [in uu0]
iscoprojfromisdecincl [in uu0]
isdeceqabgrfrac [in algebra1]
isdeceqabmonoidfrac [in algebra1]
isdeceqbool [in uu0]
isdeceqcommrngfrac [in algebra1]
isdeceqhz [in hz]
isdeceqif [in uu0]
isdeceqifisaprop [in uu0]
isdeceqinclb [in uu0]
isdeceqnat [in hnat]
isdeceqsetquot_non_constr [in hSet]
isdeceqstn [in stnfsets]
isdeceqweqb [in uu0]
isdeceqweqf [in uu0]
isdecinclcomp [in uu0]
isdecincldi [in hnat]
isdecincldni [in stnfsets]
isdecinclf [in uu0]
isdecinclfromiscoproj [in uu0]
isdecinclfromisweq [in uu0]
isdecinclg [in uu0]
isdecinclhomot [in uu0]
isdecinclii1 [in uu0]
isdecinclii2 [in uu0]
isdecinclplusn [in hnat]
isdecinclpr21 [in uu0]
isdecinclS [in hnat]
isdecinclstntonat [in stnfsets]
isdecincltoisincl [in uu0]
isdecpropdirprod [in uu0]
isdecpropempty [in uu0]
isdecpropeqh [in hnat]
isdecpropfibseq0 [in uu0]
isdecpropfibseq1 [in uu0]
isdecpropfromdecincl [in uu0]
isdecpropfromiscontr [in uu0]
isdecpropfromneg [in uu0]
isdecpropgth [in hnat]
isdecpropif [in uu0]
isdecprople [in hnat]
isdecpropleh [in hnat]
isdecproppaths [in uu0]
isdecproppathsfromisolated [in uu0]
isdecproppathstoisolated [in uu0]
isdecproptoisaprop [in uu0]
isdecpropweqb [in uu0]
isdecpropweqf [in uu0]
isdistrisof [in algebra1]
iseqclassdirprod [in hSet]
iseqrelabgrfrac [in algebra1]
iseqrelabmonoidfrac [in algebra1]
isfibseqg [in uu0]
isfibseqpr21 [in uu0]
isgrdirprod [in algebra1]
isgroupopif [in algebra1]
ishfsqweqhfibersgtof' [in uu0]
ishfsqweqhfibersg'tof [in uu0]
ishinhsubtypesdirprod [in hSet]
ishomotinclrecomplf [in uu0]
isinclbetweensets [in uu0]
isinclcomp [in algebra1]
isinclcomp [in uu0]
isincldi [in hnat]
isincldni [in stnfsets]
isinclfromcoprodwithnegimage [in uu0]
isinclfromhfiber [in uu0]
isinclfromstn1 [in stnfsets]
isinclfromunit [in uu0]
isinclgtogw [in uu0]
isinclgwtog [in uu0]
isinclhomot [in uu0]
isinclii1 [in uu0]
isinclii2 [in uu0]
isinclplusn [in hnat]
isinclprabgrfrac [in algebra1]
isinclprabmonoidfrac [in algebra1]
isinclprcommrngfrac [in algebra1]
isinclpr21carrier [in hSet]
isinclpr21compl [in uu0]
isinclpr21image [in hSet]
isinclpr21isolated [in uu0]
isinclpr21setquot [in hSet]
isinclpr21weq [in uu0]
isinclS [in hnat]
isinclsetquotfun [in hSet]
isinclstntonat [in stnfsets]
isincltwooutof3a [in uu0]
isincltwooutof3a [in algebra1]
isinclweq [in uu0]
isinclweqonpaths [in uu0]
isinvertiblemonob [in algebra1]
isinvertiblemonof [in algebra1]
isinvisob [in algebra1]
isinvisof [in algebra1]
isinvoncarrier [in algebra1]
isinvongrquot [in algebra1]
isisolateddecinclf [in uu0]
isisolatedinclb [in uu0]
isisolatedinstn [in stnfsets]
isisolatedn [in hnat]
isisolatedweqf [in uu0]
islcancellablemonob [in algebra1]
isldistrisof [in algebra1]
isldistrmonob [in algebra1]
islinvertibleisob [in algebra1]
islinvmultwithminus1_is_l [in algebra1]
isminusmultwithminus1_is_l [in algebra1]
ismonoidcarrier [in algebra1]
ismonoidfuncomp [in algebra1]
ismonoidfuninvmap [in algebra1]
isofhlevelcontr [in uu0]
isofhleveldirprod [in uu0]
isofhlevelfcoprodf [in uu0]
isofhlevelff [in uu0]
isofhlevelfffromZ [in uu0]
isofhlevelffib [in uu0]
isofhlevelffromXY [in uu0]
isofhlevelfgf [in uu0]
isofhlevelfgtogw [in uu0]
isofhlevelfgwtog [in uu0]
isofhlevelfhfiberpr21 [in uu0]
isofhlevelfhfiberpr21y [in uu0]
isofhlevelfhomot [in uu0]
isofhlevelfhomot2 [in uu0]
isofhlevelfonpaths [in uu0]
isofhlevelfpmap [in uu0]
isofhlevelfpr21 [in uu0]
isofhlevelfromfun [in uu0]
isofhlevelfsn [in uu0]
isofhlevelfsnfib [in uu0]
isofhlevelfsnhfiberpr21 [in uu0]
isofhlevelfsnincl [in uu0]
isofhlevelfssn [in uu0]
isofhlevelfssnsumofmaps [in uu0]
isofhlevelfsumofmapsnoi [in uu0]
isofhlevelfweq [in uu0]
isofhlevelsn [in uu0]
isofhlevelsnprop [in uu0]
isofhlevelsnsummand1 [in uu0]
isofhlevelsnsummand2 [in uu0]
isofhlevelsnweqfromhlevelsn [in uu0]
isofhlevelsnweqtohlevelsn [in uu0]
isofhlevelssn [in uu0]
isofhlevelssncoprod [in uu0]
isofhlevelssnset [in uu0]
isofhleveltofun [in uu0]
isofhleveltotal2 [in uu0]
isofhlevelweqb [in uu0]
isofhlevelweqf [in uu0]
isofhlevelXfromfY [in uu0]
isofhlevelXfromg [in uu0]
isofneluniv [in finitesets]
isolatedtoisolatedii1 [in uu0]
isolatedtoisolatedii2 [in uu0]
isrcancellablemonob [in algebra1]
isrdistrisof [in algebra1]
isrdistrmonob [in algebra1]
isrefleqh [in hnat]
isrinvertibleisob [in algebra1]
isrinvmultwithminus1_is_l [in algebra1]
isrngcarrier [in algebra1]
isrngdirprod [in algebra1]
isrngopsif [in algebra1]
isrngquot [in algebra1]
issurjcomp [in hSet]
issurjprtoimage [in hSet]
issurjsetquotfun [in hSet]
issurjsetquotpr [in hSet]
issurjsetquot2pr [in hSet]
issurjtwooutof3b [in hSet]
istwobinopfuncomp [in algebra1]
istwobinopfuninvmap [in algebra1]
isunitindirprod [in algebra1]
isunitisob [in algebra1]
isunitisof [in algebra1]
isunitquot [in algebra1]
isweqbandfmap [in uu0]
isweqboolsumtocoprod [in uu0]
isweqcontrcontr [in uu0]
isweqcontrtounit [in uu0]
isweqcoprodasstol [in uu0]
isweqcoprodasstor [in uu0]
isweqcoprodcomm [in uu0]
isweqcoprodf [in uu0]
isweqcoprodtoboolsum [in uu0]
isweqdeltap [in uu0]
isweqdirprodf [in uu0]
isweqdnitocompl [in stnfsets]
isweqetacorrection [in uu0]
isweqezmaphf [in uu0]
isweqezmap1 [in uu0]
isweqfibtototal [in uu0]
isweqfinfibseq [in uu0]
isweqforalltohfiber [in uu0]
isweqforalltototal [in uu0]
isweqfpmap [in uu0]
isweqfromcoconusf [in uu0]
isweqfromcompltodisjoint [in uu0]
isweqfunextsec [in uu0]
isweqhff [in uu0]
isweqhfiberfp [in uu0]
isweqhfibersgtof' [in uu0]
isweqhfibersg'tof [in uu0]
isweqhfibertoforall [in uu0]
isweqhomot [in uu0]
isweqii1withneg [in uu0]
isweqii2withneg [in uu0]
isweqimplimpl [in uu0]
isweqinclandsurj [in hSet]
isweqinvmap [in uu0]
isweqlcompwithweq [in uu0]
isweqleFtototal2withnat [in hnat]
isweqletoleh [in hnat]
isweqlmultingr_is [in algebra1]
isweql3 [in uu0]
isweqmaponcompl [in uu0]
isweqmaponpaths [in uu0]
isweqmaponsec [in uu0]
isweqmaponsec1 [in uu0]
isweqonpathsincl [in uu0]
isweqpathscomp0r [in uu0]
isweqpathsinv0 [in uu0]
isweqpr21 [in uu0]
isweqpr21pr21 [in uu0]
isweqrcompwithweq [in uu0]
isweqrdistrtocoprod [in uu0]
isweqrdistrtoprod [in uu0]
isweqrecompl [in uu0]
isweqrmultingr_is [in algebra1]
isweqtococonusf [in uu0]
isweqtocompltodisjoint [in uu0]
isweqtocompltoii1x [in uu0]
isweqtocompltoii2y [in uu0]
isweqtoempty2 [in uu0]
isweqtoforallpaths [in uu0]
isweqtotaltofib [in uu0]
isweqtotaltoforall [in uu0]
isweqtransportb [in uu0]
isweqtransportf [in uu0]
is2binoptransrel [in algebra1]
L
leFiter [in hnat]leFtototal2withnat [in hnat]
leFtototal2withnat_l0 [in hnat]
lehandmultl [in hnat]
lehandmultlinv [in hnat]
lehandmultr [in hnat]
lehandmultrinv [in hnat]
lehandplusl [in hnat]
lehandpluslinv [in hnat]
lehandplusr [in hnat]
lehandplusrinv [in hnat]
lehchoice [in hnat]
lehdinsn [in hnat]
lehimpllehs [in hnat]
lehlthtrans [in hnat]
lehmplusnm [in hnat]
lehmultnatdiv [in hnat]
lehnplusnm [in hnat]
lehnsn [in hnat]
lehrefl [in hnat]
lehsimplleh [in hnat]
lehsnimpllth [in hnat]
lehtole [in hnat]
lehtrans [in hnat]
leh0implis0 [in hnat]
lemmaeta1 [in uu0]
letoleh [in hnat]
lthandmultl [in hnat]
lthandmultlinv [in hnat]
lthandmultr [in hnat]
lthandmultrinv [in hnat]
lthimpllehsn [in hnat]
lthlehtrans [in hnat]
lthnatrem [in hnat]
lthtrans [in hnat]
lth1implis0 [in hnat]
M
maponpathscomp [in uu0]maponpathshomid1 [in uu0]
maponpathshomid12 [in uu0]
maponpathshomid2 [in uu0]
maponpathsidfun [in uu0]
maponsec1l1 [in uu0]
maponsec1l2 [in uu0]
monoidfuninvtoinv [in algebra1]
multnsm [in hnat]
multn0 [in hnat]
multsnm [in hnat]
multx0_is_l [in algebra1]
mult0x_is_l [in algebra1]
N
natdivremrule [in hnat]natdivremunique [in hnat]
natldistr [in hnat]
natmultassoc [in hnat]
natmultcomm [in hnat]
natmultl1 [in hnat]
natmultr1 [in hnat]
natplusassoc [in hnat]
natpluscomm [in hnat]
natplusl0 [in hnat]
natplusr0 [in hnat]
natrdistr [in hnat]
neggthmplusnm [in hnat]
neggthnn [in hnat]
neggthnplusnm [in hnat]
neggth0n [in hnat]
neghfiberdi [in hnat]
neghfiberdni [in stnfsets]
neghfiberii1y [in uu0]
neghfiberii2x [in uu0]
neghfiberplusn [in hnat]
neghfiberstntonat [in stnfsets]
negintersectii1ii2 [in uu0]
neglehgth [in hnat]
neglehsnn [in hnat]
neglehsn0 [in hnat]
negpathsii1ii2 [in uu0]
negpathsii2ii1 [in uu0]
negweqstnsn0 [in stnfsets]
negweqstn0sn [in stnfsets]
neqhtonegpaths [in hnat]
noeqinjS [in hnat]
noil1 [in uu0]
nopathsfalsetotrue [in uu0]
nopathsOtoSx [in hnat]
nopathsSxtoO [in hnat]
nopathstruetofalse [in uu0]
O
onefiber [in uu0]P
pathsfuntransposofnet1t2 [in uu0]pathsfuntransposoft1 [in uu0]
pathsfuntransposoft2 [in uu0]
pathsinvcuntonweqoft [in uu0]
pathsitertoplus [in hnat]
pathsrecomplfxtoy [in uu0]
plusminusnmm [in hnat]
plusnsm [in hnat]
proofirrelevance [in uu0]
proofirrelevancecontr [in uu0]
S
samehfibers [in uu0]setquotbooleqintcomp [in hSet]
setquotbooleqtopaths [in hSet]
setquotfun2comm [in hSet]
setquotl0 [in hSet]
setquotpathstobooleq [in hSet]
setquotpr [in hSet]
setquotuniv [in hSet]
setquotunivcomm [in hSet]
setquotunivprop [in hSet]
setquotuniv2comm [in hSet]
setquotuniv2prop [in hSet]
setquotuniv3prop [in hSet]
setquot2univcomm [in hSet]
stnsdnegweqtoeq [in stnfsets]
surjectionisepitosets [in hSet]
T
total2asstol [in uu0]total2asstor [in uu0]
total2withnattoleF [in hnat]
transposhfpsqstr [in uu0]
twooutof3a [in uu0]
twooutof3b [in uu0]
twooutof3c [in uu0]
U
uip [in uu0]unitl0 [in uu0]
unitl1 [in uu0]
unitl2 [in uu0]
unitl3 [in uu0]
univfromtwoaxiomshProp [in hProp]
W
weqbweq [in uu0]weqcutforstn [in stnfsets]
weqfromcoprodofstn [in stnfsets]
weqfromdecsubsetofstn [in stnfsets]
weqfromfunstntostn [in stnfsets]
weqfromhfiberfromstn [in stnfsets]
weqfromprodofstn [in stnfsets]
weqfromweqstntostn [in stnfsets]
weqfunfromcoprodtoprod [in uu0]
weqfuntoprodtoprod [in uu0]
weqfweq [in uu0]
weqhfibercoprodf1 [in uu0]
weqhfibercoprodf2 [in uu0]
weqhfiberdnihfiberdi [in stnfsets]
weqhfibernoi1 [in uu0]
weqhfibernoi2 [in uu0]
weqhfibersgwtog [in uu0]
weqhfibershomot [in uu0]
weqhfibersofsumofmaps [in uu0]
weqhfibertobhfiber [in uu0]
weqhfibertocontr [in uu0]
weqhfibertohfp [in uu0]
weqhfibertounit [in uu0]
weqhfpcomm [in uu0]
weqhrelhrel0abmonoidfrac [in algebra1]
weqhrelhrel0commrngfrac [in algebra1]
weqinvweq [in uu0]
weqlcancellablercancellable [in algebra1]
weqldistrrdistr [in algebra1]
weqlinvertiblerinvertible [in algebra1]
weqlinvrinv [in algebra1]
weqlunitrunit [in algebra1]
weqpathsinsetquot [in hSet]
weqsetquottodirprod [in hSet]
weqstnprod [in stnfsets]
weqstnsum [in stnfsets]
weqstnsum2 [in stnfsets]
weqsubsetsplit [in uu0]
weqsubtypesdirprod [in hSet]
weqtoeqstn [in stnfsets]
weqtoforallpaths [in uu0]
weqtotal2asstor [in uu0]
weqtotal2overcoprod [in uu0]
weqtotal2overunit [in uu0]
weqtranspos [in uu0]
weqweqstnsn [in stnfsets]
Notation Index
other
_ + _ (addoperation_scope) [in algebra1]- _ (hz_scope) [in hz]
_ - _ (hz_scope) [in hz]
_ + _ (hz_scope) [in hz]
0 (hz_scope) [in hz]
_ * _ (multoperation_scope) [in algebra1]
_ * _ (rng_scope) [in algebra1]
0 (rng_scope) [in algebra1]
_ + _ (rng_scope) [in algebra1]
-1 (rng_scope) [in algebra1]
1 (rng_scope) [in algebra1]
_ * _ (twobinops_scope) [in algebra1]
_ + _ (twobinops_scope) [in algebra1]
Constructor Index
L
leF_O [in hnat]leF_S [in hnat]
T
tpair [in uuu]Abbreviation Index
C
coprod [in uuu]E
empty [in uuu]H
hinhprinv [in hProp]I
idpath [in uuu]ii1 [in uuu]
ii1fun [in uuu]
ii2 [in uuu]
ii2fun [in uuu]
isapropunit [in uu0]
isassocisob [in algebra1]
iscancellableisob [in algebra1]
iscommisob [in algebra1]
isdistrisob [in algebra1]
islcancellableisob [in algebra1]
isldistrisob [in algebra1]
isrcancellableisob [in algebra1]
isrdistrisob [in algebra1]
issurjtwooutof3c [in hSet]
P
paths [in uuu]U
UUU [in uuu]Inductive Index
L
leF [in hnat]Definition Index
A
abgr [in algebra1]abgrconstr [in algebra1]
abgrdirprod [in algebra1]
abgrfrac [in algebra1]
abgrfraccarrier [in algebra1]
abgrfracinv [in algebra1]
abgrfracinvint [in algebra1]
abgrhz [in hz]
abgrpair [in algebra1]
abgrquot [in algebra1]
abgrtoabmonoid [in algebra1]
abgrtogr [in algebra1]
abmonoid [in algebra1]
abmonoidconstr [in algebra1]
abmonoiddirprod [in algebra1]
abmonoidfrac [in algebra1]
abmonoidfracop [in algebra1]
abmonoidfracopint [in algebra1]
abmonoidpair [in algebra1]
abmonoidquot [in algebra1]
abmonoidtomonoid [in algebra1]
absvalhz [in hz]
absvalhzint [in hz]
addabgr [in algebra1]
addabgreqrel [in algebra1]
addabmonoidnat [in hnat]
addsubgr [in algebra1]
adjev [in uu0]
adjev2 [in uu0]
assocax [in algebra1]
assocax_is [in algebra1]
B
bandfmap [in uu0]bhfiber [in uu0]
binop [in algebra1]
binopeqrel [in algebra1]
binopeqrelabgrfrac [in algebra1]
binopeqrelabmonoidfrac [in algebra1]
binopeqrelpair [in algebra1]
binopfun [in algebra1]
binopfuncomp [in algebra1]
binopfunpair [in algebra1]
binophrel [in algebra1]
binophrelpair [in algebra1]
binopincltobinopfun [in algebra1]
binopiso [in algebra1]
binopisocomp [in algebra1]
binopisopair [in algebra1]
binopisotobinopmono [in algebra1]
binopmono [in algebra1]
binopmonocomp [in algebra1]
binopmonopair [in algebra1]
binoppo [in algebra1]
binoppopair [in algebra1]
binop1fun [in algebra1]
binop1iso [in algebra1]
binop1mono [in algebra1]
binop2fun [in algebra1]
binop2iso [in algebra1]
binop2mono [in algebra1]
boolascoprod [in uu0]
boolchoice [in uu0]
booleq [in uu0]
booleq [in hz]
boolset [in hSet]
boolsumfun [in uu0]
boolsumtocoprod [in uu0]
C
carrier [in hSet]carrierofasubabgr [in algebra1]
carrierofasubcommrng [in algebra1]
carrierofasubgr [in algebra1]
carrierofasubrng [in algebra1]
carrierofasubsetwithbinop [in algebra1]
carrierofpo [in hSet]
carrierofposet [in hSet]
carrierofposetmorphism [in hSet]
carrierofsubabmonoid [in algebra1]
carrierofsubmonoid [in algebra1]
carrierofsubsetwith2binop [in algebra1]
carrierpair [in hSet]
coconusf [in uu0]
coconusfromt [in uu0]
coconusfromtpair [in uu0]
coconusfromtpr21 [in uu0]
coconustot [in uu0]
coconustotpair [in uu0]
coconustotpr21 [in uu0]
commax [in algebra1]
commax_is [in algebra1]
commhfp [in uu0]
commrng [in algebra1]
commrngconstr [in algebra1]
commrngdirprod [in algebra1]
commrngfrac [in algebra1]
commrngfracinv1 [in algebra1]
commrngfracinv1int [in algebra1]
commrngfracl4 [in algebra1]
commrngfracop1 [in algebra1]
commrngfracop1int [in algebra1]
commrngfracop2 [in algebra1]
commrngfracop2int [in algebra1]
commrngfracunel1 [in algebra1]
commrngfracunel1int [in algebra1]
commrngfracunel2 [in algebra1]
commrngfracunel2int [in algebra1]
commrngop2axs [in algebra1]
commrngpair [in algebra1]
commrngquot [in algebra1]
commrngtorng [in algebra1]
commsqstr [in uu0]
commsqZtohfp [in uu0]
commsqZtohfphomot [in uu0]
commsqZtohfphomot' [in uu0]
compevmap [in hSet]
compfun [in hSet]
compfunpair [in hSet]
compl [in uu0]
complpair [in uu0]
complxstr [in uu0]
constr1 [in uu0]
coprodasstol [in uu0]
coprodasstor [in uu0]
coprodcomm [in uu0]
coprodf [in uu0]
coprodtobool [in uu0]
coprodtoboolsum [in uu0]
curry [in uu0]
cutonweq [in uu0]
D
ddualand [in uu0]deltap [in uu0]
di [in hnat]
dirprod [in uu0]
dirprodadj [in uu0]
dirprodf [in uu0]
dirprodpair [in uu0]
dirprodtosetquot [in hSet]
distraxs_is [in algebra1]
dneg [in uu0]
dneganddnegimpldneg [in uu0]
dnegf [in uu0]
dnegnegtoneg [in uu0]
dni [in stnfsets]
dnitocompl [in stnfsets]
d1 [in uu0]
d1g [in uu0]
d2 [in uu0]
d2g [in uu0]
d3g [in uu0]
E
eqax0 [in hSet]eqax1 [in hSet]
eqax2 [in hSet]
eqbhz [in hz]
eqbnat [in hnat]
eqbx [in uu0]
eqh [in hnat]
eqhtopaths [in hnat]
eqhz [in hz]
eqnat [in hnat]
eqrel [in hSet]
eqrelabgrfrac [in algebra1]
eqrelabmonoidfrac [in algebra1]
eqrelcommrngfrac [in algebra1]
eqrelconstr [in hSet]
eqreldirprod [in hSet]
eqrelpair [in hSet]
eqrelrefl [in hSet]
eqrelsymm [in hSet]
eqreltrans [in hSet]
eqset [in hSet]
eqweqmaphProp [in hProp]
etacor [in uu0]
ezmap [in uu0]
ezmaphf [in uu0]
ezmappr21 [in uu0]
ezmap1 [in uu0]
ezweq [in uu0]
ezweqg [in uu0]
ezweqhf [in uu0]
ezweqpr21 [in uu0]
ezweq1 [in uu0]
ezweq1g [in uu0]
ezweq1pr21 [in uu0]
ezweq2 [in uu0]
ezweq2g [in uu0]
ezweq3g [in uu0]
F
factorial [in hnat]falsetonegtrue [in uu0]
ffgg [in uu0]
fibseqg [in uu0]
fibseqhf [in uu0]
fibseqpr21 [in uu0]
fibseqstr [in uu0]
fibseqstrpair [in uu0]
fibseqstrtocomplxstr [in uu0]
fibseq1 [in uu0]
fibseq1g [in uu0]
fibseq2 [in uu0]
fibseq2g [in uu0]
fibseq3g [in uu0]
fincard [in finitesets]
finstruct [in finitesets]
finstructonbool [in finitesets]
finstructoncompl [in finitesets]
finstructoncontr [in finitesets]
finstructoncoprod [in finitesets]
finstructoncoprodwithunit [in finitesets]
finstructondecsubset [in finitesets]
finstructondirprod [in finitesets]
finstructonempty [in finitesets]
finstructonempty2 [in finitesets]
finstructonforall [in finitesets]
finstructonfun [in finitesets]
finstructonstn [in finitesets]
finstructontotal2 [in finitesets]
finstructonunit [in finitesets]
finstructonweq [in finitesets]
finstructweqb [in finitesets]
finstructweqf [in finitesets]
fintructpair [in finitesets]
foralltohfiber [in uu0]
foralltototal [in uu0]
foralltototaltoforall [in uu0]
fpmap [in uu0]
fromcoconusf [in uu0]
fromcompltodisjoint [in uu0]
fromcompltoii1x [in uu0]
fromcompltoii2y [in uu0]
fromdsubtypesdirprodcarrier [in hSet]
fromempty [in uu0]
fromtotal2overcoprod [in uu0]
fromtotal2overunit [in uu0]
funcomp [in uu0]
funextfun [in uu0]
funextsec [in uu0]
funfromcoprodtoprod [in uu0]
funtoprodtoprod [in uu0]
funtranspos [in uu0]
funtranspos0 [in uu0]
G
geh [in hnat]gehpo [in hnat]
gr [in algebra1]
grconstr [in algebra1]
grdirprod [in algebra1]
grinv [in algebra1]
grinv_is [in algebra1]
grlinvax [in algebra1]
grlinvax_is [in algebra1]
grpair [in algebra1]
grquot [in algebra1]
grrinvax [in algebra1]
grrinvax_is [in algebra1]
grtomonoid [in algebra1]
gth [in hnat]
H
hconj [in hProp]hdisj [in hProp]
hexists [in hProp]
hfalse [in hProp]
hffpmap2 [in uu0]
hfiber [in uu0]
hfiberfpmap [in uu0]
hfiberpair [in uu0]
hfiberpr21 [in uu0]
hfibersftogf [in uu0]
hfibersgftog [in uu0]
hfibersgtof' [in uu0]
hfibersg'tof [in uu0]
hfibertoforall [in uu0]
hfibertohfp [in uu0]
hfibertosec [in uu0]
hforall [in hProp]
hfp [in uu0]
hfpg [in uu0]
hfpg' [in uu0]
hfpoverX [in uu0]
hfpoverX' [in uu0]
hfptohfiber [in uu0]
hfsqstr [in uu0]
hfsqstrpair [in uu0]
hfsqstrtocommsqstr [in uu0]
himpl [in hProp]
hinhand [in hProp]
hinhfun [in hProp]
hinhfun2 [in hProp]
hinhimplinhdneg [in hProp]
hinhpr [in hProp]
hinhuniv [in hProp]
hinhunivcor1 [in hProp]
hinhuniv2 [in hProp]
hneg [in hProp]
homot [in uu0]
homotcoprodfcomp [in uu0]
homotcoprodfhomot [in uu0]
homotffggid [in uu0]
homotinvweqweq [in uu0]
homotinvweqweq0 [in uu0]
homotrecomplfcomp [in uu0]
homotrecomplfhomot [in uu0]
homotrecomplfidfun [in uu0]
homottranspost2t1t1t2 [in uu0]
homottranspos0t2t1t1t2 [in uu0]
homotweqinvweq [in uu0]
homotweqinvweqweq [in uu0]
homotweqoncomplcomp [in uu0]
hProp [in hProp]
hProppair [in hProp]
hProppr21 [in hProp]
hrel [in hSet]
hrelabgrfrac [in algebra1]
hrelabgrfrac' [in algebra1]
hrelabmonoidfrac [in algebra1]
hrelcommrngfrac0 [in algebra1]
hreldirprod [in hSet]
hrel0abmonoidfrac [in algebra1]
hSet [in hSet]
hSetpair [in hSet]
hsubtypes [in hSet]
htrue [in hProp]
hz [in hz]
hzminus [in hz]
hzplus [in hz]
hzsign [in hz]
hzzero [in hz]
I
idfun [in uu0]idweq [in uu0]
image [in hSet]
imagepair [in hSet]
incl [in uu0]
inclcomp [in algebra1]
inclcomp [in uu0]
inclpair [in uu0]
inhdnegand [in hProp]
inhdnegfun [in hProp]
inhdnegpr [in hProp]
inhdneguniv [in hProp]
invbinopiso [in algebra1]
invcutonweq [in uu0]
invezmaphf [in uu0]
invezmappr21 [in uu0]
invezmap1 [in uu0]
invimpl [in uu0]
invmap [in uu0]
invmaponpathsincl [in uu0]
invmaponpathsweq [in uu0]
invmaponpathsweqid [in uu0]
invmonoidiso [in algebra1]
invongrquot [in algebra1]
invrecompl [in uu0]
invstruct [in algebra1]
invtwobinopiso [in algebra1]
invweq [in uu0]
isabgroupop [in algebra1]
isabgroupopisob [in algebra1]
isabgroupopisof [in algebra1]
isabgroupoptoisabmonoidop [in algebra1]
isabmonoidop [in algebra1]
isabmonoidopisob [in algebra1]
isabmonoidopisof [in algebra1]
isaninvprop [in uu0]
isaposetmorphism [in hSet]
isaprop [in uu0]
isapropinclb [in uu0]
isapropisdecprop [in uu0]
isapropisincl [in uu0]
isaset [in uu0]
isassoc [in algebra1]
isbinopfun [in algebra1]
isbinophrel [in algebra1]
iscancellable [in algebra1]
ischoicebase [in hSet]
ischoicebase_uu1 [in hSet]
iscomm [in algebra1]
iscommop2_is [in algebra1]
iscommrng [in algebra1]
iscommrngops [in algebra1]
iscommrngopsisob [in algebra1]
iscommrngopsisof [in algebra1]
iscomprelfun [in hSet]
iscomprelfun2 [in hSet]
iscomprelrelfun [in hSet]
iscomprelrelfun2 [in hSet]
iscontr [in uu0]
iscontrpair [in uu0]
iscontrpr21 [in uu0]
iscontrsecoverempty [in uu0]
iscontrsecoverempty2 [in uu0]
iscoproj [in uu0]
isdeceq [in uu0]
isdeceqsetquot [in hSet]
isdecincl [in uu0]
isdecprop [in uu0]
isdistr [in algebra1]
isdistrmonob [in algebra1]
iseqclass [in hSet]
iseqclassconstr [in hSet]
iseqrel [in hSet]
iseqrelconstr [in hSet]
isfibseq [in uu0]
isfinite [in finitesets]
isfinitebool [in finitesets]
isfinitecompl [in finitesets]
isfinitecontr [in finitesets]
isfinitecoprod [in finitesets]
isfinitecoprodwithunit [in finitesets]
isfinitedecsubset [in finitesets]
isfinitedirprod [in finitesets]
isfiniteempty [in finitesets]
isfiniteempty2 [in finitesets]
isfiniteforall [in finitesets]
isfinitefun [in finitesets]
isfinitestn [in finitesets]
isfinitetotal2 [in finitesets]
isfiniteunit [in finitesets]
isfiniteweq [in finitesets]
isfiniteweqb [in finitesets]
isfiniteweqf [in finitesets]
isgrcarrier [in algebra1]
isgroupop [in algebra1]
isgroupopisob [in algebra1]
isgroupopisof [in algebra1]
isgroupoppair [in algebra1]
isgrquot [in algebra1]
ishfsq [in uu0]
ishinh [in hProp]
ishinh_UU [in hProp]
isincl [in uu0]
isinclpr21 [in uu0]
isinhdneg [in hProp]
isinv [in algebra1]
isinvertible [in algebra1]
isisolated [in uu0]
islcancellable [in algebra1]
isldistr [in algebra1]
islinv [in algebra1]
islinvertible [in algebra1]
islinvertibleisof [in algebra1]
islunit [in algebra1]
ismonoiddirprod [in algebra1]
ismonoidfun [in algebra1]
ismonoidop [in algebra1]
ismonoidopisob [in algebra1]
ismonoidopisof [in algebra1]
ismonoidquot [in algebra1]
isofhlevel [in uu0]
isofhlevelf [in uu0]
isofhlevelsninclb [in uu0]
isofnel [in finitesets]
isofnelbool [in finitesets]
isofnelcompl [in finitesets]
isofnelcontr [in finitesets]
isofnelcoprod [in finitesets]
isofnelcoprodwithunit [in finitesets]
isofnelempty [in finitesets]
isofnelempty2 [in finitesets]
isofnelondirprod [in finitesets]
isofnelonfun [in finitesets]
isofnelonweq [in finitesets]
isofnelstn [in finitesets]
isofnelunit [in finitesets]
isofnelweqb [in finitesets]
isofnelweqf [in finitesets]
isolated [in uu0]
isolatedpair [in uu0]
ispo [in hSet]
isrcancellable [in algebra1]
isrdistr [in algebra1]
isrefl [in hSet]
isrefldirprod [in hSet]
isreflpathshrel [in hSet]
isrigops [in algebra1]
isrinv [in algebra1]
isrinvertible [in algebra1]
isrinvertibleisof [in algebra1]
isrng [in algebra1]
isrngops [in algebra1]
isrngopsisob [in algebra1]
isrngopsisof [in algebra1]
isrunit [in algebra1]
issubgr [in algebra1]
issubmonoid [in algebra1]
issubrng [in algebra1]
issubsetwithbinop [in algebra1]
issubsetwith2binop [in algebra1]
issurjective [in hSet]
issymm [in hSet]
issymmdirprod [in hSet]
issymmpathshrel [in hSet]
istrans [in hSet]
istransdirprod [in hSet]
istranspathshrel [in hSet]
istwobinopfun [in algebra1]
isunit [in algebra1]
isunital [in algebra1]
isunitalisob [in algebra1]
isunitalisof [in algebra1]
isunitalpair [in algebra1]
isweq [in uu0]
isweqezmappr21 [in uu0]
isweqinvezmaphf [in uu0]
isweqtoempty [in uu0]
is2binophrel [in algebra1]
iteration [in uu0]
L
lastelement [in stnfsets]ldistrax_is [in algebra1]
le [in hnat]
leb [in hnat]
leh [in hnat]
lehpo [in hnat]
le_n [in hnat]
le_S [in hnat]
lth [in hnat]
lunax [in algebra1]
lunax_is [in algebra1]
M
maponcomplincl [in uu0]maponcomplweq [in uu0]
maponpaths [in uu0]
maponpathscomp0 [in uu0]
maponpathshomidinv [in uu0]
maponpathsinv0 [in uu0]
maponsec [in uu0]
maponsec1 [in uu0]
maponsec1l0 [in uu0]
minus1_is_l [in algebra1]
monoid [in algebra1]
monoidconstr [in algebra1]
monoiddirprod [in algebra1]
monoidfun [in algebra1]
monoidfuncomp [in algebra1]
monoidfunpair [in algebra1]
monoidfuntobinopfun [in algebra1]
monoidincltomonoidfun [in algebra1]
monoidiso [in algebra1]
monoidisopair [in algebra1]
monoidisotobinopiso [in algebra1]
monoidisotomonoidmono [in algebra1]
monoidmono [in algebra1]
monoidmonocomp [in algebra1]
monoidmonopair [in algebra1]
monoidmonotobinopmono [in algebra1]
monoidpair [in algebra1]
monoidquot [in algebra1]
multabmonoid [in algebra1]
multabmonoidnat [in hnat]
multmonoid [in algebra1]
multmonoideqrel [in algebra1]
multsubmonoid [in algebra1]
N
natdiv [in hnat]natdivrem [in hnat]
natnattohz [in hz]
natpower [in hnat]
natrem [in hnat]
natset [in hnat]
neg [in uu0]
negf [in uu0]
negimage [in uu0]
negimagepair [in uu0]
negstn0 [in stnfsets]
nelstruct [in finitesets]
nelstructonbool [in finitesets]
nelstructoncompl [in finitesets]
nelstructoncontr [in finitesets]
nelstructoncoprod [in finitesets]
nelstructoncoprodwithunit [in finitesets]
nelstructondirprod [in finitesets]
nelstructonempty [in finitesets]
nelstructonempty2 [in finitesets]
nelstructonforall [in finitesets]
nelstructonfun [in finitesets]
nelstructonstn [in finitesets]
nelstructontotal2 [in finitesets]
nelstructonunit [in finitesets]
nelstructonweq [in finitesets]
nelstructweqb [in finitesets]
nelstructweqf [in finitesets]
neqh [in hnat]
O
op [in algebra1]op1 [in algebra1]
op1axs_is [in algebra1]
op2 [in algebra1]
op2axs_is [in algebra1]
P
pathscomp0 [in uu0]pathscomp0rid [in uu0]
pathsdirprod [in uu0]
pathseqrel [in hSet]
pathshrel [in hSet]
pathsinv0 [in uu0]
pathsinv0inv0 [in uu0]
pathsinv0l [in uu0]
pathsinv0r [in uu0]
pathssec1 [in uu0]
pathssec2 [in uu0]
pathssec2id [in uu0]
pathssec3 [in uu0]
pathsspace [in uu0]
pathsspacetriple [in uu0]
pathsspace' [in uu0]
pathstoeqh [in hnat]
pathsweq1 [in uu0]
pathsweq1' [in uu0]
pathsweq3 [in uu0]
pathsweq4 [in uu0]
pi0 [in hSet]
pi0pr [in hSet]
po [in hSet]
popair [in hSet]
Poset [in hSet]
posetmorphism [in hSet]
posetmorphismpair [in hSet]
Posetpair [in hSet]
prabgrfrac [in algebra1]
prabmonoidfrac [in algebra1]
prcommrngfrac [in algebra1]
prodtofunfromcoprod [in uu0]
prodtofuntoprod [in uu0]
prodtosecovercoprod [in uu0]
prtoimage [in hSet]
pr21 [in uuu]
pr21binopeqrel [in algebra1]
pr21binopfun [in algebra1]
pr21binophrel [in algebra1]
pr21binopiso [in algebra1]
pr21binopmono [in algebra1]
pr21binoppo [in algebra1]
pr21carrier [in hSet]
pr21compl [in uu0]
pr21eqrel [in hSet]
pr21hSet [in hSet]
pr21image [in hSet]
pr21incl [in uu0]
pr21isabgroupop [in algebra1]
pr21isabmonoidop [in algebra1]
pr21iscommrngops [in algebra1]
pr21isgroupop [in algebra1]
pr21isolated [in uu0]
pr21monoid [in algebra1]
pr21monoidfun [in algebra1]
pr21monoidiso [in algebra1]
pr21monoidmono [in algebra1]
pr21rng [in algebra1]
pr21setquot [in hSet]
pr21setwithbinop [in algebra1]
pr21setwith2binop [in algebra1]
pr21submonoids [in algebra1]
pr21subrng [in algebra1]
pr21subsetswithbinop [in algebra1]
pr21subsetswith2binop [in algebra1]
pr21twobinopeqrel [in algebra1]
pr21twobinopfun [in algebra1]
pr21twobinophrel [in algebra1]
pr21twobinopiso [in algebra1]
pr21twobinopmono [in algebra1]
pr21twobinoppo [in algebra1]
pr21weq [in uu0]
pr22 [in uuu]
R
rdistrax_is [in algebra1]rdistrtocoprod [in uu0]
rdistrtoprod [in uu0]
recompl [in uu0]
recomplf [in uu0]
rng [in algebra1]
rngassoc1 [in algebra1]
rngassoc2 [in algebra1]
rngaxs [in algebra1]
rngcomm1 [in algebra1]
rngcomm2 [in algebra1]
rngconstr [in algebra1]
rngdirprod [in algebra1]
rngdistraxs [in algebra1]
rngeqrel [in algebra1]
rnginv1 [in algebra1]
rngldistrax [in algebra1]
rnglinvax1 [in algebra1]
rnglunax1 [in algebra1]
rnglunax2 [in algebra1]
rngminus1 [in algebra1]
rngminus1_is [in algebra1]
rngmultwithminus1 [in algebra1]
rngmultwithminus1_is [in algebra1]
rngmultx0 [in algebra1]
rngmultx0_is [in algebra1]
rngmult0x [in algebra1]
rngmult0x_is [in algebra1]
rngop1axs [in algebra1]
rngop2axs [in algebra1]
rngpair [in algebra1]
rngquot [in algebra1]
rngrdistrax [in algebra1]
rngrinvax1 [in algebra1]
rngrunax1 [in algebra1]
rngrunax2 [in algebra1]
rngunel1 [in algebra1]
rngunel2 [in algebra1]
runax [in algebra1]
runax_is [in algebra1]
S
secovercoprodtoprod [in uu0]sectohfiber [in uu0]
sectohfibertosec [in uu0]
setdirprod [in hSet]
setproperty [in hSet]
setquot [in hSet]
setquotbooleq [in hSet]
setquotbooleqint [in hSet]
setquotfun [in hSet]
setquotfuncomm [in hSet]
setquotfun2 [in hSet]
setquotincl [in hSet]
setquotinset [in hSet]
setquotpair [in hSet]
setquottodirprod [in hSet]
setquottosetquot2 [in hSet]
setquottouu0 [in hSet]
setquotuniv2 [in hSet]
setquot2 [in hSet]
setquot2pr [in hSet]
setquot2univ [in hSet]
setwithbinop [in algebra1]
setwithbinopdirprod [in algebra1]
setwithbinoppair [in algebra1]
setwithbinopquot [in algebra1]
setwithbinop1 [in algebra1]
setwithbinop2 [in algebra1]
setwith2binop [in algebra1]
setwith2binopdirprod [in algebra1]
setwith2binoppair [in algebra1]
setwith2binopquot [in algebra1]
stn [in stnfsets]
stnmtostnn [in stnfsets]
stnpair [in stnfsets]
stnprod [in stnfsets]
stnsum [in stnfsets]
stntonat [in stnfsets]
subabgrs [in algebra1]
subabmonoids [in algebra1]
subgrconstr [in algebra1]
subgrpair [in algebra1]
subgrs [in algebra1]
subgrstosubmonoids [in algebra1]
submonoidconstr [in algebra1]
submonoidpair [in algebra1]
submonoids [in algebra1]
submonoidstosubsetswithbinop [in algebra1]
subrngpair [in algebra1]
subrngs [in algebra1]
subrngtosubsetswith2binop [in algebra1]
subsetsplit [in uu0]
subsetsplitinv [in uu0]
subsetswithbinop [in algebra1]
subsetswithbinopconstr [in algebra1]
subsetswithbinoppair [in algebra1]
subsetswith2binop [in algebra1]
subsetswith2binopconstr [in algebra1]
subsetswith2binoppair [in algebra1]
subtypesdirprod [in hSet]
sumofmaps [in uu0]
T
termfun [in uu0]tococonusf [in uu0]
tocompltodisjoint [in uu0]
tocompltoii1x [in uu0]
tocompltoii2y [in uu0]
todneg [in uu0]
toforallpaths [in uu0]
tosecovertotal2 [in uu0]
tosecoverunit [in uu0]
tosubtypesdirprodcarrier [in hSet]
totalfun [in uu0]
totalsubmonoid [in algebra1]
totalsubsetwithbinop [in algebra1]
totalsubsetwith2binop [in algebra1]
totalsubtype [in hSet]
totaltoforall [in uu0]
totaltoforalltototal [in uu0]
tototal2overcoprod [in uu0]
tototal2overunit [in uu0]
tounit [in uu0]
tppr [in uu0]
transportb [in uu0]
transportf [in uu0]
transposcommsqstr [in uu0]
truetonegfalse [in uu0]
twobinopeqrel [in algebra1]
twobinopeqrelpair [in algebra1]
twobinopfun [in algebra1]
twobinopfuncomp [in algebra1]
twobinopfunpair [in algebra1]
twobinophrel [in algebra1]
twobinophrelpair [in algebra1]
twobinopincltotwobinopfun [in algebra1]
twobinopiso [in algebra1]
twobinopisocomp [in algebra1]
twobinopisopair [in algebra1]
twobinopisototwobinopmono [in algebra1]
twobinopmono [in algebra1]
twobinopmonocomp [in algebra1]
twobinopmonopair [in algebra1]
twobinoppo [in algebra1]
twobinoppopair [in algebra1]
U
unel [in algebra1]unel_is [in algebra1]
UU [in uu0]
UU0 [in hProp]
W
weq [in uu0]weqabgrfrac [in algebra1]
weqbandf [in uu0]
weqbfun [in uu0]
weqboolsumtocoprod [in uu0]
weqcomp [in uu0]
weqcontrcontr [in uu0]
weqcontrtounit [in uu0]
weqcoprodasstol [in uu0]
weqcoprodasstor [in uu0]
weqcoprodcomm [in uu0]
weqcoprodf [in uu0]
weqcoprodsplit [in uu0]
weqcoprodtoboolsum [in uu0]
weqcoproj [in uu0]
weqcutonweq [in uu0]
weqdirprodasstol [in uu0]
weqdirprodasstor [in uu0]
weqdirprodcomm [in uu0]
weqdirprodf [in uu0]
weqdnicompl [in stnfsets]
weqdnicoprod [in stnfsets]
weqeqhtopaths [in hnat]
weqeqweqhProp [in hProp]
weqeta [in uu0]
weqffun [in uu0]
weqfibtototal [in uu0]
weqforalltohfiber [in uu0]
weqforalltototal [in uu0]
weqfp [in uu0]
weqfromcoconusf [in uu0]
weqfunextsec [in uu0]
weqfunfromcontr [in uu0]
weqfunfromdirprod [in uu0]
weqfunfromtotal2 [in uu0]
weqfunfromunit [in uu0]
weqfuntototaltototal [in uu0]
weqgradth [in uu0]
weqhfibersgtof' [in uu0]
weqhfibersg'tof [in uu0]
weqhfibertoforall [in uu0]
weqhfptohfpoverX [in uu0]
weqhfptohfpoverX' [in uu0]
weqii1withneg [in uu0]
weqii2withneg [in uu0]
weqimplimpl [in uu0]
weqisolatedstntostn [in stnfsets]
weqleFtototalwithnat [in hnat]
weqletoleh [in hnat]
weqoncompl [in uu0]
weqonpaths [in uu0]
weqonpathsincl [in uu0]
weqonsecbase [in uu0]
weqonseqfibers [in uu0]
weqpair [in uu0]
weqpathsinv0 [in uu0]
weqpathsweqhProp [in hProp]
weqpr21 [in uu0]
weqrdistrtocoprod [in uu0]
weqrdistrtoprod [in uu0]
weqrecompl [in uu0]
weqrecomplf [in uu0]
weqsecovercontr [in uu0]
weqsecovercoprodtoprod [in uu0]
weqsecovertotal2 [in uu0]
weqsecoverunit [in uu0]
weqsetquotsurj [in hSet]
weqsetquotweq [in hSet]
weqstn0toempty [in stnfsets]
weqstn1tounit [in stnfsets]
weqstn2tobool [in stnfsets]
weqtococonusf [in uu0]
weqtocompltodisjoint [in uu0]
weqtodirprodwithunit [in uu0]
weqtoempty [in uu0]
weqtoempty2 [in uu0]
weqtoincl [in uu0]
weqtopathshProp [in hProp]
weqtotalsubtype [in hSet]
weqtotaltofib [in uu0]
weqtotaltoforall [in uu0]
weqtotal2asstol [in uu0]
weqtranspos0 [in uu0]
wequnittocontr [in uu0]
weqZtohfp [in uu0]
wittohexists [in hProp]
Axiom Index
E
etacorrection [in uu0]F
funextempty [in uu0]funextfunax [in uu0]
U
uahp [in hProp]Library Index
A
algebra1F
finitesetsH
hnathProp
hSet
hz
S
stnfsetsU
uuuuu0
| 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 | (1579 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 | (2 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 | (1 entry) |
| 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 | (642 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 | (13 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 | (3 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 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 | (1 entry) |
| 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 | (884 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (9 entries) |
This page has been generated by coqdoc