| 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 | (225 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 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 | (8 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (62 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 | (11 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 | (8 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 | (28 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (60 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 | (5 entries) |
Global Index
A
ACC [inductive, in Paradoxes.Logics]ACC [inductive, in Paradoxes.BuraliForti_ex]
ACC_inverse_image [lemma, in Paradoxes.Logics]
ACC_lemma [lemma, in Paradoxes.Logics]
ACC_nonreflexive [lemma, in Paradoxes.Logics]
ACC_intro [constructor, in Paradoxes.Logics]
ACC_emb [lemma, in Paradoxes.BuraliForti_ex]
ACC_irrefl [lemma, in Paradoxes.BuraliForti_ex]
ACC_intro [constructor, in Paradoxes.BuraliForti_ex]
ACC_emb [lemma, in Paradoxes.BuraliForti]
A0 [record, in Paradoxes.BuraliForti_ex]
A0 [record, in Paradoxes.BuraliForti]
A0 [definition, in Paradoxes.Reynolds1]
B
Bool [variable, in Paradoxes.Log_Rel1]BuraliForti [library]
BuraliForti_ex [library]
Burali_Forti [lemma, in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.Subsets.a [variable, in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.Subsets [section, in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.inj [variable, in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.i0 [variable, in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.A0 [variable, in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox [section, in Paradoxes.BuraliForti_ex]
Burali_Forti [lemma, in Paradoxes.BuraliForti]
Burali_Forti_Paradox.Subsets.a [variable, in Paradoxes.BuraliForti]
Burali_Forti_Paradox.Subsets [section, in Paradoxes.BuraliForti]
Burali_Forti_Paradox.inj [variable, in Paradoxes.BuraliForti]
Burali_Forti_Paradox.i0 [variable, in Paradoxes.BuraliForti]
Burali_Forti_Paradox.A0 [variable, in Paradoxes.BuraliForti]
Burali_Forti_Paradox [section, in Paradoxes.BuraliForti]
b2p [definition, in Paradoxes.Hurkens_Set]
C
cut [lemma, in Paradoxes.Log_Rel]D
define_on [definition, in Paradoxes.BuraliForti_ex]diaconescu [library]
dn [definition, in Paradoxes.Hurkens_Set]
dom [definition, in Paradoxes.BuraliForti_ex]
E
EM [lemma, in Paradoxes.diaconescu]emb [record, in Paradoxes.BuraliForti_ex]
emb [record, in Paradoxes.BuraliForti]
emb_morph [lemma, in Paradoxes.BuraliForti_ex]
emb_irrefl [lemma, in Paradoxes.BuraliForti_ex]
emb_trans [lemma, in Paradoxes.BuraliForti_ex]
emb_wit [projection, in Paradoxes.BuraliForti]
emb_trans [lemma, in Paradoxes.BuraliForti]
EM_set_inconsistency.EM_set_neg [variable, in Paradoxes.Hurkens_Set]
EM_set_inconsistency [section, in Paradoxes.Hurkens_Set]
EM_set_neg_inconsistency.EM_set_neg [variable, in Paradoxes.Hurkens_Set]
EM_set_neg_inconsistency [section, in Paradoxes.Hurkens_Set]
EM2 [lemma, in Paradoxes.diaconescu]
Eq [definition, in Paradoxes.Log_Rel1]
equiv [inductive, in Paradoxes.Log_Rel]
equiv [inductive, in Paradoxes.Log_Rel1]
EquivRel [definition, in Paradoxes.diaconescu]
equiv_intro [constructor, in Paradoxes.Log_Rel]
equiv_intro [constructor, in Paradoxes.Log_Rel1]
eqx [projection, in Paradoxes.BuraliForti_ex]
eqx [projection, in Paradoxes.BuraliForti]
eqy [projection, in Paradoxes.BuraliForti_ex]
eqy [projection, in Paradoxes.BuraliForti]
eq_bool_dec [lemma, in Paradoxes.diaconescu]
EXi [constructor, in Paradoxes.diaconescu]
exp [definition, in Paradoxes.Log_Rel]
exp [definition, in Paradoxes.Log_Rel1]
EXType [inductive, in Paradoxes.diaconescu]
E0 [definition, in Paradoxes.Reynolds1]
E1 [variable, in Paradoxes.Log_Rel1]
E2 [variable, in Paradoxes.Log_Rel1]
F
F [definition, in Paradoxes.BuraliForti_ex]f [projection, in Paradoxes.BuraliForti_ex]
F [definition, in Paradoxes.BuraliForti]
f [projection, in Paradoxes.BuraliForti]
fmorph [projection, in Paradoxes.BuraliForti_ex]
fmorph [projection, in Paradoxes.BuraliForti]
fstrict [projection, in Paradoxes.BuraliForti_ex]
fsub [definition, in Paradoxes.BuraliForti]
F_preserve_strictness [lemma, in Paradoxes.BuraliForti_ex]
F_morphism [lemma, in Paradoxes.BuraliForti_ex]
F_emb_strict_Omega [lemma, in Paradoxes.BuraliForti_ex]
F_Omega_neq [lemma, in Paradoxes.BuraliForti_ex]
F_emb_Omega [lemma, in Paradoxes.BuraliForti_ex]
F_morphism [lemma, in Paradoxes.BuraliForti]
F_emb_Omega [lemma, in Paradoxes.BuraliForti]
f0 [definition, in Paradoxes.Reynolds1]
F0 [definition, in Paradoxes.Reynolds1]
G
G0 [definition, in Paradoxes.Reynolds1]H
Hurkens_set_neg [lemma, in Paradoxes.Hurkens_Set]Hurkens_set_neg.p2p2 [variable, in Paradoxes.Hurkens_Set]
Hurkens_set_neg.p2p1 [variable, in Paradoxes.Hurkens_Set]
Hurkens_set_neg.b2p [variable, in Paradoxes.Hurkens_Set]
Hurkens_set_neg.p2b [variable, in Paradoxes.Hurkens_Set]
Hurkens_set_neg [section, in Paradoxes.Hurkens_Set]
Hurkens_Set [library]
I
i [constructor, in Paradoxes.BuraliForti_ex]I [definition, in Paradoxes.Hurkens_Set]
I [variable, in Paradoxes.Log_Rel1]
id_teta_intro [lemma, in Paradoxes.Reynolds1]
id_intro_teta [lemma, in Paradoxes.Reynolds1]
inclus [definition, in Paradoxes.Log_Rel]
inclus [definition, in Paradoxes.Log_Rel1]
induct [definition, in Paradoxes.Hurkens_Set]
inj [lemma, in Paradoxes.BuraliForti_ex]
inj [lemma, in Paradoxes.BuraliForti]
INTER [definition, in Paradoxes.Reynolds1]
inter [definition, in Paradoxes.Reynolds1]
intro [definition, in Paradoxes.Reynolds1]
Inverse_Image.f [variable, in Paradoxes.Logics]
Inverse_Image.R [variable, in Paradoxes.Logics]
Inverse_Image.B [variable, in Paradoxes.Logics]
Inverse_Image.A [variable, in Paradoxes.Logics]
Inverse_Image [section, in Paradoxes.Logics]
iter_A0 [definition, in Paradoxes.Reynolds1]
i0 [constructor, in Paradoxes.BuraliForti]
K
khi [definition, in Paradoxes.Reynolds1]L
large_emb [definition, in Paradoxes.BuraliForti_ex]le [definition, in Paradoxes.Hurkens_Set]
lemma [lemma, in Paradoxes.Hurkens_Set]
lemma_inter [lemma, in Paradoxes.Reynolds1]
lemma_teta [lemma, in Paradoxes.Reynolds1]
lemma1 [lemma, in Paradoxes.Reynolds1]
lemma2 [lemma, in Paradoxes.Hurkens_Set]
lemma3 [lemma, in Paradoxes.Reynolds1]
lemma4 [lemma, in Paradoxes.Reynolds1]
lemma5 [lemma, in Paradoxes.Reynolds1]
lemma6 [lemma, in Paradoxes.Reynolds1]
lemma7 [lemma, in Paradoxes.Reynolds1]
logical_relation [section, in Paradoxes.Log_Rel]
logical_relation [section, in Paradoxes.Log_Rel1]
Logics [library]
Log_Rel1 [library]
Log_Rel [library]
M
maj [projection, in Paradoxes.BuraliForti_ex]maj [projection, in Paradoxes.BuraliForti]
majd [projection, in Paradoxes.BuraliForti_ex]
majf [projection, in Paradoxes.BuraliForti_ex]
majf [projection, in Paradoxes.BuraliForti]
morphism [definition, in Paradoxes.BuraliForti_ex]
morphism [definition, in Paradoxes.BuraliForti]
morphism_restrict [lemma, in Paradoxes.BuraliForti_ex]
N
not_EM_set [lemma, in Paradoxes.Hurkens_Set]not_EM_set_neg [lemma, in Paradoxes.Hurkens_Set]
O
Omega [definition, in Paradoxes.BuraliForti_ex]Omega [lemma, in Paradoxes.Hurkens_Set]
Omega [definition, in Paradoxes.BuraliForti]
Omega_refl [lemma, in Paradoxes.BuraliForti_ex]
Omega_refl [lemma, in Paradoxes.BuraliForti]
P
paradox [section, in Paradoxes.Reynolds1]paradox.p [variable, in Paradoxes.Reynolds1]
per [inductive, in Paradoxes.Log_Rel]
per [inductive, in Paradoxes.Log_Rel1]
per_G0 [lemma, in Paradoxes.Reynolds1]
per_F0 [lemma, in Paradoxes.Reynolds1]
per_E0 [lemma, in Paradoxes.Reynolds1]
per_equiv [lemma, in Paradoxes.Log_Rel]
per_intro [constructor, in Paradoxes.Log_Rel]
per_Eq [lemma, in Paradoxes.Log_Rel1]
per_intro [constructor, in Paradoxes.Log_Rel1]
phi [definition, in Paradoxes.Reynolds1]
PHI [definition, in Paradoxes.Reynolds1]
phi2 [definition, in Paradoxes.Reynolds1]
power [definition, in Paradoxes.Log_Rel]
power [definition, in Paradoxes.Log_Rel1]
preserve_strictness [definition, in Paradoxes.BuraliForti_ex]
psi [definition, in Paradoxes.Reynolds1]
p2b [definition, in Paradoxes.Hurkens_Set]
p2p1 [lemma, in Paradoxes.Hurkens_Set]
p2p2 [lemma, in Paradoxes.Hurkens_Set]
R
rel [inductive, in Paradoxes.diaconescu]Rel [definition, in Paradoxes.Log_Rel]
Rel [definition, in Paradoxes.Log_Rel1]
relation [section, in Paradoxes.Log_Rel]
Relation [section, in Paradoxes.Log_Rel1]
rel_equiv [lemma, in Paradoxes.diaconescu]
rel_sym [lemma, in Paradoxes.diaconescu]
rel_trans [lemma, in Paradoxes.diaconescu]
rel' [definition, in Paradoxes.diaconescu]
rel2 [constructor, in Paradoxes.diaconescu]
restrict [definition, in Paradoxes.BuraliForti_ex]
Reynolds [lemma, in Paradoxes.Reynolds1]
Reynolds1 [library]
Rof [definition, in Paradoxes.Logics]
rrefl [constructor, in Paradoxes.diaconescu]
R0 [projection, in Paradoxes.BuraliForti_ex]
R0 [projection, in Paradoxes.BuraliForti]
R1 [projection, in Paradoxes.BuraliForti_ex]
R1 [projection, in Paradoxes.BuraliForti]
R2 [projection, in Paradoxes.BuraliForti_ex]
R2 [projection, in Paradoxes.BuraliForti]
S
sb [definition, in Paradoxes.Hurkens_Set]strict [definition, in Paradoxes.BuraliForti_ex]
sub [record, in Paradoxes.BuraliForti]
sym [definition, in Paradoxes.Log_Rel]
sym [definition, in Paradoxes.Log_Rel1]
sym_E0 [lemma, in Paradoxes.Reynolds1]
T
T [variable, in Paradoxes.Log_Rel1]Tchoice [definition, in Paradoxes.diaconescu]
Tchoice2 [definition, in Paradoxes.diaconescu]
teta [definition, in Paradoxes.Reynolds1]
trans [definition, in Paradoxes.Log_Rel]
trans [definition, in Paradoxes.Log_Rel1]
trans_E0 [lemma, in Paradoxes.Reynolds1]
TTDiaconescu [section, in Paradoxes.diaconescu]
TTDiaconescu.P [variable, in Paradoxes.diaconescu]
TTDiaconescu.TTCA [variable, in Paradoxes.diaconescu]
TTDiaconescu2 [section, in Paradoxes.diaconescu]
TTDiaconescu2.P [variable, in Paradoxes.diaconescu]
TTDiaconescu2.TTAC2 [variable, in Paradoxes.diaconescu]
U
U [definition, in Paradoxes.Hurkens_Set]u0 [definition, in Paradoxes.Reynolds1]
V
V [definition, in Paradoxes.Hurkens_Set]W
WF [definition, in Paradoxes.Logics]WF [definition, in Paradoxes.BuraliForti_ex]
WF [definition, in Paradoxes.Hurkens_Set]
WF_inverse_image [lemma, in Paradoxes.Logics]
WF_restrict [lemma, in Paradoxes.BuraliForti_ex]
WF_emb_strict [lemma, in Paradoxes.BuraliForti_ex]
WF_emb [lemma, in Paradoxes.BuraliForti_ex]
WF_emb [lemma, in Paradoxes.BuraliForti]
witness [projection, in Paradoxes.BuraliForti]
W2 [projection, in Paradoxes.BuraliForti_ex]
W2 [projection, in Paradoxes.BuraliForti]
X
X0 [projection, in Paradoxes.BuraliForti_ex]X0 [projection, in Paradoxes.BuraliForti]
x0 [definition, in Paradoxes.Reynolds1]
X1 [projection, in Paradoxes.BuraliForti]
X2 [projection, in Paradoxes.BuraliForti]
Variable Index
B
Bool [in Paradoxes.Log_Rel1]Burali_Forti_Paradox.Subsets.a [in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.inj [in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.i0 [in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.A0 [in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.Subsets.a [in Paradoxes.BuraliForti]
Burali_Forti_Paradox.inj [in Paradoxes.BuraliForti]
Burali_Forti_Paradox.i0 [in Paradoxes.BuraliForti]
Burali_Forti_Paradox.A0 [in Paradoxes.BuraliForti]
E
EM_set_inconsistency.EM_set_neg [in Paradoxes.Hurkens_Set]EM_set_neg_inconsistency.EM_set_neg [in Paradoxes.Hurkens_Set]
E1 [in Paradoxes.Log_Rel1]
E2 [in Paradoxes.Log_Rel1]
H
Hurkens_set_neg.p2p2 [in Paradoxes.Hurkens_Set]Hurkens_set_neg.p2p1 [in Paradoxes.Hurkens_Set]
Hurkens_set_neg.b2p [in Paradoxes.Hurkens_Set]
Hurkens_set_neg.p2b [in Paradoxes.Hurkens_Set]
I
I [in Paradoxes.Log_Rel1]Inverse_Image.f [in Paradoxes.Logics]
Inverse_Image.R [in Paradoxes.Logics]
Inverse_Image.B [in Paradoxes.Logics]
Inverse_Image.A [in Paradoxes.Logics]
P
paradox.p [in Paradoxes.Reynolds1]T
T [in Paradoxes.Log_Rel1]TTDiaconescu.P [in Paradoxes.diaconescu]
TTDiaconescu.TTCA [in Paradoxes.diaconescu]
TTDiaconescu2.P [in Paradoxes.diaconescu]
TTDiaconescu2.TTAC2 [in Paradoxes.diaconescu]
Library Index
B
BuraliFortiBuraliForti_ex
D
diaconescuH
Hurkens_SetL
LogicsLog_Rel1
Log_Rel
R
Reynolds1Lemma Index
A
ACC_inverse_image [in Paradoxes.Logics]ACC_lemma [in Paradoxes.Logics]
ACC_nonreflexive [in Paradoxes.Logics]
ACC_emb [in Paradoxes.BuraliForti_ex]
ACC_irrefl [in Paradoxes.BuraliForti_ex]
ACC_emb [in Paradoxes.BuraliForti]
B
Burali_Forti [in Paradoxes.BuraliForti_ex]Burali_Forti [in Paradoxes.BuraliForti]
C
cut [in Paradoxes.Log_Rel]E
EM [in Paradoxes.diaconescu]emb_morph [in Paradoxes.BuraliForti_ex]
emb_irrefl [in Paradoxes.BuraliForti_ex]
emb_trans [in Paradoxes.BuraliForti_ex]
emb_trans [in Paradoxes.BuraliForti]
EM2 [in Paradoxes.diaconescu]
eq_bool_dec [in Paradoxes.diaconescu]
F
F_preserve_strictness [in Paradoxes.BuraliForti_ex]F_morphism [in Paradoxes.BuraliForti_ex]
F_emb_strict_Omega [in Paradoxes.BuraliForti_ex]
F_Omega_neq [in Paradoxes.BuraliForti_ex]
F_emb_Omega [in Paradoxes.BuraliForti_ex]
F_morphism [in Paradoxes.BuraliForti]
F_emb_Omega [in Paradoxes.BuraliForti]
H
Hurkens_set_neg [in Paradoxes.Hurkens_Set]I
id_teta_intro [in Paradoxes.Reynolds1]id_intro_teta [in Paradoxes.Reynolds1]
inj [in Paradoxes.BuraliForti_ex]
inj [in Paradoxes.BuraliForti]
L
lemma [in Paradoxes.Hurkens_Set]lemma_inter [in Paradoxes.Reynolds1]
lemma_teta [in Paradoxes.Reynolds1]
lemma1 [in Paradoxes.Reynolds1]
lemma2 [in Paradoxes.Hurkens_Set]
lemma3 [in Paradoxes.Reynolds1]
lemma4 [in Paradoxes.Reynolds1]
lemma5 [in Paradoxes.Reynolds1]
lemma6 [in Paradoxes.Reynolds1]
lemma7 [in Paradoxes.Reynolds1]
M
morphism_restrict [in Paradoxes.BuraliForti_ex]N
not_EM_set [in Paradoxes.Hurkens_Set]not_EM_set_neg [in Paradoxes.Hurkens_Set]
O
Omega [in Paradoxes.Hurkens_Set]Omega_refl [in Paradoxes.BuraliForti_ex]
Omega_refl [in Paradoxes.BuraliForti]
P
per_G0 [in Paradoxes.Reynolds1]per_F0 [in Paradoxes.Reynolds1]
per_E0 [in Paradoxes.Reynolds1]
per_equiv [in Paradoxes.Log_Rel]
per_Eq [in Paradoxes.Log_Rel1]
p2p1 [in Paradoxes.Hurkens_Set]
p2p2 [in Paradoxes.Hurkens_Set]
R
rel_equiv [in Paradoxes.diaconescu]rel_sym [in Paradoxes.diaconescu]
rel_trans [in Paradoxes.diaconescu]
Reynolds [in Paradoxes.Reynolds1]
S
sym_E0 [in Paradoxes.Reynolds1]T
trans_E0 [in Paradoxes.Reynolds1]W
WF_inverse_image [in Paradoxes.Logics]WF_restrict [in Paradoxes.BuraliForti_ex]
WF_emb_strict [in Paradoxes.BuraliForti_ex]
WF_emb [in Paradoxes.BuraliForti_ex]
WF_emb [in Paradoxes.BuraliForti]
Constructor Index
A
ACC_intro [in Paradoxes.Logics]ACC_intro [in Paradoxes.BuraliForti_ex]
E
equiv_intro [in Paradoxes.Log_Rel]equiv_intro [in Paradoxes.Log_Rel1]
EXi [in Paradoxes.diaconescu]
I
i [in Paradoxes.BuraliForti_ex]i0 [in Paradoxes.BuraliForti]
P
per_intro [in Paradoxes.Log_Rel]per_intro [in Paradoxes.Log_Rel1]
R
rel2 [in Paradoxes.diaconescu]rrefl [in Paradoxes.diaconescu]
Inductive Index
A
ACC [in Paradoxes.Logics]ACC [in Paradoxes.BuraliForti_ex]
E
equiv [in Paradoxes.Log_Rel]equiv [in Paradoxes.Log_Rel1]
EXType [in Paradoxes.diaconescu]
P
per [in Paradoxes.Log_Rel]per [in Paradoxes.Log_Rel1]
R
rel [in Paradoxes.diaconescu]Projection Index
E
emb_wit [in Paradoxes.BuraliForti]eqx [in Paradoxes.BuraliForti_ex]
eqx [in Paradoxes.BuraliForti]
eqy [in Paradoxes.BuraliForti_ex]
eqy [in Paradoxes.BuraliForti]
F
f [in Paradoxes.BuraliForti_ex]f [in Paradoxes.BuraliForti]
fmorph [in Paradoxes.BuraliForti_ex]
fmorph [in Paradoxes.BuraliForti]
fstrict [in Paradoxes.BuraliForti_ex]
M
maj [in Paradoxes.BuraliForti_ex]maj [in Paradoxes.BuraliForti]
majd [in Paradoxes.BuraliForti_ex]
majf [in Paradoxes.BuraliForti_ex]
majf [in Paradoxes.BuraliForti]
R
R0 [in Paradoxes.BuraliForti_ex]R0 [in Paradoxes.BuraliForti]
R1 [in Paradoxes.BuraliForti_ex]
R1 [in Paradoxes.BuraliForti]
R2 [in Paradoxes.BuraliForti_ex]
R2 [in Paradoxes.BuraliForti]
W
witness [in Paradoxes.BuraliForti]W2 [in Paradoxes.BuraliForti_ex]
W2 [in Paradoxes.BuraliForti]
X
X0 [in Paradoxes.BuraliForti_ex]X0 [in Paradoxes.BuraliForti]
X1 [in Paradoxes.BuraliForti]
X2 [in Paradoxes.BuraliForti]
Section Index
B
Burali_Forti_Paradox.Subsets [in Paradoxes.BuraliForti_ex]Burali_Forti_Paradox [in Paradoxes.BuraliForti_ex]
Burali_Forti_Paradox.Subsets [in Paradoxes.BuraliForti]
Burali_Forti_Paradox [in Paradoxes.BuraliForti]
E
EM_set_inconsistency [in Paradoxes.Hurkens_Set]EM_set_neg_inconsistency [in Paradoxes.Hurkens_Set]
H
Hurkens_set_neg [in Paradoxes.Hurkens_Set]I
Inverse_Image [in Paradoxes.Logics]L
logical_relation [in Paradoxes.Log_Rel]logical_relation [in Paradoxes.Log_Rel1]
P
paradox [in Paradoxes.Reynolds1]R
relation [in Paradoxes.Log_Rel]Relation [in Paradoxes.Log_Rel1]
T
TTDiaconescu [in Paradoxes.diaconescu]TTDiaconescu2 [in Paradoxes.diaconescu]
Definition Index
A
A0 [in Paradoxes.Reynolds1]B
b2p [in Paradoxes.Hurkens_Set]D
define_on [in Paradoxes.BuraliForti_ex]dn [in Paradoxes.Hurkens_Set]
dom [in Paradoxes.BuraliForti_ex]
E
Eq [in Paradoxes.Log_Rel1]EquivRel [in Paradoxes.diaconescu]
exp [in Paradoxes.Log_Rel]
exp [in Paradoxes.Log_Rel1]
E0 [in Paradoxes.Reynolds1]
F
F [in Paradoxes.BuraliForti_ex]F [in Paradoxes.BuraliForti]
fsub [in Paradoxes.BuraliForti]
f0 [in Paradoxes.Reynolds1]
F0 [in Paradoxes.Reynolds1]
G
G0 [in Paradoxes.Reynolds1]I
I [in Paradoxes.Hurkens_Set]inclus [in Paradoxes.Log_Rel]
inclus [in Paradoxes.Log_Rel1]
induct [in Paradoxes.Hurkens_Set]
INTER [in Paradoxes.Reynolds1]
inter [in Paradoxes.Reynolds1]
intro [in Paradoxes.Reynolds1]
iter_A0 [in Paradoxes.Reynolds1]
K
khi [in Paradoxes.Reynolds1]L
large_emb [in Paradoxes.BuraliForti_ex]le [in Paradoxes.Hurkens_Set]
M
morphism [in Paradoxes.BuraliForti_ex]morphism [in Paradoxes.BuraliForti]
O
Omega [in Paradoxes.BuraliForti_ex]Omega [in Paradoxes.BuraliForti]
P
phi [in Paradoxes.Reynolds1]PHI [in Paradoxes.Reynolds1]
phi2 [in Paradoxes.Reynolds1]
power [in Paradoxes.Log_Rel]
power [in Paradoxes.Log_Rel1]
preserve_strictness [in Paradoxes.BuraliForti_ex]
psi [in Paradoxes.Reynolds1]
p2b [in Paradoxes.Hurkens_Set]
R
Rel [in Paradoxes.Log_Rel]Rel [in Paradoxes.Log_Rel1]
rel' [in Paradoxes.diaconescu]
restrict [in Paradoxes.BuraliForti_ex]
Rof [in Paradoxes.Logics]
S
sb [in Paradoxes.Hurkens_Set]strict [in Paradoxes.BuraliForti_ex]
sym [in Paradoxes.Log_Rel]
sym [in Paradoxes.Log_Rel1]
T
Tchoice [in Paradoxes.diaconescu]Tchoice2 [in Paradoxes.diaconescu]
teta [in Paradoxes.Reynolds1]
trans [in Paradoxes.Log_Rel]
trans [in Paradoxes.Log_Rel1]
U
U [in Paradoxes.Hurkens_Set]u0 [in Paradoxes.Reynolds1]
V
V [in Paradoxes.Hurkens_Set]W
WF [in Paradoxes.Logics]WF [in Paradoxes.BuraliForti_ex]
WF [in Paradoxes.Hurkens_Set]
X
x0 [in Paradoxes.Reynolds1]Record Index
A
A0 [in Paradoxes.BuraliForti_ex]A0 [in Paradoxes.BuraliForti]
E
emb [in Paradoxes.BuraliForti_ex]emb [in Paradoxes.BuraliForti]
S
sub [in Paradoxes.BuraliForti]| 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 | (225 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 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 | (8 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (62 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 | (11 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 | (8 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 | (28 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (60 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 | (5 entries) |