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

(1805 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

(10 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

(41 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

(969 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

(78 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

(69 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

(261 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

(11 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

(76 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

(235 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

(47 entries)

---

Global Index

A

abs [constructor, in lc.Slc]
abs [constructor, in lc.Slc]
abs [constructor, in lc.Slc]
ap [definition, in lc.Monad]
ap [definition, in lc.Monad]
app [constructor, in lc.Slc]
app [constructor, in lc.Slc]
app [constructor, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app_as_app1 [lemma, in lc.Slc]
app1 [definition, in lc.Slc]
app1 [definition, in lc.Slc]
app1 [definition, in lc.Slc]
app1 [definition, in lc.Slc]
app1_app [lemma, in lc.Slc]
app1_app [lemma, in lc.Slc]
app1_app [lemma, in lc.Slc]
app1_app [lemma, in lc.Slc]
app1_app [lemma, in lc.Slc]
app1_app [lemma, in lc.Slc]
app1_app [lemma, in lc.Slc]
app1_app [lemma, in lc.Slc]

B

bb_bb [lemma, in lc.Mod]
bb_bb [lemma, in lc.Mod]
bb_bb [lemma, in lc.Mod]
bb_bb [lemma, in lc.Mod]
bb_bb [lemma, in lc.Mod]
Beta [inductive, in lc.Slc]
Beta [inductive, in lc.Slc]
Beta [inductive, in lc.Slc]
Beta [inductive, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
beta_intro [constructor, in lc.Slc]
beta_intro_alt [lemma, in lc.Slc]
bind [projection, in lc.Monad]
bind [projection, in lc.Monad]
bind [projection, in lc.Monad]
bind [projection, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_unit [projection, in lc.Monad]
bind_unit [projection, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_unit [projection, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_map [lemma, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_unit [projection, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_unit [projection, in lc.Monad]
bind_map [lemma, in lc.Monad]
bind_map [lemma, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_map [lemma, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_map [lemma, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_map [lemma, in lc.Monad]
bind_unit [projection, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_bind [projection, in lc.Monad]
bind_unit [projection, in lc.Monad]
bind_map [lemma, in lc.Monad]
bind_unit [projection, in lc.Monad]
bind_map [lemma, in lc.Monad]
bind_congr [lemma, in lc.Monad]
bind_unit [projection, in lc.Monad]
bT_bT [lemma, in lc.Derived_Mod]
bT_bT [lemma, in lc.Derived_Mod]
bT_bT [lemma, in lc.Derived_Mod]
bT_bT [lemma, in lc.Derived_Mod]
bT_bT [lemma, in lc.Derived_Mod]

C

class [axiom, in lc.Quot]
class [axiom, in lc.Quot]
class [axiom, in lc.Quot]
class [axiom, in lc.Quot]
class [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_eq [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
class_eq [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_eq [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_eq [axiom, in lc.Quot]
class_ind [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
class_eq [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
class_eq [axiom, in lc.Quot]
class_eq [axiom, in lc.Quot]
class_eq [axiom, in lc.Quot]
class_rel [axiom, in lc.Quot]
comm [definition, in lc.Slc]
comm [definition, in lc.Slc]
comm [definition, in lc.Slc]
comm [definition, in lc.Slc]
comm_var [lemma, in lc.Slc]
comm_var [lemma, in lc.Slc]
comm_var [lemma, in lc.Slc]
comm_var [lemma, in lc.Slc]
comm_var [lemma, in lc.Slc]
comm_var [lemma, in lc.Slc]
comm_var [lemma, in lc.Slc]
comm_var [lemma, in lc.Slc]

D

default [definition, in lc.Misc]
default [definition, in lc.Misc]
default [definition, in lc.Misc]
default [definition, in lc.Misc]
default [definition, in lc.Misc]
default [definition, in lc.Misc]
default [definition, in lc.Misc]
Derived_Mod.Inc [section, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
Derived_Mod.M [variable, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod.P [variable, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
Derived_Mod.Def [section, in lc.Derived_Mod]
Derived_Mod.Def.bT [variable, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod.Inc.i [variable, in lc.Derived_Mod]
Derived_Mod.Def.T [variable, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
Derived_Mod.Inc [section, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
Derived_Mod.Def [section, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
Derived_Mod.Inc [section, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
Derived_Mod.Def [section, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod.Def.bT [variable, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
derived_inc [definition, in lc.Derived_Mod]
Derived_Mod [section, in lc.Derived_Mod]
Derived_Mod [definition, in lc.Derived_Mod]
Derived_Mod [library]

E

Eqv [record, in lc.Quot]
Eqv [record, in lc.Quot]
Eqv [record, in lc.Quot]
eqv_rfl [projection, in lc.Quot]
eqv_trs [projection, in lc.Quot]
eqv_rfl [projection, in lc.Quot]
eqv_rfl [projection, in lc.Quot]
eqv_sym [projection, in lc.Quot]
eqv_rfl [projection, in lc.Quot]
eqv_data [projection, in lc.Quot]
eqv_data [projection, in lc.Quot]
eqv_sym [projection, in lc.Quot]
eqv_data [projection, in lc.Quot]
eqv_sym [projection, in lc.Quot]
eqv_trs [projection, in lc.Quot]
eqv_sym [projection, in lc.Quot]
eqv_sym [projection, in lc.Quot]
eqv_data [projection, in lc.Quot]
eqv_trs [projection, in lc.Quot]
eqv_data [projection, in lc.Quot]
eqv_trs [projection, in lc.Quot]
eqv_trs [projection, in lc.Quot]
eqv_data [projection, in lc.Quot]
eqv_sym [projection, in lc.Quot]
eqv_trs [projection, in lc.Quot]
eqv_sym [projection, in lc.Quot]
eqv_data [projection, in lc.Quot]
eqv_trs [projection, in lc.Quot]
eqv_rfl [projection, in lc.Quot]
eqv_rfl [projection, in lc.Quot]
eqv_rfl [projection, in lc.Quot]
eqv_data [projection, in lc.Quot]
eq_eqv [lemma, in lc.Quot]
eq_eqv [lemma, in lc.Quot]
eq_eqv [lemma, in lc.Quot]
eq_eqv [lemma, in lc.Quot]
eq_eqv [lemma, in lc.Quot]
eq_eqv [lemma, in lc.Quot]
eta_fct [lemma, in lc.Slc]
eta_fct [lemma, in lc.Slc]
eta_fct [lemma, in lc.Slc]
eta_fct [lemma, in lc.Slc]
eta_fct [lemma, in lc.Slc]
eta_fct [lemma, in lc.Slc]
eta_fct [lemma, in lc.Slc]
ExpMonad [record, in lc.Derived_Mod]
ExpMonad [record, in lc.Derived_Mod]
ExpMonad [record, in lc.Derived_Mod]
ExpMonad [record, in lc.Derived_Mod]
ExpMonad [record, in lc.Derived_Mod]
ExpMonad [record, in lc.Derived_Mod]
ExpMonad [record, in lc.Derived_Mod]
ExpMonad [record, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
expmonad_hom_abs [projection, in lc.Derived_Mod]
ExpMonad_Hom [record, in lc.Derived_Mod]
expmonad_hom_app [projection, in lc.Derived_Mod]
expmonad_hom [projection, in lc.Derived_Mod]
exp_abs [projection, in lc.Derived_Mod]
exp_eta [projection, in lc.Derived_Mod]
exp_eta [projection, in lc.Derived_Mod]
exp_beta [projection, in lc.Derived_Mod]
exp_beta [projection, in lc.Derived_Mod]
exp_abs [projection, in lc.Derived_Mod]
exp_app [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_beta [projection, in lc.Derived_Mod]
exp_abs [projection, in lc.Derived_Mod]
exp_app [projection, in lc.Derived_Mod]
exp_abs [projection, in lc.Derived_Mod]
exp_beta [projection, in lc.Derived_Mod]
exp_beta [projection, in lc.Derived_Mod]
exp_eta [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_app [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_beta [projection, in lc.Derived_Mod]
exp_eta [projection, in lc.Derived_Mod]
exp_app [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_abs [projection, in lc.Derived_Mod]
exp_eta [projection, in lc.Derived_Mod]
exp_beta [projection, in lc.Derived_Mod]
exp_app [projection, in lc.Derived_Mod]
exp_app [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_eta [projection, in lc.Derived_Mod]
exp_abs [projection, in lc.Derived_Mod]
exp_eta [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_beta [projection, in lc.Derived_Mod]
exp_monad [projection, in lc.Derived_Mod]
exp_app [projection, in lc.Derived_Mod]
exp_abs [projection, in lc.Derived_Mod]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
extensionality [axiom, in lc.Extensionality]
Extensionality [library]

F

factor [axiom, in lc.Quot]
factor [axiom, in lc.Quot]
factor [axiom, in lc.Quot]
factor [axiom, in lc.Quot]
factor [axiom, in lc.Quot]
factor [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize [axiom, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize1 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factorize2 [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor_extens [lemma, in lc.Quot]
factor1 [definition, in lc.Quot]
factor1 [definition, in lc.Quot]
Factor1 [section, in lc.Quot]
Factor1 [section, in lc.Quot]
Factor1 [section, in lc.Quot]
Factor1 [section, in lc.Quot]
factor1 [definition, in lc.Quot]
factor1 [definition, in lc.Quot]
factor1 [definition, in lc.Quot]
factor1 [definition, in lc.Quot]
Factor1 [section, in lc.Quot]
Factor1 [section, in lc.Quot]
factor1 [definition, in lc.Quot]
Factor1 [section, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
factor1_extens [lemma, in lc.Quot]
Factor1.f [variable, in lc.Quot]
Factor1.Hf [variable, in lc.Quot]
Factor1.Hf [variable, in lc.Quot]
Factor1.rX [variable, in lc.Quot]
Factor1.rX [variable, in lc.Quot]
Factor1.rY [variable, in lc.Quot]
Factor1.rY [variable, in lc.Quot]
Factor1.X [variable, in lc.Quot]
Factor1.Y [variable, in lc.Quot]
factor2 [definition, in lc.Quot]
factor2 [definition, in lc.Quot]
Factor2 [section, in lc.Quot]
factor2 [definition, in lc.Quot]
Factor2 [section, in lc.Quot]
factor2 [definition, in lc.Quot]
factor2 [definition, in lc.Quot]
factor2 [definition, in lc.Quot]
Factor2 [section, in lc.Quot]
Factor2 [section, in lc.Quot]
Factor2 [section, in lc.Quot]
Factor2 [section, in lc.Quot]
Factor2 [section, in lc.Quot]
factor2 [definition, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
factor2_extens [lemma, in lc.Quot]
Factor2.f [variable, in lc.Quot]
Factor2.h [variable, in lc.Quot]
Factor2.Hf [variable, in lc.Quot]
Factor2.Hf [variable, in lc.Quot]
Factor2.rX [variable, in lc.Quot]
Factor2.rX [variable, in lc.Quot]
Factor2.rY [variable, in lc.Quot]
Factor2.rY [variable, in lc.Quot]
Factor2.rZ [variable, in lc.Quot]
Factor2.rZ [variable, in lc.Quot]
Factor2.X [variable, in lc.Quot]
Factor2.Y [variable, in lc.Quot]
Factor2.Z [variable, in lc.Quot]
fct [definition, in lc.Slc]
fct [definition, in lc.Slc]
fct [definition, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_app1 [lemma, in lc.Slc]
fct_id [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_id [lemma, in lc.Slc]
fct_fct [lemma, in lc.Slc]
fct_fct [lemma, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_fct [lemma, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_fct [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_fct [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_id [lemma, in lc.Slc]
fct_id [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_app1 [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_app1 [lemma, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_app1 [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_app1 [lemma, in lc.Slc]
fct_fct [lemma, in lc.Slc]
fct_fct [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_id [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_app1 [lemma, in lc.Slc]
fct_app1 [lemma, in lc.Slc]
fct_fun_cong [lemma, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_shift [lemma, in lc.Slc]
fct_app1 [lemma, in lc.Slc]
fct_id [lemma, in lc.Slc]
feqv [definition, in lc.Quot]
feqv [definition, in lc.Quot]
feqv [definition, in lc.Quot]
feqv [definition, in lc.Quot]
frel [definition, in lc.Quot]
frel [definition, in lc.Quot]
frel [definition, in lc.Quot]
frel [definition, in lc.Quot]

I

i_hom [lemma, in lc.Derived_Mod]
i_hom [lemma, in lc.Derived_Mod]
i_hom [lemma, in lc.Derived_Mod]
i_hom [lemma, in lc.Derived_Mod]
i_hom [lemma, in lc.Derived_Mod]

J

join [definition, in lc.Monad]
join [definition, in lc.Monad]
join [definition, in lc.Monad]
join [definition, in lc.Monad]
join_join [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_join [lemma, in lc.Monad]
join_join [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_map [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_map [lemma, in lc.Monad]
join_map [lemma, in lc.Monad]
join_map [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_map [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_join [lemma, in lc.Monad]
join_join [lemma, in lc.Monad]
join_join [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_map [lemma, in lc.Monad]
join_join [lemma, in lc.Monad]
join_join [lemma, in lc.Monad]
join_map [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_map [lemma, in lc.Monad]
join_unit [lemma, in lc.Monad]
join_join [lemma, in lc.Monad]

L

Lc [section, in lc.Lc]
lc [definition, in lc.Lc]
lc [definition, in lc.Lc]
Lc [section, in lc.Lc]
Lc [library]
lcr [inductive, in lc.Slc]
lcr [inductive, in lc.Slc]
lcr [inductive, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_eq [lemma, in lc.Slc]
lcr_app [constructor, in lc.Slc]
lcr_fct [lemma, in lc.Slc]
lcr_var [constructor, in lc.Slc]
lcr_sym [constructor, in lc.Slc]
lcr_app [constructor, in lc.Slc]
lcr_trs [constructor, in lc.Slc]
lcr_sym [constructor, in lc.Slc]
lcr_abs [constructor, in lc.Slc]
lcr_eta [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_var [constructor, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_eta [constructor, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_sym [constructor, in lc.Slc]
lcr_abs [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_sym [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_app1 [lemma, in lc.Slc]
lcr_eq [lemma, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_app1 [lemma, in lc.Slc]
lcr_var [constructor, in lc.Slc]
lcr_var [constructor, in lc.Slc]
lcr_rfl [lemma, in lc.Slc]
lcr_beta [constructor, in lc.Slc]
lcr_eta [constructor, in lc.Slc]
lcr_rfl [lemma, in lc.Slc]
lcr_fct [lemma, in lc.Slc]
lcr_eq [lemma, in lc.Slc]
lcr_fct [lemma, in lc.Slc]
lcr_bind [lemma, in lc.Slc]
lcr_app1 [lemma, in lc.Slc]
lcr_app1 [lemma, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_abs [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_abs [constructor, in lc.Slc]
lcr_bind [lemma, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_app [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_beta [constructor, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_bind [lemma, in lc.Slc]
lcr_eta [constructor, in lc.Slc]
lcr_bind [lemma, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_trs [constructor, in lc.Slc]
lcr_eq [lemma, in lc.Slc]
lcr_app1 [lemma, in lc.Slc]
lcr_eta [constructor, in lc.Slc]
lcr_eq [lemma, in lc.Slc]
lcr_bind [lemma, in lc.Slc]
lcr_eta [constructor, in lc.Slc]
lcr_beta [constructor, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_fct [lemma, in lc.Slc]
lcr_rfl [lemma, in lc.Slc]
lcr_var [constructor, in lc.Slc]
lcr_var [constructor, in lc.Slc]
lcr_bind [lemma, in lc.Slc]
lcr_var [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_eq [lemma, in lc.Slc]
lcr_beta [constructor, in lc.Slc]
lcr_trs [constructor, in lc.Slc]
lcr_abs [constructor, in lc.Slc]
lcr_abs [constructor, in lc.Slc]
lcr_trs [constructor, in lc.Slc]
lcr_bind [lemma, in lc.Slc]
lcr_fct [lemma, in lc.Slc]
lcr_trs [constructor, in lc.Slc]
lcr_eta [constructor, in lc.Slc]
lcr_rfl [lemma, in lc.Slc]
lcr_app [constructor, in lc.Slc]
lcr_trs [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_app1 [lemma, in lc.Slc]
lcr_sym [constructor, in lc.Slc]
lcr_app [constructor, in lc.Slc]
lcr_beta [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_beta [constructor, in lc.Slc]
lcr_rfl [lemma, in lc.Slc]
lcr_fct [lemma, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_trs [constructor, in lc.Slc]
lcr_beta [constructor, in lc.Slc]
lcr_abs [constructor, in lc.Slc]
lcr_app1 [lemma, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_rfl [lemma, in lc.Slc]
lcr_beta [constructor, in lc.Slc]
lcr_app1 [lemma, in lc.Slc]
lcr_sym [constructor, in lc.Slc]
lcr_bind_fun [lemma, in lc.Slc]
lcr_bind [lemma, in lc.Slc]
lcr_app [constructor, in lc.Slc]
lcr_app [constructor, in lc.Slc]
lcr_sym [constructor, in lc.Slc]
lcr_rfl [lemma, in lc.Slc]
lcr_bind_arg [lemma, in lc.Slc]
lcr_fct [lemma, in lc.Slc]
lc_bind [definition, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_class [definition, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_app [definition, in lc.Lc]
lc_eta [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_app [definition, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_var [definition, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_abs [definition, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_class [definition, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_eta [lemma, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_fct [definition, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_eta [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_app1 [definition, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_eta [lemma, in lc.Lc]
lc_class [definition, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_var [definition, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_fct [definition, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_bind [definition, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_app [definition, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_beta [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_app [definition, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_app1 [definition, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_bind [definition, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_beta [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_abs [definition, in lc.Lc]
lc_fct [definition, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_comm [definition, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_fct [definition, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_bind [definition, in lc.Lc]
lc_app1 [definition, in lc.Lc]
lc_eta [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_class [definition, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_comm [definition, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_var [definition, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_var [definition, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_app1 [definition, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_app [definition, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_fct [definition, in lc.Lc]
lc_beta [lemma, in lc.Lc]
lc_beta [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_class [definition, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_comm [definition, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_bind [definition, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_class [definition, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_abs [definition, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_app [definition, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_comm [definition, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_fct [definition, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_bind [definition, in lc.Lc]
lc_abs [definition, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_factor1 [definition, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_class [definition, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_comm [definition, in lc.Lc]
lc_app1 [definition, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_factor2 [definition, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_abs [definition, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_var [definition, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_eta [lemma, in lc.Lc]
lc_factorize [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_var_bind [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_factor_cong [lemma, in lc.Lc]
lc_app_factorize [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_bind_assoc [lemma, in lc.Lc]
lc_var [definition, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_comm [definition, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_abs_factorize [lemma, in lc.Lc]
lc_bind_fix_fun_cong [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_app1_factorize [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_abs [definition, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_factorize2 [lemma, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_beta [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_bind_fix_factorize [lemma, in lc.Lc]
lc_app1 [definition, in lc.Lc]
lc_beta [lemma, in lc.Lc]
lc_bind [definition, in lc.Lc]
lc_class [definition, in lc.Lc]
lc_fun_lift [lemma, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_bind_factorize [lemma, in lc.Lc]
lc_bind_var [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_factor [definition, in lc.Lc]
lc_bind_fix [definition, in lc.Lc]
lc_factorize1 [lemma, in lc.Lc]
lc_fct_factorize [lemma, in lc.Lc]
lc_class_eq [lemma, in lc.Lc]
lc_bind_fix_wd [lemma, in lc.Lc]
lc_app1 [definition, in lc.Lc]
lc_bind_fun_cong [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_bind_abs [lemma, in lc.Lc]
lc_beta [lemma, in lc.Lc]
lc_comm [definition, in lc.Lc]
lc_class_rel [lemma, in lc.Lc]
lc_bind_app1 [lemma, in lc.Lc]
lc_fct_as_bind [lemma, in lc.Lc]
lc_class_surj [lemma, in lc.Lc]
Lc.r [variable, in lc.Lc]
/ _ [notation, in lc.Lc]
lift [definition, in lc.Monad]
lift [definition, in lc.Monad]
lift [definition, in lc.Monad]
lift [definition, in lc.Monad]
lift_fun [lemma, in lc.Quot]
lift_fun [lemma, in lc.Quot]
lift_fun [lemma, in lc.Quot]
lift_fun [lemma, in lc.Quot]
lift_fun [lemma, in lc.Quot]
lift_fun [lemma, in lc.Quot]
lift_fun [lemma, in lc.Quot]
lift_fun [lemma, in lc.Quot]
lift2 [definition, in lc.Monad]
lift2 [definition, in lc.Monad]
lift2 [definition, in lc.Monad]
lift2 [definition, in lc.Monad]
lift2 [definition, in lc.Monad]
lift3 [definition, in lc.Monad]
lift3 [definition, in lc.Monad]
lift3 [definition, in lc.Monad]
lift3 [definition, in lc.Monad]
lift3 [definition, in lc.Monad]

M

map [definition, in lc.Monad]
map [definition, in lc.Monad]
map [definition, in lc.Monad]
map_bind [lemma, in lc.Monad]
map_bind [lemma, in lc.Monad]
map_map [lemma, in lc.Monad]
map_unit [lemma, in lc.Monad]
map_id [lemma, in lc.Monad]
map_map [lemma, in lc.Monad]
map_unit [lemma, in lc.Monad]
map_map [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_unit [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_unit [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_map [lemma, in lc.Monad]
map_bind [lemma, in lc.Monad]
map_id [lemma, in lc.Monad]
map_id [lemma, in lc.Monad]
map_unit [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_id [lemma, in lc.Monad]
map_id [lemma, in lc.Monad]
map_unit [lemma, in lc.Monad]
map_unit [lemma, in lc.Monad]
map_bind [lemma, in lc.Monad]
map_bind [lemma, in lc.Monad]
map_unit [lemma, in lc.Monad]
map_map [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_id [lemma, in lc.Monad]
map_map [lemma, in lc.Monad]
map_map [lemma, in lc.Monad]
map_bind [lemma, in lc.Monad]
map_congr [lemma, in lc.Monad]
map_bind [lemma, in lc.Monad]
map_bind [lemma, in lc.Monad]
mbind [projection, in lc.Mod]
mbind [projection, in lc.Mod]
mbind [projection, in lc.Mod]
mbind [projection, in lc.Mod]
mbind [projection, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_congr [lemma, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
mbind_mmap [lemma, in lc.Mod]
mbind_mbind [projection, in lc.Mod]
Misc [library]
mlift [definition, in lc.Mod]
mlift [definition, in lc.Mod]
mlift [definition, in lc.Mod]
mlift [definition, in lc.Mod]
mlift [definition, in lc.Mod]
mlift2 [definition, in lc.Mod]
mlift2 [definition, in lc.Mod]
mlift2 [definition, in lc.Mod]
mlift2 [definition, in lc.Mod]
mlift2 [definition, in lc.Mod]
mlift2 [definition, in lc.Mod]
mmap [definition, in lc.Mod]
mmap [definition, in lc.Mod]
mmap [definition, in lc.Mod]
mmap [definition, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
mmap_mbind [lemma, in lc.Mod]
mmap_mmap [lemma, in lc.Mod]
Mod [record, in lc.Mod]
Mod [record, in lc.Mod]
Mod [record, in lc.Mod]
Mod [library]
Mod_Hom [record, in lc.Mod]
Mod_Facts [section, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
Mod_Facts [section, in lc.Mod]
mod_carrier [projection, in lc.Mod]
Mod_Hom [record, in lc.Mod]
Mod_Hom [record, in lc.Mod]
mod_carrier [projection, in lc.Mod]
mod_carrier [projection, in lc.Mod]
Mod_Facts [section, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
Mod_Facts.P [variable, in lc.Mod]
Mod_Hom [record, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
Mod_Facts [section, in lc.Mod]
Mod_Facts [section, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
Mod_Facts [section, in lc.Mod]
Mod_Hom [record, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_carrier [projection, in lc.Mod]
Mod_Facts [section, in lc.Mod]
Mod_Hom [record, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
Mod_Hom [record, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_carrier [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_hom_carrier [projection, in lc.Mod]
Mod_Facts [section, in lc.Mod]
mod_carrier [projection, in lc.Mod]
Mod_Facts [section, in lc.Mod]
mod_hom_mbind [projection, in lc.Mod]
mod_carrier [projection, in lc.Mod]
mod_carrier [projection, in lc.Mod]
Mod_Facts.M [variable, in lc.Mod]
Monad [record, in lc.Monad]
Monad [record, in lc.Monad]
Monad [record, in lc.Monad]
Monad [record, in lc.Monad]
Monad [record, in lc.Monad]
Monad [library]
monad_hom_bind [projection, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
Monad_Hom.P [variable, in lc.Monad]
Monad_Hom [record, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
Monad_Hom [section, in lc.Monad]
Monad_Facts [section, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
Monad_Facts [section, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
Monad_Hom.Facts [section, in lc.Monad]
Monad_Hom [section, in lc.Monad]
monad_carrier [projection, in lc.Monad]
Monad_Hom [record, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_carrier [projection, in lc.Monad]
Monad_Hom.Facts [section, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_hom [projection, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
Monad_Facts [section, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_carrier [projection, in lc.Monad]
Monad_Hom [record, in lc.Monad]
Monad_Hom.Facts.h [variable, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
Monad_Facts [section, in lc.Monad]
Monad_Facts.P [variable, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
Monad_Facts [section, in lc.Monad]
monad_hom [projection, in lc.Monad]
Monad_Hom.Facts [section, in lc.Monad]
Monad_Facts [section, in lc.Monad]
Monad_Hom [record, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_hom [projection, in lc.Monad]
monad_carrier [projection, in lc.Monad]
Monad_Facts [section, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_carrier [projection, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
monad_carrier [projection, in lc.Monad]
monad_hom [projection, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
Monad_Hom.Facts [section, in lc.Monad]
Monad_Hom [section, in lc.Monad]
monad_hom [projection, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
monad_carrier [projection, in lc.Monad]
Monad_Hom.Facts [section, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
Monad_Hom [record, in lc.Monad]
monad_carrier [projection, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
monad_carrier [projection, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_carrier [projection, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
Monad_Facts [section, in lc.Monad]
Monad_Hom [section, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_carrier [projection, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
Monad_Hom.Q [variable, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
Monad_Hom [section, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
Monad_Hom [record, in lc.Monad]
monad_hom [projection, in lc.Monad]
monad_hom [projection, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
Monad_Hom [section, in lc.Monad]
Monad_Hom [record, in lc.Monad]
Monad_Facts [section, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
Monad_Hom [record, in lc.Monad]
monad_hom_join [lemma, in lc.Monad]
monad_hom_bind [projection, in lc.Monad]
Monad_Facts [section, in lc.Monad]
Monad_Hom [section, in lc.Monad]
monad_hom [projection, in lc.Monad]
Monad_Hom [section, in lc.Monad]
Monad_Facts [section, in lc.Monad]
monad_hom [projection, in lc.Monad]
monad_hom_unit [projection, in lc.Monad]
Monad_Hom [section, in lc.Monad]
Monad_Hom [record, in lc.Monad]
monad_carrier [projection, in lc.Monad]
monad_carrier [projection, in lc.Monad]
monad_hom_map [lemma, in lc.Monad]

O

optmap [definition, in lc.Misc]
optmap [definition, in lc.Misc]
optmap [definition, in lc.Misc]
optmap [definition, in lc.Misc]
optmap [definition, in lc.Misc]
optmap [definition, in lc.Misc]

P

PB [definition, in lc.Mod]
PB [definition, in lc.Mod]
Pull_back [section, in lc.Mod]
Pull_back.bb [variable, in lc.Mod]
Pull_back.bb [variable, in lc.Mod]
Pull_back [section, in lc.Mod]
Pull_back [section, in lc.Mod]
Pull_back [section, in lc.Mod]
Pull_back.P [variable, in lc.Mod]
Pull_back.M [variable, in lc.Mod]
Pull_back [section, in lc.Mod]
Pull_back.h [variable, in lc.Mod]
Pull_back [section, in lc.Mod]
Pull_back [section, in lc.Mod]
Pull_back.Q [variable, in lc.Mod]
Pull_back [section, in lc.Mod]
Pull_back [section, in lc.Mod]

Q

Quot [library]
quotient [axiom, in lc.Quot]
quotient [axiom, in lc.Quot]
quotient [axiom, in lc.Quot]
quotient [axiom, in lc.Quot]
quotient [axiom, in lc.Quot]
quotient [axiom, in lc.Quot]
quotient [axiom, in lc.Quot]
quotient [axiom, in lc.Quot]

R

rmk [lemma, in lc.Quot]
rmk [lemma, in lc.Quot]
rmk [lemma, in lc.Quot]

S

shift [definition, in lc.Slc]
shift [definition, in lc.Slc]
shift [definition, in lc.Slc]
shift [definition, in lc.Slc]
shift [definition, in lc.Slc]
shift_fct [lemma, in lc.Slc]
shift_fct [lemma, in lc.Slc]
shift_fct [lemma, in lc.Slc]
shift_fct [lemma, in lc.Slc]
shift_fct [lemma, in lc.Slc]
shift_fct [lemma, in lc.Slc]
shift_fct [lemma, in lc.Slc]
shift_fct [lemma, in lc.Slc]
shift_fct [lemma, in lc.Slc]
Slc [library]
slc_bind_fct [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_bind [definition, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind [definition, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind [definition, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind [definition, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind [definition, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_bind [definition, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind [definition, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_fct_bind [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_bind_var [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_shift_bind [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_bind [definition, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_bind_app1 [lemma, in lc.Slc]
slc_bind_fct [lemma, in lc.Slc]
slc_bind_shift [lemma, in lc.Slc]
slc_eta_bind [lemma, in lc.Slc]
slc_var_bind_match [lemma, in lc.Slc]
slc_var_bind [lemma, in lc.Slc]
slc_bind_fun_cong [lemma, in lc.Slc]
slc_fct_as_bind [lemma, in lc.Slc]
slc_bind_bind [lemma, in lc.Slc]

T

Taut_Mod [definition, in lc.Mod]
Taut_Mod [definition, in lc.Mod]
Taut_Mod [definition, in lc.Mod]
Taut_Mod [definition, in lc.Mod]
Taut_Mod [definition, in lc.Mod]
Taut_Mod [definition, in lc.Mod]
Taut_Mod [definition, in lc.Mod]
Taut_Mod [definition, in lc.Mod]
term [inductive, in lc.Slc]
term [inductive, in lc.Slc]
term [inductive, in lc.Slc]
term [inductive, in lc.Slc]
theta [definition, in lc.Quot]
theta [definition, in lc.Quot]
theta [definition, in lc.Quot]
theta [definition, in lc.Quot]
theta [definition, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta_surj [axiom, in lc.Quot]
theta' [definition, in lc.Quot]
theta' [definition, in lc.Quot]
theta' [definition, in lc.Quot]
theta' [definition, in lc.Quot]
theta' [definition, in lc.Quot]
theta' [definition, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]
theta'_compat [lemma, in lc.Quot]

U

unit [projection, in lc.Monad]
unit [projection, in lc.Monad]
unit [projection, in lc.Monad]
unit [projection, in lc.Monad]
unit_bind [projection, in lc.Monad]
unit_bb [lemma, in lc.Mod]
unit_mbind_match [lemma, in lc.Mod]
unit_bind_match [lemma, in lc.Monad]
unit_bind_match [lemma, in lc.Monad]
unit_join [lemma, in lc.Monad]
unit_bT [lemma, in lc.Derived_Mod]
unit_bind_match [lemma, in lc.Monad]
unit_mbind_match [lemma, in lc.Mod]
unit_bind_match [lemma, in lc.Monad]
unit_bT [lemma, in lc.Derived_Mod]
unit_bind_match [lemma, in lc.Monad]
unit_join [lemma, in lc.Monad]
unit_mbind_match [lemma, in lc.Mod]
unit_mbind_match [lemma, in lc.Mod]
unit_bind_match [lemma, in lc.Monad]
unit_mbind [projection, in lc.Mod]
unit_bb [lemma, in lc.Mod]
unit_bind_match [lemma, in lc.Monad]
unit_bT [lemma, in lc.Derived_Mod]
unit_join [lemma, in lc.Monad]
unit_bind_match [lemma, in lc.Monad]
unit_bb [lemma, in lc.Mod]
unit_bb [lemma, in lc.Mod]
unit_mbind_match [lemma, in lc.Mod]
unit_bind_match [lemma, in lc.Monad]
unit_bb [lemma, in lc.Mod]
unit_mbind_match [lemma, in lc.Mod]
unit_mbind_match [lemma, in lc.Mod]
unit_mbind [projection, in lc.Mod]
unit_bind_match [lemma, in lc.Monad]
unit_bind [projection, in lc.Monad]
unit_join [lemma, in lc.Monad]
unit_bT [lemma, in lc.Derived_Mod]
unit_mbind [projection, in lc.Mod]
unit_bind [projection, in lc.Monad]
unit_join [lemma, in lc.Monad]
unit_mbind_match [lemma, in lc.Mod]
unit_bind_match [lemma, in lc.Monad]
unit_join [lemma, in lc.Monad]
unit_mbind_match [lemma, in lc.Mod]
unit_mbind [projection, in lc.Mod]
unit_mbind [projection, in lc.Mod]
unit_mbind_match [lemma, in lc.Mod]
unit_mbind_match [lemma, in lc.Mod]
unit_bind_match [lemma, in lc.Monad]
unit_mbind_match [lemma, in lc.Mod]
unit_mbind_match [lemma, in lc.Mod]
unit_bT [lemma, in lc.Derived_Mod]
unit_bind_match [lemma, in lc.Monad]
unit_bind [projection, in lc.Monad]
unit_bT [lemma, in lc.Derived_Mod]
unit_bb [lemma, in lc.Mod]
unit_bb [lemma, in lc.Mod]
unit_mbind [projection, in lc.Mod]
unit_bind [projection, in lc.Monad]
unit_mbind_match [lemma, in lc.Mod]
unit_mbind [projection, in lc.Mod]
unit_mbind [projection, in lc.Mod]
unit_join [lemma, in lc.Monad]
unit_mbind_match [lemma, in lc.Mod]
unit_bT [lemma, in lc.Derived_Mod]
unit_join [lemma, in lc.Monad]
unit_bind_match [lemma, in lc.Monad]
unit_bind [projection, in lc.Monad]
unit_bind_match [lemma, in lc.Monad]
unit_mbind_match [lemma, in lc.Mod]
unit_bind [projection, in lc.Monad]
unit_mbind [projection, in lc.Mod]
unit_bind [projection, in lc.Monad]
unit_join [lemma, in lc.Monad]
unit_mbind [projection, in lc.Mod]
unit_bind [projection, in lc.Monad]

V

var [constructor, in lc.Slc]
var [constructor, in lc.Slc]
var [constructor, in lc.Slc]

other

_ / _ (quotient) [notation, in lc.Quot]
_ // _ (quotient) [notation, in lc.Quot]
_ >>>= _ [notation, in lc.Mod]
_ >>>- _ [notation, in lc.Mod]
_ >>- _ [notation, in lc.Monad]
_ >>= _ [notation, in lc.Monad]
_ //= _ [notation, in lc.Slc]
_ //- _ [notation, in lc.Slc]
_ == _ [notation, in lc.Slc]

---

Notation Index

L

/ _ [in lc.Lc]

other

_ / _ (quotient) [in lc.Quot]
_ // _ (quotient) [in lc.Quot]
_ >>>= _ [in lc.Mod]
_ >>>- _ [in lc.Mod]
_ >>- _ [in lc.Monad]
_ >>= _ [in lc.Monad]
_ //= _ [in lc.Slc]
_ //- _ [in lc.Slc]
_ == _ [in lc.Slc]

---

Variable Index

D

Derived_Mod.M [in lc.Derived_Mod]
Derived_Mod.P [in lc.Derived_Mod]
Derived_Mod.Def.bT [in lc.Derived_Mod]
Derived_Mod.Inc.i [in lc.Derived_Mod]
Derived_Mod.Def.T [in lc.Derived_Mod]
Derived_Mod.Def.bT [in lc.Derived_Mod]

F

Factor1.f [in lc.Quot]
Factor1.Hf [in lc.Quot]
Factor1.Hf [in lc.Quot]
Factor1.rX [in lc.Quot]
Factor1.rX [in lc.Quot]
Factor1.rY [in lc.Quot]
Factor1.rY [in lc.Quot]
Factor1.X [in lc.Quot]
Factor1.Y [in lc.Quot]
Factor2.f [in lc.Quot]
Factor2.h [in lc.Quot]
Factor2.Hf [in lc.Quot]
Factor2.Hf [in lc.Quot]
Factor2.rX [in lc.Quot]
Factor2.rX [in lc.Quot]
Factor2.rY [in lc.Quot]
Factor2.rY [in lc.Quot]
Factor2.rZ [in lc.Quot]
Factor2.rZ [in lc.Quot]
Factor2.X [in lc.Quot]
Factor2.Y [in lc.Quot]
Factor2.Z [in lc.Quot]

L

Lc.r [in lc.Lc]

M

Mod_Facts.P [in lc.Mod]
Mod_Facts.M [in lc.Mod]
Monad_Hom.P [in lc.Monad]
Monad_Hom.Facts.h [in lc.Monad]
Monad_Facts.P [in lc.Monad]
Monad_Hom.Q [in lc.Monad]

P

Pull_back.bb [in lc.Mod]
Pull_back.bb [in lc.Mod]
Pull_back.P [in lc.Mod]
Pull_back.M [in lc.Mod]
Pull_back.h [in lc.Mod]
Pull_back.Q [in lc.Mod]

---

Library Index

D

Derived_Mod

E

Extensionality

L

Lc

M

Misc
Mod
Monad

Q

Quot

S

Slc

---

Lemma Index

A

app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app_as_app1 [in lc.Slc]
app1_app [in lc.Slc]
app1_app [in lc.Slc]
app1_app [in lc.Slc]
app1_app [in lc.Slc]
app1_app [in lc.Slc]
app1_app [in lc.Slc]
app1_app [in lc.Slc]
app1_app [in lc.Slc]

B

bb_bb [in lc.Mod]
bb_bb [in lc.Mod]
bb_bb [in lc.Mod]
bb_bb [in lc.Mod]
bb_bb [in lc.Mod]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
beta_intro_alt [in lc.Slc]
bind_congr [in lc.Monad]
bind_congr [in lc.Monad]
bind_congr [in lc.Monad]
bind_congr [in lc.Monad]
bind_map [in lc.Monad]
bind_congr [in lc.Monad]
bind_congr [in lc.Monad]
bind_congr [in lc.Monad]
bind_map [in lc.Monad]
bind_map [in lc.Monad]
bind_congr [in lc.Monad]
bind_map [in lc.Monad]
bind_map [in lc.Monad]
bind_congr [in lc.Monad]
bind_map [in lc.Monad]
bind_map [in lc.Monad]
bind_map [in lc.Monad]
bind_congr [in lc.Monad]
bT_bT [in lc.Derived_Mod]
bT_bT [in lc.Derived_Mod]
bT_bT [in lc.Derived_Mod]
bT_bT [in lc.Derived_Mod]
bT_bT [in lc.Derived_Mod]

C

comm_var [in lc.Slc]
comm_var [in lc.Slc]
comm_var [in lc.Slc]
comm_var [in lc.Slc]
comm_var [in lc.Slc]
comm_var [in lc.Slc]
comm_var [in lc.Slc]
comm_var [in lc.Slc]

E

eq_eqv [in lc.Quot]
eq_eqv [in lc.Quot]
eq_eqv [in lc.Quot]
eq_eqv [in lc.Quot]
eq_eqv [in lc.Quot]
eq_eqv [in lc.Quot]
eta_fct [in lc.Slc]
eta_fct [in lc.Slc]
eta_fct [in lc.Slc]
eta_fct [in lc.Slc]
eta_fct [in lc.Slc]
eta_fct [in lc.Slc]
eta_fct [in lc.Slc]

F

factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize1 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factorize2 [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor1_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
factor2_extens [in lc.Quot]
fct_shift [in lc.Slc]
fct_app1 [in lc.Slc]
fct_id [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_id [in lc.Slc]
fct_fct [in lc.Slc]
fct_fct [in lc.Slc]
fct_shift [in lc.Slc]
fct_fct [in lc.Slc]
fct_shift [in lc.Slc]
fct_fct [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_fct [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_id [in lc.Slc]
fct_id [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_app1 [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_shift [in lc.Slc]
fct_shift [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_app1 [in lc.Slc]
fct_shift [in lc.Slc]
fct_app1 [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_shift [in lc.Slc]
fct_app1 [in lc.Slc]
fct_fct [in lc.Slc]
fct_fct [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_id [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_app1 [in lc.Slc]
fct_app1 [in lc.Slc]
fct_fun_cong [in lc.Slc]
fct_shift [in lc.Slc]
fct_shift [in lc.Slc]
fct_app1 [in lc.Slc]
fct_id [in lc.Slc]

I

i_hom [in lc.Derived_Mod]
i_hom [in lc.Derived_Mod]
i_hom [in lc.Derived_Mod]
i_hom [in lc.Derived_Mod]
i_hom [in lc.Derived_Mod]

J

join_join [in lc.Monad]
join_unit [in lc.Monad]
join_join [in lc.Monad]
join_join [in lc.Monad]
join_unit [in lc.Monad]
join_unit [in lc.Monad]
join_map [in lc.Monad]
join_unit [in lc.Monad]
join_map [in lc.Monad]
join_map [in lc.Monad]
join_map [in lc.Monad]
join_unit [in lc.Monad]
join_map [in lc.Monad]
join_unit [in lc.Monad]
join_join [in lc.Monad]
join_join [in lc.Monad]
join_join [in lc.Monad]
join_unit [in lc.Monad]
join_map [in lc.Monad]
join_join [in lc.Monad]
join_join [in lc.Monad]
join_map [in lc.Monad]
join_unit [in lc.Monad]
join_map [in lc.Monad]
join_unit [in lc.Monad]
join_join [in lc.Monad]

L

lcr_bind_arg [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_eq [in lc.Slc]
lcr_fct [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_app1 [in lc.Slc]
lcr_eq [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_app1 [in lc.Slc]
lcr_rfl [in lc.Slc]
lcr_rfl [in lc.Slc]
lcr_fct [in lc.Slc]
lcr_eq [in lc.Slc]
lcr_fct [in lc.Slc]
lcr_bind [in lc.Slc]
lcr_app1 [in lc.Slc]
lcr_app1 [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_bind [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_bind [in lc.Slc]
lcr_bind [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_eq [in lc.Slc]
lcr_app1 [in lc.Slc]
lcr_eq [in lc.Slc]
lcr_bind [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_fct [in lc.Slc]
lcr_rfl [in lc.Slc]
lcr_bind [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_eq [in lc.Slc]
lcr_bind [in lc.Slc]
lcr_fct [in lc.Slc]
lcr_rfl [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_app1 [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_rfl [in lc.Slc]
lcr_fct [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_app1 [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_rfl [in lc.Slc]
lcr_app1 [in lc.Slc]
lcr_bind_fun [in lc.Slc]
lcr_bind [in lc.Slc]
lcr_rfl [in lc.Slc]
lcr_bind_arg [in lc.Slc]
lcr_fct [in lc.Slc]
lc_abs_factorize [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_eta [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_eta [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_eta [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_factorize [in lc.Lc]
lc_factorize [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_eta [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_factorize [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_beta [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_beta [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_factorize [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_eta [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_factorize [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_factorize [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_factorize [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_factorize [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_beta [in lc.Lc]
lc_beta [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_factorize [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_class_surj [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_eta [in lc.Lc]
lc_factorize [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_var_bind [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_factor_cong [in lc.Lc]
lc_app_factorize [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_bind_assoc [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_abs_factorize [in lc.Lc]
lc_bind_fix_fun_cong [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_app1_factorize [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_factorize2 [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_beta [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_bind_fix_factorize [in lc.Lc]
lc_beta [in lc.Lc]
lc_fun_lift [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_bind_factorize [in lc.Lc]
lc_bind_var [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_factorize1 [in lc.Lc]
lc_fct_factorize [in lc.Lc]
lc_class_eq [in lc.Lc]
lc_bind_fix_wd [in lc.Lc]
lc_bind_fun_cong [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_bind_abs [in lc.Lc]
lc_beta [in lc.Lc]
lc_class_rel [in lc.Lc]
lc_bind_app1 [in lc.Lc]
lc_fct_as_bind [in lc.Lc]
lc_class_surj [in lc.Lc]
lift_fun [in lc.Quot]
lift_fun [in lc.Quot]
lift_fun [in lc.Quot]
lift_fun [in lc.Quot]
lift_fun [in lc.Quot]
lift_fun [in lc.Quot]
lift_fun [in lc.Quot]
lift_fun [in lc.Quot]

M

map_bind [in lc.Monad]
map_bind [in lc.Monad]
map_map [in lc.Monad]
map_unit [in lc.Monad]
map_id [in lc.Monad]
map_map [in lc.Monad]
map_unit [in lc.Monad]
map_map [in lc.Monad]
map_congr [in lc.Monad]
map_congr [in lc.Monad]
map_unit [in lc.Monad]
map_congr [in lc.Monad]
map_congr [in lc.Monad]
map_unit [in lc.Monad]
map_congr [in lc.Monad]
map_map [in lc.Monad]
map_bind [in lc.Monad]
map_id [in lc.Monad]
map_id [in lc.Monad]
map_unit [in lc.Monad]
map_congr [in lc.Monad]
map_id [in lc.Monad]
map_id [in lc.Monad]
map_unit [in lc.Monad]
map_unit [in lc.Monad]
map_bind [in lc.Monad]
map_bind [in lc.Monad]
map_unit [in lc.Monad]
map_map [in lc.Monad]
map_congr [in lc.Monad]
map_congr [in lc.Monad]
map_id [in lc.Monad]
map_map [in lc.Monad]
map_map [in lc.Monad]
map_bind [in lc.Monad]
map_congr [in lc.Monad]
map_bind [in lc.Monad]
map_bind [in lc.Monad]
mbind_mmap [in lc.Mod]
mbind_mmap [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_mmap [in lc.Mod]
mbind_mmap [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_mmap [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_mmap [in lc.Mod]
mbind_mmap [in lc.Mod]
mbind_mmap [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_mmap [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_congr [in lc.Mod]
mbind_mmap [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mmap [in lc.Mod]
mmap_mmap [in lc.Mod]
mmap_mmap [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mmap [in lc.Mod]
mmap_mmap [in lc.Mod]
mmap_mmap [in lc.Mod]
mmap_mmap [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mmap [in lc.Mod]
mmap_mbind [in lc.Mod]
mmap_mmap [in lc.Mod]
monad_hom_join [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_map [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_join [in lc.Monad]
monad_hom_map [in lc.Monad]

R

rmk [in lc.Quot]
rmk [in lc.Quot]
rmk [in lc.Quot]

S

shift_fct [in lc.Slc]
shift_fct [in lc.Slc]
shift_fct [in lc.Slc]
shift_fct [in lc.Slc]
shift_fct [in lc.Slc]
shift_fct [in lc.Slc]
shift_fct [in lc.Slc]
shift_fct [in lc.Slc]
shift_fct [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_bind_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_fct_bind [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_bind_var [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_shift_bind [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_bind_app1 [in lc.Slc]
slc_bind_fct [in lc.Slc]
slc_bind_shift [in lc.Slc]
slc_eta_bind [in lc.Slc]
slc_var_bind_match [in lc.Slc]
slc_var_bind [in lc.Slc]
slc_bind_fun_cong [in lc.Slc]
slc_fct_as_bind [in lc.Slc]
slc_bind_bind [in lc.Slc]

T

theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]
theta'_compat [in lc.Quot]

U

unit_bb [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_bind_match [in lc.Monad]
unit_bind_match [in lc.Monad]
unit_join [in lc.Monad]
unit_bT [in lc.Derived_Mod]
unit_bind_match [in lc.Monad]
unit_mbind_match [in lc.Mod]
unit_bind_match [in lc.Monad]
unit_bT [in lc.Derived_Mod]
unit_bind_match [in lc.Monad]
unit_join [in lc.Monad]
unit_mbind_match [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_bind_match [in lc.Monad]
unit_bb [in lc.Mod]
unit_bind_match [in lc.Monad]
unit_bT [in lc.Derived_Mod]
unit_join [in lc.Monad]
unit_bind_match [in lc.Monad]
unit_bb [in lc.Mod]
unit_bb [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_bind_match [in lc.Monad]
unit_bb [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_bind_match [in lc.Monad]
unit_join [in lc.Monad]
unit_bT [in lc.Derived_Mod]
unit_join [in lc.Monad]
unit_mbind_match [in lc.Mod]
unit_bind_match [in lc.Monad]
unit_join [in lc.Monad]
unit_mbind_match [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_bind_match [in lc.Monad]
unit_mbind_match [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_bT [in lc.Derived_Mod]
unit_bind_match [in lc.Monad]
unit_bT [in lc.Derived_Mod]
unit_bb [in lc.Mod]
unit_bb [in lc.Mod]
unit_mbind_match [in lc.Mod]
unit_join [in lc.Monad]
unit_mbind_match [in lc.Mod]
unit_bT [in lc.Derived_Mod]
unit_join [in lc.Monad]
unit_bind_match [in lc.Monad]
unit_bind_match [in lc.Monad]
unit_mbind_match [in lc.Mod]
unit_join [in lc.Monad]

---

Axiom Index

C

class [in lc.Quot]
class [in lc.Quot]
class [in lc.Quot]
class [in lc.Quot]
class [in lc.Quot]
class_rel [in lc.Quot]
class_ind [in lc.Quot]
class_eq [in lc.Quot]
class_ind [in lc.Quot]
class_rel [in lc.Quot]
class_eq [in lc.Quot]
class_ind [in lc.Quot]
class_rel [in lc.Quot]
class_ind [in lc.Quot]
class_rel [in lc.Quot]
class_ind [in lc.Quot]
class_ind [in lc.Quot]
class_ind [in lc.Quot]
class_eq [in lc.Quot]
class_rel [in lc.Quot]
class_ind [in lc.Quot]
class_eq [in lc.Quot]
class_ind [in lc.Quot]
class_rel [in lc.Quot]
class_rel [in lc.Quot]
class_eq [in lc.Quot]
class_rel [in lc.Quot]
class_eq [in lc.Quot]
class_eq [in lc.Quot]
class_eq [in lc.Quot]
class_rel [in lc.Quot]

E

extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]
extensionality [in lc.Extensionality]

F

factor [in lc.Quot]
factor [in lc.Quot]
factor [in lc.Quot]
factor [in lc.Quot]
factor [in lc.Quot]
factor [in lc.Quot]
factorize [in lc.Quot]
factorize [in lc.Quot]
factorize [in lc.Quot]
factorize [in lc.Quot]
factorize [in lc.Quot]
factorize [in lc.Quot]
factorize [in lc.Quot]
factorize [in lc.Quot]
factorize [in lc.Quot]

Q

quotient [in lc.Quot]
quotient [in lc.Quot]
quotient [in lc.Quot]
quotient [in lc.Quot]
quotient [in lc.Quot]
quotient [in lc.Quot]
quotient [in lc.Quot]
quotient [in lc.Quot]

T

theta_surj [in lc.Quot]
theta_surj [in lc.Quot]
theta_surj [in lc.Quot]
theta_surj [in lc.Quot]
theta_surj [in lc.Quot]
theta_surj [in lc.Quot]
theta_surj [in lc.Quot]
theta_surj [in lc.Quot]
theta_surj [in lc.Quot]
theta_surj [in lc.Quot]

---

Constructor Index

A

abs [in lc.Slc]
abs [in lc.Slc]
abs [in lc.Slc]
app [in lc.Slc]
app [in lc.Slc]
app [in lc.Slc]

B

beta_intro [in lc.Slc]
beta_intro [in lc.Slc]
beta_intro [in lc.Slc]
beta_intro [in lc.Slc]
beta_intro [in lc.Slc]
beta_intro [in lc.Slc]
beta_intro [in lc.Slc]
beta_intro [in lc.Slc]
beta_intro [in lc.Slc]
beta_intro [in lc.Slc]

L

lcr_app [in lc.Slc]
lcr_var [in lc.Slc]
lcr_sym [in lc.Slc]
lcr_app [in lc.Slc]
lcr_trs [in lc.Slc]
lcr_sym [in lc.Slc]
lcr_abs [in lc.Slc]
lcr_eta [in lc.Slc]
lcr_var [in lc.Slc]
lcr_eta [in lc.Slc]
lcr_sym [in lc.Slc]
lcr_abs [in lc.Slc]
lcr_sym [in lc.Slc]
lcr_var [in lc.Slc]
lcr_var [in lc.Slc]
lcr_beta [in lc.Slc]
lcr_eta [in lc.Slc]
lcr_abs [in lc.Slc]
lcr_abs [in lc.Slc]
lcr_app [in lc.Slc]
lcr_beta [in lc.Slc]
lcr_eta [in lc.Slc]
lcr_trs [in lc.Slc]
lcr_eta [in lc.Slc]
lcr_eta [in lc.Slc]
lcr_beta [in lc.Slc]
lcr_var [in lc.Slc]
lcr_var [in lc.Slc]
lcr_var [in lc.Slc]
lcr_beta [in lc.Slc]
lcr_trs [in lc.Slc]
lcr_abs [in lc.Slc]
lcr_abs [in lc.Slc]
lcr_trs [in lc.Slc]
lcr_trs [in lc.Slc]
lcr_eta [in lc.Slc]
lcr_app [in lc.Slc]
lcr_trs [in lc.Slc]
lcr_sym [in lc.Slc]
lcr_app [in lc.Slc]
lcr_beta [in lc.Slc]
lcr_beta [in lc.Slc]
lcr_trs [in lc.Slc]
lcr_beta [in lc.Slc]
lcr_abs [in lc.Slc]
lcr_beta [in lc.Slc]
lcr_sym [in lc.Slc]
lcr_app [in lc.Slc]
lcr_app [in lc.Slc]
lcr_sym [in lc.Slc]

V

var [in lc.Slc]
var [in lc.Slc]
var [in lc.Slc]

---

Projection Index

B

bind [in lc.Monad]
bind [in lc.Monad]
bind [in lc.Monad]
bind [in lc.Monad]
bind_bind [in lc.Monad]
bind_unit [in lc.Monad]
bind_unit [in lc.Monad]
bind_bind [in lc.Monad]
bind_unit [in lc.Monad]
bind_bind [in lc.Monad]
bind_unit [in lc.Monad]
bind_unit [in lc.Monad]
bind_bind [in lc.Monad]
bind_bind [in lc.Monad]
bind_bind [in lc.Monad]
bind_unit [in lc.Monad]
bind_bind [in lc.Monad]
bind_bind [in lc.Monad]
bind_bind [in lc.Monad]
bind_unit [in lc.Monad]
bind_unit [in lc.Monad]
bind_unit [in lc.Monad]

E

eqv_rfl [in lc.Quot]
eqv_trs [in lc.Quot]
eqv_rfl [in lc.Quot]
eqv_rfl [in lc.Quot]
eqv_sym [in lc.Quot]
eqv_rfl [in lc.Quot]
eqv_data [in lc.Quot]
eqv_data [in lc.Quot]
eqv_sym [in lc.Quot]
eqv_data [in lc.Quot]
eqv_sym [in lc.Quot]
eqv_trs [in lc.Quot]
eqv_sym [in lc.Quot]
eqv_sym [in lc.Quot]
eqv_data [in lc.Quot]
eqv_trs [in lc.Quot]
eqv_data [in lc.Quot]
eqv_trs [in lc.Quot]
eqv_trs [in lc.Quot]
eqv_data [in lc.Quot]
eqv_sym [in lc.Quot]
eqv_trs [in lc.Quot]
eqv_sym [in lc.Quot]
eqv_data [in lc.Quot]
eqv_trs [in lc.Quot]
eqv_rfl [in lc.Quot]
eqv_rfl [in lc.Quot]
eqv_rfl [in lc.Quot]
eqv_data [in lc.Quot]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_abs [in lc.Derived_Mod]
expmonad_hom_app [in lc.Derived_Mod]
expmonad_hom [in lc.Derived_Mod]
exp_abs [in lc.Derived_Mod]
exp_eta [in lc.Derived_Mod]
exp_eta [in lc.Derived_Mod]
exp_beta [in lc.Derived_Mod]
exp_beta [in lc.Derived_Mod]
exp_abs [in lc.Derived_Mod]
exp_app [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_beta [in lc.Derived_Mod]
exp_abs [in lc.Derived_Mod]
exp_app [in lc.Derived_Mod]
exp_abs [in lc.Derived_Mod]
exp_beta [in lc.Derived_Mod]
exp_beta [in lc.Derived_Mod]
exp_eta [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_app [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_beta [in lc.Derived_Mod]
exp_eta [in lc.Derived_Mod]
exp_app [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_abs [in lc.Derived_Mod]
exp_eta [in lc.Derived_Mod]
exp_beta [in lc.Derived_Mod]
exp_app [in lc.Derived_Mod]
exp_app [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_eta [in lc.Derived_Mod]
exp_abs [in lc.Derived_Mod]
exp_eta [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_beta [in lc.Derived_Mod]
exp_monad [in lc.Derived_Mod]
exp_app [in lc.Derived_Mod]
exp_abs [in lc.Derived_Mod]

M

mbind [in lc.Mod]
mbind [in lc.Mod]
mbind [in lc.Mod]
mbind [in lc.Mod]
mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mbind_mbind [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_carrier [in lc.Mod]
mod_carrier [in lc.Mod]
mod_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_carrier [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_hom_carrier [in lc.Mod]
mod_carrier [in lc.Mod]
mod_hom_mbind [in lc.Mod]
mod_carrier [in lc.Mod]
mod_carrier [in lc.Mod]
monad_hom_bind [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom [in lc.Monad]
monad_carrier [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom [in lc.Monad]
monad_hom [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_carrier [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom [in lc.Monad]
monad_hom [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom_bind [in lc.Monad]
monad_hom [in lc.Monad]
monad_hom [in lc.Monad]
monad_hom_unit [in lc.Monad]
monad_carrier [in lc.Monad]
monad_carrier [in lc.Monad]

U

unit [in lc.Monad]
unit [in lc.Monad]
unit [in lc.Monad]
unit [in lc.Monad]
unit_bind [in lc.Monad]
unit_mbind [in lc.Mod]
unit_mbind [in lc.Mod]
unit_bind [in lc.Monad]
unit_mbind [in lc.Mod]
unit_bind [in lc.Monad]
unit_mbind [in lc.Mod]
unit_mbind [in lc.Mod]
unit_bind [in lc.Monad]
unit_mbind [in lc.Mod]
unit_bind [in lc.Monad]
unit_mbind [in lc.Mod]
unit_mbind [in lc.Mod]
unit_bind [in lc.Monad]
unit_bind [in lc.Monad]
unit_mbind [in lc.Mod]
unit_bind [in lc.Monad]
unit_mbind [in lc.Mod]
unit_bind [in lc.Monad]

---

Inductive Index

B

Beta [in lc.Slc]
Beta [in lc.Slc]
Beta [in lc.Slc]
Beta [in lc.Slc]

L

lcr [in lc.Slc]
lcr [in lc.Slc]
lcr [in lc.Slc]

T

term [in lc.Slc]
term [in lc.Slc]
term [in lc.Slc]
term [in lc.Slc]

---

Section Index

D

Derived_Mod.Inc [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod.Def [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod.Inc [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod.Def [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod.Inc [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod.Def [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]

F

Factor1 [in lc.Quot]
Factor1 [in lc.Quot]
Factor1 [in lc.Quot]
Factor1 [in lc.Quot]
Factor1 [in lc.Quot]
Factor1 [in lc.Quot]
Factor1 [in lc.Quot]
Factor2 [in lc.Quot]
Factor2 [in lc.Quot]
Factor2 [in lc.Quot]
Factor2 [in lc.Quot]
Factor2 [in lc.Quot]
Factor2 [in lc.Quot]
Factor2 [in lc.Quot]

L

Lc [in lc.Lc]
Lc [in lc.Lc]

M

Mod_Facts [in lc.Mod]
Mod_Facts [in lc.Mod]
Mod_Facts [in lc.Mod]
Mod_Facts [in lc.Mod]
Mod_Facts [in lc.Mod]
Mod_Facts [in lc.Mod]
Mod_Facts [in lc.Mod]
Mod_Facts [in lc.Mod]
Mod_Facts [in lc.Mod]
Monad_Hom [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Hom.Facts [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom.Facts [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Hom.Facts [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Hom.Facts [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom.Facts [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Facts [in lc.Monad]
Monad_Hom [in lc.Monad]

P

Pull_back [in lc.Mod]
Pull_back [in lc.Mod]
Pull_back [in lc.Mod]
Pull_back [in lc.Mod]
Pull_back [in lc.Mod]
Pull_back [in lc.Mod]
Pull_back [in lc.Mod]
Pull_back [in lc.Mod]
Pull_back [in lc.Mod]

---

Definition Index

A

ap [in lc.Monad]
ap [in lc.Monad]
app1 [in lc.Slc]
app1 [in lc.Slc]
app1 [in lc.Slc]
app1 [in lc.Slc]

C

comm [in lc.Slc]
comm [in lc.Slc]
comm [in lc.Slc]
comm [in lc.Slc]

D

default [in lc.Misc]
default [in lc.Misc]
default [in lc.Misc]
default [in lc.Misc]
default [in lc.Misc]
default [in lc.Misc]
default [in lc.Misc]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]
derived_inc [in lc.Derived_Mod]
Derived_Mod [in lc.Derived_Mod]

F

factor1 [in lc.Quot]
factor1 [in lc.Quot]
factor1 [in lc.Quot]
factor1 [in lc.Quot]
factor1 [in lc.Quot]
factor1 [in lc.Quot]
factor1 [in lc.Quot]
factor2 [in lc.Quot]
factor2 [in lc.Quot]
factor2 [in lc.Quot]
factor2 [in lc.Quot]
factor2 [in lc.Quot]
factor2 [in lc.Quot]
factor2 [in lc.Quot]
fct [in lc.Slc]
fct [in lc.Slc]
fct [in lc.Slc]
feqv [in lc.Quot]
feqv [in lc.Quot]
feqv [in lc.Quot]
feqv [in lc.Quot]
frel [in lc.Quot]
frel [in lc.Quot]
frel [in lc.Quot]
frel [in lc.Quot]

J

join [in lc.Monad]
join [in lc.Monad]
join [in lc.Monad]
join [in lc.Monad]

L

lc [in lc.Lc]
lc [in lc.Lc]
lc_bind [in lc.Lc]
lc_class [in lc.Lc]
lc_app [in lc.Lc]
lc_app [in lc.Lc]
lc_var [in lc.Lc]
lc_abs [in lc.Lc]
lc_class [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_fct [in lc.Lc]
lc_factor [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_app1 [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_class [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_var [in lc.Lc]
lc_factor [in lc.Lc]
lc_fct [in lc.Lc]
lc_bind [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_app [in lc.Lc]
lc_factor [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_app [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_app1 [in lc.Lc]
lc_bind [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_abs [in lc.Lc]
lc_fct [in lc.Lc]
lc_factor [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_comm [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_fct [in lc.Lc]
lc_bind [in lc.Lc]
lc_app1 [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_class [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_comm [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_var [in lc.Lc]
lc_var [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_app1 [in lc.Lc]
lc_app [in lc.Lc]
lc_fct [in lc.Lc]
lc_class [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_comm [in lc.Lc]
lc_bind [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_factor [in lc.Lc]
lc_class [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_abs [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_app [in lc.Lc]
lc_comm [in lc.Lc]
lc_fct [in lc.Lc]
lc_bind [in lc.Lc]
lc_abs [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_factor1 [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_class [in lc.Lc]
lc_factor [in lc.Lc]
lc_comm [in lc.Lc]
lc_app1 [in lc.Lc]
lc_factor2 [in lc.Lc]
lc_abs [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_var [in lc.Lc]
lc_factor [in lc.Lc]
lc_var [in lc.Lc]
lc_factor [in lc.Lc]
lc_comm [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_abs [in lc.Lc]
lc_app1 [in lc.Lc]
lc_bind [in lc.Lc]
lc_class [in lc.Lc]
lc_factor [in lc.Lc]
lc_bind_fix [in lc.Lc]
lc_app1 [in lc.Lc]
lc_comm [in lc.Lc]
lift [in lc.Monad]
lift [in lc.Monad]
lift [in lc.Monad]
lift [in lc.Monad]
lift2 [in lc.Monad]
lift2 [in lc.Monad]
lift2 [in lc.Monad]
lift2 [in lc.Monad]
lift2 [in lc.Monad]
lift3 [in lc.Monad]
lift3 [in lc.Monad]
lift3 [in lc.Monad]
lift3 [in lc.Monad]
lift3 [in lc.Monad]

M

map [in lc.Monad]
map [in lc.Monad]
map [in lc.Monad]
mlift [in lc.Mod]
mlift [in lc.Mod]
mlift [in lc.Mod]
mlift [in lc.Mod]
mlift [in lc.Mod]
mlift2 [in lc.Mod]
mlift2 [in lc.Mod]
mlift2 [in lc.Mod]
mlift2 [in lc.Mod]
mlift2 [in lc.Mod]
mlift2 [in lc.Mod]
mmap [in lc.Mod]
mmap [in lc.Mod]
mmap [in lc.Mod]
mmap [in lc.Mod]

O

optmap [in lc.Misc]
optmap [in lc.Misc]
optmap [in lc.Misc]
optmap [in lc.Misc]
optmap [in lc.Misc]
optmap [in lc.Misc]

P

PB [in lc.Mod]
PB [in lc.Mod]

S

shift [in lc.Slc]
shift [in lc.Slc]
shift [in lc.Slc]
shift [in lc.Slc]
shift [in lc.Slc]
slc_bind [in lc.Slc]
slc_bind [in lc.Slc]
slc_bind [in lc.Slc]
slc_bind [in lc.Slc]
slc_bind [in lc.Slc]
slc_bind [in lc.Slc]
slc_bind [in lc.Slc]
slc_bind [in lc.Slc]

T

Taut_Mod [in lc.Mod]
Taut_Mod [in lc.Mod]
Taut_Mod [in lc.Mod]
Taut_Mod [in lc.Mod]
Taut_Mod [in lc.Mod]
Taut_Mod [in lc.Mod]
Taut_Mod [in lc.Mod]
Taut_Mod [in lc.Mod]
theta [in lc.Quot]
theta [in lc.Quot]
theta [in lc.Quot]
theta [in lc.Quot]
theta [in lc.Quot]
theta' [in lc.Quot]
theta' [in lc.Quot]
theta' [in lc.Quot]
theta' [in lc.Quot]
theta' [in lc.Quot]
theta' [in lc.Quot]

---

Record Index

E

Eqv [in lc.Quot]
Eqv [in lc.Quot]
Eqv [in lc.Quot]
ExpMonad [in lc.Derived_Mod]
ExpMonad [in lc.Derived_Mod]
ExpMonad [in lc.Derived_Mod]
ExpMonad [in lc.Derived_Mod]
ExpMonad [in lc.Derived_Mod]
ExpMonad [in lc.Derived_Mod]
ExpMonad [in lc.Derived_Mod]
ExpMonad [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]
ExpMonad_Hom [in lc.Derived_Mod]

M

Mod [in lc.Mod]
Mod [in lc.Mod]
Mod [in lc.Mod]
Mod_Hom [in lc.Mod]
Mod_Hom [in lc.Mod]
Mod_Hom [in lc.Mod]
Mod_Hom [in lc.Mod]
Mod_Hom [in lc.Mod]
Mod_Hom [in lc.Mod]
Mod_Hom [in lc.Mod]
Monad [in lc.Monad]
Monad [in lc.Monad]
Monad [in lc.Monad]
Monad [in lc.Monad]
Monad [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]
Monad_Hom [in lc.Monad]

---

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

(1805 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

(10 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

(41 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

(969 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

(78 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

(69 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

(261 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

(11 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

(76 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

(235 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

(47 entries)