Benedikt Ahrens and Régis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory

Table of contents

Index

Global Index

G

J

K

Q

V

W

X

Y

Z

_

(574 entries)

Notation Index

A

B

C

E

G

H

I

J

K

L

N

O

Q

R

U

V

W

X

Y

Z

_

(139 entries)

Module Index

A

B

C

E

F

G

H

I

J

K

L

N

O

P

Q

R

U

V

W

X

Y

Z

_

(21 entries)

Variable Index

A

B

C

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(3 entries)

Library Index

B

E

G

H

J

K

L

O

Q

V

W

X

Y

Z

_

other

(32 entries)

Lemma Index

A

B

D

E

G

H

J

K

N

O

Q

U

V

W

X

Y

Z

_

(77 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

Q

R

U

V

W

X

Y

Z

_

(29 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(20 entries)

Projection Index

D

G

J

K

N

Q

U

V

W

X

Y

Z

_

(76 entries)

Inductive Index

A

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(5 entries)

Section Index

A

B

G

H

J

K

L

N

O

Q

R

U

V

W

X

Y

Z

_

other

(28 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

(6 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

(13 entries)

Definition Index

A

B

G

J

K

N

O

Q

U

V

W

X

Y

Z

_

(100 entries)

Record Index

A

D

E

G

H

J

K

L

O

Q

U

V

W

X

Y

Z

_

(25 entries)

Global Index

A

AxB [projection, in Cat.Theory.Product]
Axioms [library]
Axioms [library]

B

BinaryProduct [record, in Cat.Theory.Product]
BinaryProduct [inductive, in Cat.Theory.Product]
bottom [projection, in Cat.Theory.InitialTerminal]
bottom_unique [projection, in Cat.Theory.InitialTerminal]

C

CanonicalCut [section, in Cat.Theory.RelativeComonadWithCut]
CartesianStrongMonoidal [record, in Cat.Theory.CartesianStrongMonoidal]
CartesianStrongMonoidal [library]
Category [record, in Cat.Theory.Category]
Category [library]
Category [library]
Category [library]
ccut [definition, in Cat.Theory.RelativeComonadWithCut]
cobind [projection, in Cat.Theory.RelativeComonad]
cobind_cobind [projection, in Cat.Theory.RelativeComonad]
cobind_counit [projection, in Cat.Theory.RelativeComonad]
Commutes [section, in Cat.Theory.PushforwardComodule]
Comodule [record, in Cat.Theory.Comodule]
Comodule [library]
compose [definition, in Cat.Category.Stream.Category]
compose [definition, in Cat.Category.TriMat.Category]
compose [projection, in Cat.Theory.Category]
compose [definition, in Cat.Category.Setoids]
compose [definition, in Cat.Category.Types]
compose_assoc [lemma, in Cat.Category.RComonadWithCut]
compose_assoc [lemma, in Cat.Category.Stream.Category]
compose_assoc [lemma, in Cat.Category.TriMat.Category]
compose_assoc [lemma, in Cat.Category.RComonad]
compose_assoc [projection, in Cat.Theory.Category]
compose_assoc [lemma, in Cat.Category.Setoids]
compose_assoc [lemma, in Cat.Category.RComod]
compose_assoc [lemma, in Cat.Category.Types]
counit [projection, in Cat.Theory.RelativeComonad]
counit_cobind [projection, in Cat.Theory.RelativeComonad]
cut [projection, in Cat.Theory.RelativeComonadWithCut]
cut_cobind [projection, in Cat.Theory.RelativeComonadWithCut]
cut_counit [projection, in Cat.Theory.RelativeComonadWithCut]
Cut_NT [library]

D

Definitions [section, in Cat.Category.RComonadWithCut]
Definitions [section, in Cat.Category.RComonad]
Definitions [section, in Cat.Category.RComod]
_ ∘ _ [notation, in Cat.Category.RComonadWithCut]
_ ⇒ _ [notation, in Cat.Category.RComonadWithCut]
_ ∘ _ [notation, in Cat.Category.RComonad]
_ ⇒ _ [notation, in Cat.Category.RComonad]
_ ∘ _ [notation, in Cat.Category.RComod]
_ ⇒ _ [notation, in Cat.Category.RComod]
Defs [section, in Cat.Category.RComonad_RComonadWithCut]
Defs [section, in Cat.Category.Stream.Category]
Defs [section, in Cat.Category.TriMat.Category]
Defs [section, in Cat.Theory.RelativeComonadWithCut]
Defs.E [variable, in Cat.Category.TriMat.Category]
Defs.ExtendConstruction [section, in Cat.Theory.RelativeComonadWithCut]
_ ∘ _ [notation, in Cat.Category.Stream.Category]
_ ⇒ _ [notation, in Cat.Category.Stream.Category]
_ ∘ _ [notation, in Cat.Category.TriMat.Category]
_ ⇒ _ [notation, in Cat.Category.TriMat.Category]
Diag [module, in Cat.Category.Diag]
Diag [library]
Diag.Str [module, in Cat.Category.Diag]
Diag.Tri [module, in Cat.Category.Diag]
Diag.𝒅𝒊𝒂𝒈 [definition, in Cat.Category.Diag]

E

empty [projection, in Cat.Theory.InitialTerminal]
equations [section, in Cat.Theory.CartesianStrongMonoidal]
extend [definition, in Cat.Theory.RelativeComonadWithCut]
Extend [definition, in Cat.Theory.RelativeComonadWithCut]

F

F [projection, in Cat.Theory.Functor]
F [definition, in Cat.Category.Types_Setoids]
Functor [record, in Cat.Theory.Functor]
Functor [library]
Functoriality [section, in Cat.Theory.PushforwardComodule]
Functoriality [section, in Cat.Theory.Comodule]
Functoriality [section, in Cat.Theory.RelativeComonad]
_ ⁎ _ [notation, in Cat.Theory.PushforwardComodule]
Fπ₁_φ_inv [lemma, in Cat.Theory.CartesianStrongMonoidal]
Fπ₂_φ_inv [lemma, in Cat.Theory.CartesianStrongMonoidal]

H

Hom [projection, in Cat.Theory.Category]
Hom [definition, in Cat.Category.Types]

I

id [definition, in Cat.Category.Stream.Category]
id [definition, in Cat.Category.TriMat.Category]
id [projection, in Cat.Theory.Category]
id [definition, in Cat.Category.Setoids]
id [lemma, in Cat.Category.Types_Setoids]
id [definition, in Cat.Category.Types]
identity [projection, in Cat.Theory.Functor]
induced_morphism [definition, in Cat.Theory.PushforwardComodule]
induced_morphism [section, in Cat.Theory.PushforwardComodule]
Initial [record, in Cat.Theory.InitialTerminal]
InitialTerminal [library]
inverse_of [definition, in Cat.Theory.Isomorphism]
IsInverse [record, in Cat.Theory.Isomorphism]
Iso [record, in Cat.Theory.Isomorphism]
Isomorphism [library]
Iso_Equivalence [section, in Cat.Theory.Isomorphism]
iso_inverse [projection, in Cat.Theory.Isomorphism]
iso_to [projection, in Cat.Theory.Isomorphism]
iso_from [projection, in Cat.Theory.Isomorphism]
iso_right [projection, in Cat.Theory.Isomorphism]
iso_left [projection, in Cat.Theory.Isomorphism]

L

left_id [lemma, in Cat.Category.RComonadWithCut]
left_id [lemma, in Cat.Category.Stream.Category]
left_id [lemma, in Cat.Category.TriMat.Category]
left_id [lemma, in Cat.Category.RComonad]
left_id [projection, in Cat.Theory.Category]
left_id [lemma, in Cat.Category.Setoids]
left_id [lemma, in Cat.Category.RComod]
left_id [lemma, in Cat.Category.Types]
Lift [definition, in Cat.Theory.RelativeComonad]
lift [definition, in Cat.Theory.RelativeComonad]
lift_compose [lemma, in Cat.Theory.RelativeComonad]
lift_id [lemma, in Cat.Theory.RelativeComonad]

M

M [projection, in Cat.Theory.Comodule]
map [projection, in Cat.Theory.Functor]
map [definition, in Cat.Category.Types_Setoids]
map_compose [projection, in Cat.Theory.Functor]
map_compose [lemma, in Cat.Category.Types_Setoids]
mcobind [projection, in Cat.Theory.Comodule]
mcobind_mcobind [projection, in Cat.Theory.Comodule]
mcobind_counit [projection, in Cat.Theory.Comodule]
MDefs [section, in Cat.Theory.RelativeComonadWithCut]
[ _ ] [notation, in Cat.Theory.RelativeComonadWithCut]
mkCartesianStrongMonoidal [constructor, in Cat.Theory.CartesianStrongMonoidal]
mkCategory [constructor, in Cat.Theory.Category]
mkComodule [constructor, in Cat.Theory.Comodule]
mkFunctor [constructor, in Cat.Theory.Functor]
mkInitial [constructor, in Cat.Theory.InitialTerminal]
mkInverse [constructor, in Cat.Theory.Isomorphism]
mkIso [constructor, in Cat.Theory.Isomorphism]
mkMorphism [constructor, in Cat.Theory.Comodule]
mkMorphism [constructor, in Cat.Theory.RelativeComonad]
mkMorphism [constructor, in Cat.Theory.RelativeComonadWithCut]
mkNaturalTransformation [constructor, in Cat.Theory.NaturalTransformation]
mkProduct [constructor, in Cat.Theory.Product]
mkRelativeComonad [constructor, in Cat.Theory.RelativeComonad]
mkRelativeComonadWithCut [constructor, in Cat.Theory.RelativeComonadWithCut]
mkTerminal [constructor, in Cat.Theory.InitialTerminal]
MLift [definition, in Cat.Theory.Comodule]
mlift [definition, in Cat.Theory.Comodule]
mlift_compose [lemma, in Cat.Theory.Comodule]
mlift_id [lemma, in Cat.Theory.Comodule]
Model [library]
Model [library]
Morphism [module, in Cat.Theory.Comodule]
Morphism [record, in Cat.Theory.Comodule]
Morphism [module, in Cat.Theory.RelativeComonad]
Morphism [record, in Cat.Theory.RelativeComonad]
Morphism [module, in Cat.Theory.RelativeComonadWithCut]
Morphism [record, in Cat.Theory.RelativeComonadWithCut]
Morphisms [section, in Cat.Theory.PrecompositionWithProduct]
Morphism.compose [definition, in Cat.Theory.Comodule]
Morphism.compose [definition, in Cat.Theory.RelativeComonad]
Morphism.compose [definition, in Cat.Theory.RelativeComonadWithCut]
Morphism.Hom [definition, in Cat.Theory.Comodule]
Morphism.Hom [definition, in Cat.Theory.RelativeComonad]
Morphism.Hom [definition, in Cat.Theory.RelativeComonadWithCut]
Morphism.id [definition, in Cat.Theory.Comodule]
Morphism.id [definition, in Cat.Theory.RelativeComonad]
Morphism.id [definition, in Cat.Theory.RelativeComonadWithCut]
_ ⇒ _ [notation, in Cat.Theory.Comodule]
Morphism.id_composition [section, in Cat.Theory.Comodule]
_ ⇒ _ [notation, in Cat.Theory.RelativeComonad]
Morphism.id_composition [section, in Cat.Theory.RelativeComonad]
_ ⇒ _ [notation, in Cat.Theory.RelativeComonadWithCut]
Morphism.id_composition [section, in Cat.Theory.RelativeComonadWithCut]

N

NaturalTransformation [record, in Cat.Theory.NaturalTransformation]
NaturalTransformation [library]
Notations [library]

O

Obj [projection, in Cat.Theory.Category]
one [projection, in Cat.Theory.InitialTerminal]

P

Pmor [projection, in Cat.Theory.Product]
Pmor_universal [projection, in Cat.Theory.Product]
PrecompositionWithProduct [section, in Cat.Theory.PrecompositionWithProduct]
PrecompositionWithProduct [library]
precomposition_with_product_mor [definition, in Cat.Theory.PrecompositionWithProduct]
precomposition_with_product [definition, in Cat.Theory.PrecompositionWithProduct]
product [definition, in Cat.Category.Setoids]
product [projection, in Cat.Theory.Product]
product [constructor, in Cat.Theory.Product]
Product [record, in Cat.Theory.Product]
Product [library]
product_mor [definition, in Cat.Category.Setoids]
_ ∼ _ [notation, in Cat.Category.Setoids]
Product_construction [section, in Cat.Category.Setoids]
product_precompose [lemma, in Cat.Theory.Product]
product_postcompose [lemma, in Cat.Theory.Product]
prod_cat [definition, in Cat.Theory.Category]
prod_on_arrow [definition, in Cat.Theory.Product]
proj_r [definition, in Cat.Category.Setoids]
proj_l [definition, in Cat.Category.Setoids]
Pushforward [definition, in Cat.Theory.PushforwardComodule]
pushforward [definition, in Cat.Theory.PushforwardComodule]
PushforwardComodule [library]
pushforward_mor [definition, in Cat.Theory.PushforwardComodule]
Pushforward_construction [section, in Cat.Theory.PushforwardComodule]

R

RComod [library]
RComonad [library]
RComonadWithCut [library]
RComonad_RComonadWithCut [library]
refl [definition, in Cat.Theory.Isomorphism]
RelativeComonad [record, in Cat.Theory.RelativeComonad]
RelativeComonad [library]
RelativeComonadWithCut [record, in Cat.Theory.RelativeComonadWithCut]
RelativeComonadWithCut [library]
right_id [lemma, in Cat.Category.RComonadWithCut]
right_id [lemma, in Cat.Category.Stream.Category]
right_id [lemma, in Cat.Category.TriMat.Category]
right_id [lemma, in Cat.Category.RComonad]
right_id [projection, in Cat.Theory.Category]
right_id [lemma, in Cat.Category.Setoids]
right_id [lemma, in Cat.Category.RComod]
right_id [lemma, in Cat.Category.Types]

S

Setoid [module, in Cat.Theory.SetoidType]
Setoids [module, in Cat.Category.Setoids]
Setoids [library]
Setoids.cong [projection, in Cat.Category.Setoids]
Setoids.Hom [definition, in Cat.Category.Setoids]
Setoids.is_SEquiv [projection, in Cat.Category.Setoids]
Setoids.map [projection, in Cat.Category.Setoids]
Setoids.map_Proper [instance, in Cat.Category.Setoids]
Setoids.mkMorphism [constructor, in Cat.Category.Setoids]
Setoids.mkObj [constructor, in Cat.Category.Setoids]
Setoids.Morphism [module, in Cat.Category.Setoids]
Setoids.Morphism [record, in Cat.Category.Setoids]
Setoids.Morphism.make [abbreviation, in Cat.Category.Setoids]
Setoids.Obj [record, in Cat.Category.Setoids]
Setoids.SCarrier [projection, in Cat.Category.Setoids]
Setoids.SEquiv [projection, in Cat.Category.Setoids]
Setoids.make ⦃ Carrier ≔ _ ; Equiv ≔ _ ⦄ [notation, in Cat.Category.Setoids]
SetoidType [library]
Setoid.Carrier [projection, in Cat.Theory.SetoidType]
Setoid.Equiv [projection, in Cat.Theory.SetoidType]
Setoid.eq_setoid [definition, in Cat.Theory.SetoidType]
Setoid.is_Equiv [projection, in Cat.Theory.SetoidType]
Setoid.mkSetoid [constructor, in Cat.Theory.SetoidType]
Setoid.Setoid [record, in Cat.Theory.SetoidType]
_ ≉ _ [notation, in Cat.Theory.SetoidType]
_ ≈ _ [notation, in Cat.Theory.SetoidType]
_ ≈ _ :> _ [notation, in Cat.Theory.SetoidType]
Setoid.make ⦃ Carrier ≔ _ ; Equiv ≔ _ ⦄ [notation, in Cat.Theory.SetoidType]
_≈_ [notation, in Cat.Theory.SetoidType]
Stream [module, in Cat.Category.Stream.Category]
StreamAxioms [module, in Cat.Category.Stream.Axioms]
StreamAxioms.bisim [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.bisim_intro [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.bisim_tail [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.bisim_head [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.corec [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.head [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.head_corec [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.Stream [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.tail [axiom, in Cat.Category.Stream.Axioms]
StreamAxioms.tail_corec [axiom, in Cat.Category.Stream.Axioms]
_ ∼ _ [notation, in Cat.Category.Stream.Axioms]
∼-head [notation, in Cat.Category.Stream.Axioms]
∼-tail [notation, in Cat.Category.Stream.Axioms]
StreamInstance [module, in Cat.Category.Stream.Model]
StreamInstance.bintro [constructor, in Cat.Category.Stream.Model]
StreamInstance.bisim [definition, in Cat.Category.Stream.Model]
StreamInstance.bisim_intro [lemma, in Cat.Category.Stream.Model]
StreamInstance.bisim_tail [lemma, in Cat.Category.Stream.Model]
StreamInstance.bisim_head [lemma, in Cat.Category.Stream.Model]
StreamInstance.bisim_ [inductive, in Cat.Category.Stream.Model]
StreamInstance.Cons [constructor, in Cat.Category.Stream.Model]
StreamInstance.corec [definition, in Cat.Category.Stream.Model]
StreamInstance.head [definition, in Cat.Category.Stream.Model]
StreamInstance.head_corec [lemma, in Cat.Category.Stream.Model]
StreamInstance.Stream [definition, in Cat.Category.Stream.Model]
StreamInstance.Stream_ [inductive, in Cat.Category.Stream.Model]
StreamInstance.tail [definition, in Cat.Category.Stream.Model]
StreamInstance.tail_corec [lemma, in Cat.Category.Stream.Model]
_ ∼ _ [notation, in Cat.Category.Stream.Model]
_ ∷ _ [notation, in Cat.Category.Stream.Model]
_∷_ [notation, in Cat.Category.Stream.Model]
StreamTerminal [module, in Cat.Category.Stream.Terminality]
StreamTerminal.bisim_equiv [instance, in Cat.Category.Stream.Terminality]
StreamTerminal.bisim_trans [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.bisim_sym [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.bisim_refl [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.cosubst [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.Defs [section, in Cat.Category.Stream.Terminality]
StreamTerminal.Defs.Tr [variable, in Cat.Category.Stream.Terminality]
_ ∼ _ [notation, in Cat.Category.Stream.Terminality]
STR⋅tail [notation, in Cat.Category.Stream.Terminality]
STR⋅tail[ _ ] [notation, in Cat.Category.Stream.Terminality]
T⋅tail [notation, in Cat.Category.Stream.Terminality]
T⋅tail[ _ ] [notation, in Cat.Category.Stream.Terminality]
StreamTerminal.eq_bisim [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.head_tau [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.head_cong [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.STR [abbreviation, in Cat.Category.Stream.Terminality]
StreamTerminal.STREAM [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.T [abbreviation, in Cat.Category.Stream.Terminality]
StreamTerminal.tail_tau [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.tail_cong [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.Tau [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.tau [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.tau_cobind [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.tau_counit [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.tau_cong [lemma, in Cat.Category.Stream.Terminality]
StreamTerminal.Terminality [definition, in Cat.Category.Stream.Terminality]
⟨ _ ⟩ [notation, in Cat.Category.Stream.Terminality]
StreamTerminal.τ [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.𝑺𝑻𝑹 [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.𝑺𝒕𝒓 [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.𝑻𝒂𝒊𝒍 [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.𝒉𝒆𝒂𝒅 [definition, in Cat.Category.Stream.Terminality]
StreamTerminal.𝒕𝒂𝒊𝒍 [definition, in Cat.Category.Stream.Terminality]
Stream.Hom [definition, in Cat.Category.Stream.Category]
Stream.mkMorphism [constructor, in Cat.Category.Stream.Category]
Stream.mkObj [constructor, in Cat.Category.Stream.Category]
Stream.Morphism [record, in Cat.Category.Stream.Category]
Stream.Obj [record, in Cat.Category.Stream.Category]
Stream.T [projection, in Cat.Category.Stream.Category]
Stream.tail [projection, in Cat.Category.Stream.Category]
Stream.make ⦃ τ ≔ _ ⦄ [notation, in Cat.Category.Stream.Category]
Stream.make ⦃ T ≔ _ ; tail ≔ _ ⦄ [notation, in Cat.Category.Stream.Category]
Stream.τ [projection, in Cat.Category.Stream.Category]
Stream.τ_commutes [projection, in Cat.Category.Stream.Category]
StrongMonoidal [section, in Cat.Theory.CartesianStrongMonoidal]
sym [definition, in Cat.Theory.Isomorphism]

T

T [projection, in Cat.Theory.RelativeComonad]
T [projection, in Cat.Theory.RelativeComonadWithCut]
tautological_comodule [section, in Cat.Theory.PushforwardComodule]
tcomod [definition, in Cat.Theory.PushforwardComodule]
Terminal [record, in Cat.Theory.InitialTerminal]
Terminality [module, in Cat.Category.TriMat.Model]
Terminality [module, in Cat.Category.Stream.Model]
Terminality [library]
Terminality [library]
top [projection, in Cat.Theory.InitialTerminal]
top_unique [projection, in Cat.Theory.InitialTerminal]
trans [definition, in Cat.Theory.Isomorphism]
TriInstance [module, in Cat.Category.TriMat.Model]
TriInstance.bisim [definition, in Cat.Category.TriMat.Model]
TriInstance.bisim_intro [lemma, in Cat.Category.TriMat.Model]
TriInstance.bisim_rest [lemma, in Cat.Category.TriMat.Model]
TriInstance.bisim_top [lemma, in Cat.Category.TriMat.Model]
TriInstance.bisim_constr [constructor, in Cat.Category.TriMat.Model]
TriInstance.bisim_ [inductive, in Cat.Category.TriMat.Model]
TriInstance.constr [constructor, in Cat.Category.TriMat.Model]
TriInstance.corec [definition, in Cat.Category.TriMat.Model]
TriInstance.E [abbreviation, in Cat.Category.TriMat.Model]
TriInstance.rest [definition, in Cat.Category.TriMat.Model]
TriInstance.rest_corec [lemma, in Cat.Category.TriMat.Model]
TriInstance.top [definition, in Cat.Category.TriMat.Model]
TriInstance.top_corec [lemma, in Cat.Category.TriMat.Model]
TriInstance.Tri [definition, in Cat.Category.TriMat.Model]
TriInstance.Tri_ [inductive, in Cat.Category.TriMat.Model]
_ ∼ _ [notation, in Cat.Category.TriMat.Model]
∼-rest [notation, in Cat.Category.TriMat.Model]
∼-top [notation, in Cat.Category.TriMat.Model]
TriMat [module, in Cat.Category.TriMat.Category]
TriMatAxioms [module, in Cat.Category.TriMat.Axioms]
TriMatAxioms.bisim [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.bisim_intro [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.bisim_rest [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.bisim_top [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.corec [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.E [abbreviation, in Cat.Category.TriMat.Axioms]
TriMatAxioms.rest [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.rest_corec [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.top [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.top_corec [axiom, in Cat.Category.TriMat.Axioms]
TriMatAxioms.Tri [axiom, in Cat.Category.TriMat.Axioms]
_ ∼ _ [notation, in Cat.Category.TriMat.Axioms]
∼-rest [notation, in Cat.Category.TriMat.Axioms]
∼-top [notation, in Cat.Category.TriMat.Axioms]
TriMatTerminal [module, in Cat.Category.TriMat.Terminality]
TriMatTerminal.bisim_intro_bis [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.bisim_equiv [instance, in Cat.Category.TriMat.Terminality]
TriMatTerminal.bisim_trans [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.bisim_sym [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.bisim_refl [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.coRec [abbreviation, in Cat.Category.TriMat.Terminality]
TriMatTerminal.cut [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.cut_cong [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.Defs [section, in Cat.Category.TriMat.Terminality]
TriMatTerminal.Defs.Tr [variable, in Cat.Category.TriMat.Terminality]
_ ∼ _ [notation, in Cat.Category.TriMat.Terminality]
TRI⋅rest [notation, in Cat.Category.TriMat.Terminality]
TRI⋅rest[ _ ] [notation, in Cat.Category.TriMat.Terminality]
T⋅rest [notation, in Cat.Category.TriMat.Terminality]
T⋅rest[ _ ] [notation, in Cat.Category.TriMat.Terminality]
TriMatTerminal.E [abbreviation, in Cat.Category.TriMat.Terminality]
TriMatTerminal.eq_bisim [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.lift [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.lift_ext [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.lift_cong [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.redec [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.redec_cut [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.redec_ext [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.redec_cong [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.rest_tau [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.rest_redec [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.rest_cut [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.rest_cong [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.T [abbreviation, in Cat.Category.TriMat.Terminality]
TriMatTerminal.Tau [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau_cobind [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau_cut [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau_counit [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau_cong [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.Terminality [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.top_tau [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.top_redec [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.top_cut [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.top_cong [lemma, in Cat.Category.TriMat.Terminality]
TriMatTerminal.TRI [abbreviation, in Cat.Category.TriMat.Terminality]
TriMatTerminal.TRI [definition, in Cat.Category.TriMat.Terminality]
⟨ _ ⟩ [notation, in Cat.Category.TriMat.Terminality]
TriMatTerminal.τ [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝑪𝒖𝒕 [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝑹𝒆𝒔𝒕 [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝑻𝑹𝑰 [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝑻𝒓𝒊 [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝒓𝒆𝒔𝒕 [definition, in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝒕𝒐𝒑 [definition, in Cat.Category.TriMat.Terminality]
TriMat.Hom [definition, in Cat.Category.TriMat.Category]
TriMat.mkMorphism [constructor, in Cat.Category.TriMat.Category]
TriMat.mkObj [constructor, in Cat.Category.TriMat.Category]
TriMat.Morphism [record, in Cat.Category.TriMat.Category]
TriMat.Obj [record, in Cat.Category.TriMat.Category]
TriMat.rest [projection, in Cat.Category.TriMat.Category]
TriMat.rest_cut [projection, in Cat.Category.TriMat.Category]
TriMat.T [projection, in Cat.Category.TriMat.Category]
TriMat.make ⦃ τ ≔ _ ⦄ [notation, in Cat.Category.TriMat.Category]
TriMat.make ⦃ T ≔ _ ; rest ≔ _ ⦄ [notation, in Cat.Category.TriMat.Category]
TriMat.τ [projection, in Cat.Category.TriMat.Category]
TriMat.τ_commutes [projection, in Cat.Category.TriMat.Category]
Types [library]
Types_Setoids [library]

U

Unicode [library]

other

_ ≠ _ (type_scope) [notation, in Cat.Misc.Unicode]
¬ _ (type_scope) [notation, in Cat.Misc.Unicode]
_ ↔ _ (type_scope) [notation, in Cat.Misc.Unicode]
_ → _ (type_scope) [notation, in Cat.Misc.Unicode]
_ ∧ _ (type_scope) [notation, in Cat.Misc.Unicode]
_ ∨ _ (type_scope) [notation, in Cat.Misc.Unicode]
∃ _ .. _ , _ (type_scope) [notation, in Cat.Misc.Unicode]
∀ _ .. _ , _ (type_scope) [notation, in Cat.Misc.Unicode]
_ ⁎ [notation, in Cat.Theory.PushforwardComodule]
_ ⋅mcobind [notation, in Cat.Theory.Comodule]
_ ⋅ _ [notation, in Cat.Theory.Functor]
_ ［ _ ×─ ］ [notation, in Cat.Theory.PrecompositionWithProduct]
_ [ _ ×─ ] [notation, in Cat.Theory.PrecompositionWithProduct]
_ 𝘅 _ [notation, in Cat.Theory.Category]
_ -id[ _ ] [notation, in Cat.Theory.Category]
_ -id [notation, in Cat.Theory.Category]
_ ∘ _ [notation, in Cat.Theory.Category]
_ ⇒ _ [notation, in Cat.Theory.Category]
_ ⋅cobind [notation, in Cat.Theory.RelativeComonad]
_ ⋅counit[ _ ] [notation, in Cat.Theory.RelativeComonad]
_ ⋅counit [notation, in Cat.Theory.RelativeComonad]
_ ⟨×⟩ _ [notation, in Cat.Theory.Notations]
_ ⟨⊎⟩ _ [notation, in Cat.Theory.Notations]
_ ∘ _ [notation, in Cat.Category.Setoids]
_ ⇒ _ [notation, in Cat.Category.Setoids]
_ ⋅≅-right [notation, in Cat.Theory.Isomorphism]
_ ⋅≅-left [notation, in Cat.Theory.Isomorphism]
_ ≅ _ [notation, in Cat.Theory.Isomorphism]
_ ⁻¹ [notation, in Cat.Theory.Isomorphism]
_ -×- _ [notation, in Cat.Theory.Product]
_ × _ [notation, in Cat.Theory.Product]
_ ⋅π₂ [notation, in Cat.Theory.Product]
_ ⋅π₁ [notation, in Cat.Theory.Product]
_ ⋅extend [notation, in Cat.Theory.RelativeComonadWithCut]
_ ⋅cut[ _ ] [notation, in Cat.Theory.RelativeComonadWithCut]
_ ⋅cut [notation, in Cat.Theory.RelativeComonadWithCut]
_ ∘ _ [notation, in Cat.Category.Types]
_ ⇒ _ [notation, in Cat.Category.Types]
BinaryProduct.make ⦃ Category ≔ _ ; _×_ ≔ _ ; ⟨_,_⟩ ≔ _ ; π₁ ≔ _ ; π₂ ≔ _ ⦄ [notation, in Cat.Theory.Product]
CartesianStrongMonoidal.make ⦃ φ ≔ _ ⦄ [notation, in Cat.Theory.CartesianStrongMonoidal]
Category.make ⦃ Hom ≔ _ ; id ≔ _ ; compose ≔ _ ⦄ [notation, in Cat.Theory.Category]
Comodule.make ⦃ α ≔ _ ⦄ [notation, in Cat.Theory.Comodule]
Comodule.make ⦃ M ≔ _ ; mcobind ≔ _ ⦄ [notation, in Cat.Theory.Comodule]
counit[ _ ] [notation, in Cat.Theory.RelativeComonad]
cut[ _ ] [notation, in Cat.Theory.RelativeComonadWithCut]
Functor.make ⦃ F ≔ _ ; map ≔ _ ⦄ [notation, in Cat.Theory.Functor]
id[ _ ] [notation, in Cat.Theory.Category]
Initial.make ⦃ empty ≔ _ ; bottom ≔ _ ⦄ [notation, in Cat.Theory.InitialTerminal]
Iso.make ⦃ from ≔ _ ; to ≔ _ ⦄ [notation, in Cat.Theory.Isomorphism]
NaturalTransformation.make ⦃ η ≔ _ ⦄ [notation, in Cat.Theory.NaturalTransformation]
RelativeComonadWithCut.make ⦃ τ ≔ _ ⦄ [notation, in Cat.Theory.RelativeComonadWithCut]
RelativeComonadWithCut.make ⦃ RelativeComonad-τ ≔ _ ⦄ [notation, in Cat.Theory.RelativeComonadWithCut]
RelativeComonadWithCut.make ⦃ T ≔ _ ; counit ≔ _ ; cobind ≔ _ ; cut ≔ _ ⦄ [notation, in Cat.Theory.RelativeComonadWithCut]
RelativeComonadWithCut.make ⦃ RelativeComonad ≔ _ ; cut ≔ _ ⦄ [notation, in Cat.Theory.RelativeComonadWithCut]
RelativeComonad.make ⦃ τ ≔ _ ⦄ [notation, in Cat.Theory.RelativeComonad]
RelativeComonad.make ⦃ T ≔ _ ; counit ≔ _ ; cobind ≔ _ ⦄ [notation, in Cat.Theory.RelativeComonad]
Terminal.make ⦃ one ≔ _ ; top ≔ _ ⦄ [notation, in Cat.Theory.InitialTerminal]
_𝘅_ [notation, in Cat.Theory.Category]
_∘_ [notation, in Cat.Theory.Category]
_⇒_ [notation, in Cat.Theory.Category]
_⟨×⟩_ [notation, in Cat.Theory.Notations]
_⟨⊎⟩_ [notation, in Cat.Theory.Notations]
!-⊤ [notation, in Cat.Theory.InitialTerminal]
!-⊥ [notation, in Cat.Theory.InitialTerminal]
[ _ ] [notation, in Cat.Theory.PushforwardComodule]
‵ _ ′ [notation, in Cat.Theory.Notations]
↑[ _ ; _ ] [notation, in Cat.Theory.RelativeComonadWithCut]
↑[ _ ] [notation, in Cat.Theory.RelativeComonadWithCut]
∘-× [notation, in Cat.Theory.Product]
≅-refl [notation, in Cat.Theory.Isomorphism]
≅-sym [notation, in Cat.Theory.Isomorphism]
≅-trans [notation, in Cat.Theory.Isomorphism]
⊤ [notation, in Cat.Theory.Notations]
⊤-unique [notation, in Cat.Theory.InitialTerminal]
⊥ [notation, in Cat.Theory.Notations]
⊥-unique [notation, in Cat.Theory.InitialTerminal]
⟨ _ ⟩ [notation, in Cat.Theory.PushforwardComodule]
⟨ _ , _ ⟩ [notation, in Cat.Theory.Product]
⟨⊤⟩ [notation, in Cat.Theory.InitialTerminal]
⟨⊥⟩ [notation, in Cat.Theory.InitialTerminal]
×-∘ [notation, in Cat.Theory.Product]
λ _ .. _ ∙ _ [notation, in Cat.Misc.Unicode]
π₁[ _ , _ ] [notation, in Cat.Theory.Product]
π₂[ _ , _ ] [notation, in Cat.Theory.Product]
𝑬𝑸-𝘅 [notation, in Cat.Category.Types_Setoids]
Π [module, in Cat.Theory.SetoidType]
Π.compose [definition, in Cat.Theory.SetoidType]
Π.cong [lemma, in Cat.Theory.SetoidType]
Π.id [definition, in Cat.Theory.SetoidType]
Π.make [abbreviation, in Cat.Theory.SetoidType]
Π.map [projection, in Cat.Theory.SetoidType]
Π.map_proper [projection, in Cat.Theory.SetoidType]
Π.mkΠ [constructor, in Cat.Theory.SetoidType]
Π.setoid [definition, in Cat.Theory.SetoidType]
[ _ ⟶ _ ] [notation, in Cat.Theory.SetoidType]
λ _ .. _ ↦ _ [notation, in Cat.Theory.SetoidType]
Π.Π [record, in Cat.Theory.SetoidType]
Π₂ [module, in Cat.Theory.SetoidType]
Π₂.cong [lemma, in Cat.Theory.SetoidType]
Π₂.make [abbreviation, in Cat.Theory.SetoidType]
Π₂.map [projection, in Cat.Theory.SetoidType]
Π₂.map_compose [projection, in Cat.Theory.SetoidType]
Π₂.mkΠ₂ [constructor, in Cat.Theory.SetoidType]
[ _ ⟶ _ ⟶ _ ] [notation, in Cat.Theory.SetoidType]
λ _ .. _ ↦₂ _ [notation, in Cat.Theory.SetoidType]
Π₂.Π₂ [record, in Cat.Theory.SetoidType]
Φ [definition, in Cat.Theory.PushforwardComodule]
α [projection, in Cat.Theory.Comodule]
α_commutes [projection, in Cat.Theory.Comodule]
η [projection, in Cat.Theory.NaturalTransformation]
η_commutes [projection, in Cat.Theory.NaturalTransformation]
π₁ [abbreviation, in Cat.Theory.Category]
π₁ [projection, in Cat.Theory.Product]
π₁_compose [projection, in Cat.Theory.Product]
π₂ [abbreviation, in Cat.Theory.Category]
π₂ [projection, in Cat.Theory.Product]
π₂_compose [projection, in Cat.Theory.Product]
τ [projection, in Cat.Theory.RelativeComonad]
τ [projection, in Cat.Theory.RelativeComonadWithCut]
τ_commutes [projection, in Cat.Theory.RelativeComonad]
τ_counit [projection, in Cat.Theory.RelativeComonad]
τ_cut [projection, in Cat.Theory.RelativeComonadWithCut]
φ [definition, in Cat.Theory.CartesianStrongMonoidal]
φ_is_inverse [projection, in Cat.Theory.CartesianStrongMonoidal]
φ_inv [projection, in Cat.Theory.CartesianStrongMonoidal]
𝑪𝒖𝒕 [definition, in Cat.Category.RComonad_RComonadWithCut]
𝑬𝑸 [definition, in Cat.Category.Types_Setoids]
𝑬𝑸_prod [definition, in Cat.Category.Types_Setoids]
𝑬𝑸_SM [instance, in Cat.Category.Types_Setoids]
𝑹𝑪𝒐𝒎𝒐𝒅 [definition, in Cat.Category.RComod]
𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅 [definition, in Cat.Category.RComonad]
𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅𝑾𝒊𝒕𝒉𝑪𝒖𝒕 [definition, in Cat.Category.RComonadWithCut]
𝑺𝒆𝒕𝒐𝒊𝒅 [definition, in Cat.Category.Setoids]
𝑺𝒆𝒕𝒐𝒊𝒅_BinaryProduct [instance, in Cat.Category.Setoids]
𝑺𝒕𝒓𝒆𝒂𝒎 [definition, in Cat.Category.Stream.Category]
𝑻𝒓𝒊𝑴𝒂𝒕 [definition, in Cat.Category.TriMat.Category]
𝑻𝒚𝒑𝒆 [definition, in Cat.Category.Types]
𝑻𝒚𝒑𝒆_BinaryProduct [instance, in Cat.Category.Types]
𝑼 [definition, in Cat.Category.RComonad_RComonadWithCut]

Notation Index

D

_ ∘ _ [in Cat.Category.RComonadWithCut]
_ ⇒ _ [in Cat.Category.RComonadWithCut]
_ ∘ _ [in Cat.Category.RComonad]
_ ⇒ _ [in Cat.Category.RComonad]
_ ∘ _ [in Cat.Category.RComod]
_ ⇒ _ [in Cat.Category.RComod]
_ ∘ _ [in Cat.Category.Stream.Category]
_ ⇒ _ [in Cat.Category.Stream.Category]
_ ∘ _ [in Cat.Category.TriMat.Category]
_ ⇒ _ [in Cat.Category.TriMat.Category]

F

_ ⁎ _ [in Cat.Theory.PushforwardComodule]

M

[ _ ] [in Cat.Theory.RelativeComonadWithCut]
_ ⇒ _ [in Cat.Theory.Comodule]
_ ⇒ _ [in Cat.Theory.RelativeComonad]
_ ⇒ _ [in Cat.Theory.RelativeComonadWithCut]

P

_ ∼ _ [in Cat.Category.Setoids]

S

Setoids.make ⦃ Carrier ≔ _ ; Equiv ≔ _ ⦄ [in Cat.Category.Setoids]
_ ≉ _ [in Cat.Theory.SetoidType]
_ ≈ _ [in Cat.Theory.SetoidType]
_ ≈ _ :> _ [in Cat.Theory.SetoidType]
Setoid.make ⦃ Carrier ≔ _ ; Equiv ≔ _ ⦄ [in Cat.Theory.SetoidType]
_≈_ [in Cat.Theory.SetoidType]
_ ∼ _ [in Cat.Category.Stream.Axioms]
∼-head [in Cat.Category.Stream.Axioms]
∼-tail [in Cat.Category.Stream.Axioms]
_ ∼ _ [in Cat.Category.Stream.Model]
_ ∷ _ [in Cat.Category.Stream.Model]
_∷_ [in Cat.Category.Stream.Model]
_ ∼ _ [in Cat.Category.Stream.Terminality]
STR⋅tail [in Cat.Category.Stream.Terminality]
STR⋅tail[ _ ] [in Cat.Category.Stream.Terminality]
T⋅tail [in Cat.Category.Stream.Terminality]
T⋅tail[ _ ] [in Cat.Category.Stream.Terminality]
⟨ _ ⟩ [in Cat.Category.Stream.Terminality]
Stream.make ⦃ τ ≔ _ ⦄ [in Cat.Category.Stream.Category]
Stream.make ⦃ T ≔ _ ; tail ≔ _ ⦄ [in Cat.Category.Stream.Category]

T

_ ∼ _ [in Cat.Category.TriMat.Model]
∼-rest [in Cat.Category.TriMat.Model]
∼-top [in Cat.Category.TriMat.Model]
_ ∼ _ [in Cat.Category.TriMat.Axioms]
∼-rest [in Cat.Category.TriMat.Axioms]
∼-top [in Cat.Category.TriMat.Axioms]
_ ∼ _ [in Cat.Category.TriMat.Terminality]
TRI⋅rest [in Cat.Category.TriMat.Terminality]
TRI⋅rest[ _ ] [in Cat.Category.TriMat.Terminality]
T⋅rest [in Cat.Category.TriMat.Terminality]
T⋅rest[ _ ] [in Cat.Category.TriMat.Terminality]
⟨ _ ⟩ [in Cat.Category.TriMat.Terminality]
TriMat.make ⦃ τ ≔ _ ⦄ [in Cat.Category.TriMat.Category]
TriMat.make ⦃ T ≔ _ ; rest ≔ _ ⦄ [in Cat.Category.TriMat.Category]

other

_ ≠ _ (type_scope) [in Cat.Misc.Unicode]
¬ _ (type_scope) [in Cat.Misc.Unicode]
_ ↔ _ (type_scope) [in Cat.Misc.Unicode]
_ → _ (type_scope) [in Cat.Misc.Unicode]
_ ∧ _ (type_scope) [in Cat.Misc.Unicode]
_ ∨ _ (type_scope) [in Cat.Misc.Unicode]
∃ _ .. _ , _ (type_scope) [in Cat.Misc.Unicode]
∀ _ .. _ , _ (type_scope) [in Cat.Misc.Unicode]
_ ⁎ [in Cat.Theory.PushforwardComodule]
_ ⋅mcobind [in Cat.Theory.Comodule]
_ ⋅ _ [in Cat.Theory.Functor]
_ ［ _ ×─ ］ [in Cat.Theory.PrecompositionWithProduct]
_ [ _ ×─ ] [in Cat.Theory.PrecompositionWithProduct]
_ 𝘅 _ [in Cat.Theory.Category]
_ -id[ _ ] [in Cat.Theory.Category]
_ -id [in Cat.Theory.Category]
_ ∘ _ [in Cat.Theory.Category]
_ ⇒ _ [in Cat.Theory.Category]
_ ⋅cobind [in Cat.Theory.RelativeComonad]
_ ⋅counit[ _ ] [in Cat.Theory.RelativeComonad]
_ ⋅counit [in Cat.Theory.RelativeComonad]
_ ⟨×⟩ _ [in Cat.Theory.Notations]
_ ⟨⊎⟩ _ [in Cat.Theory.Notations]
_ ∘ _ [in Cat.Category.Setoids]
_ ⇒ _ [in Cat.Category.Setoids]
_ ⋅≅-right [in Cat.Theory.Isomorphism]
_ ⋅≅-left [in Cat.Theory.Isomorphism]
_ ≅ _ [in Cat.Theory.Isomorphism]
_ ⁻¹ [in Cat.Theory.Isomorphism]
_ -×- _ [in Cat.Theory.Product]
_ × _ [in Cat.Theory.Product]
_ ⋅π₂ [in Cat.Theory.Product]
_ ⋅π₁ [in Cat.Theory.Product]
_ ⋅extend [in Cat.Theory.RelativeComonadWithCut]
_ ⋅cut[ _ ] [in Cat.Theory.RelativeComonadWithCut]
_ ⋅cut [in Cat.Theory.RelativeComonadWithCut]
_ ∘ _ [in Cat.Category.Types]
_ ⇒ _ [in Cat.Category.Types]
BinaryProduct.make ⦃ Category ≔ _ ; _×_ ≔ _ ; ⟨_,_⟩ ≔ _ ; π₁ ≔ _ ; π₂ ≔ _ ⦄ [in Cat.Theory.Product]
CartesianStrongMonoidal.make ⦃ φ ≔ _ ⦄ [in Cat.Theory.CartesianStrongMonoidal]
Category.make ⦃ Hom ≔ _ ; id ≔ _ ; compose ≔ _ ⦄ [in Cat.Theory.Category]
Comodule.make ⦃ α ≔ _ ⦄ [in Cat.Theory.Comodule]
Comodule.make ⦃ M ≔ _ ; mcobind ≔ _ ⦄ [in Cat.Theory.Comodule]
counit[ _ ] [in Cat.Theory.RelativeComonad]
cut[ _ ] [in Cat.Theory.RelativeComonadWithCut]
Functor.make ⦃ F ≔ _ ; map ≔ _ ⦄ [in Cat.Theory.Functor]
id[ _ ] [in Cat.Theory.Category]
Initial.make ⦃ empty ≔ _ ; bottom ≔ _ ⦄ [in Cat.Theory.InitialTerminal]
Iso.make ⦃ from ≔ _ ; to ≔ _ ⦄ [in Cat.Theory.Isomorphism]
NaturalTransformation.make ⦃ η ≔ _ ⦄ [in Cat.Theory.NaturalTransformation]
RelativeComonadWithCut.make ⦃ τ ≔ _ ⦄ [in Cat.Theory.RelativeComonadWithCut]
RelativeComonadWithCut.make ⦃ RelativeComonad-τ ≔ _ ⦄ [in Cat.Theory.RelativeComonadWithCut]
RelativeComonadWithCut.make ⦃ T ≔ _ ; counit ≔ _ ; cobind ≔ _ ; cut ≔ _ ⦄ [in Cat.Theory.RelativeComonadWithCut]
RelativeComonadWithCut.make ⦃ RelativeComonad ≔ _ ; cut ≔ _ ⦄ [in Cat.Theory.RelativeComonadWithCut]
RelativeComonad.make ⦃ τ ≔ _ ⦄ [in Cat.Theory.RelativeComonad]
RelativeComonad.make ⦃ T ≔ _ ; counit ≔ _ ; cobind ≔ _ ⦄ [in Cat.Theory.RelativeComonad]
Terminal.make ⦃ one ≔ _ ; top ≔ _ ⦄ [in Cat.Theory.InitialTerminal]
_𝘅_ [in Cat.Theory.Category]
_∘_ [in Cat.Theory.Category]
_⇒_ [in Cat.Theory.Category]
_⟨×⟩_ [in Cat.Theory.Notations]
_⟨⊎⟩_ [in Cat.Theory.Notations]
!-⊤ [in Cat.Theory.InitialTerminal]
!-⊥ [in Cat.Theory.InitialTerminal]
[ _ ] [in Cat.Theory.PushforwardComodule]
‵ _ ′ [in Cat.Theory.Notations]
↑[ _ ; _ ] [in Cat.Theory.RelativeComonadWithCut]
↑[ _ ] [in Cat.Theory.RelativeComonadWithCut]
∘-× [in Cat.Theory.Product]
≅-refl [in Cat.Theory.Isomorphism]
≅-sym [in Cat.Theory.Isomorphism]
≅-trans [in Cat.Theory.Isomorphism]
⊤ [in Cat.Theory.Notations]
⊤-unique [in Cat.Theory.InitialTerminal]
⊥ [in Cat.Theory.Notations]
⊥-unique [in Cat.Theory.InitialTerminal]
⟨ _ ⟩ [in Cat.Theory.PushforwardComodule]
⟨ _ , _ ⟩ [in Cat.Theory.Product]
⟨⊤⟩ [in Cat.Theory.InitialTerminal]
⟨⊥⟩ [in Cat.Theory.InitialTerminal]
×-∘ [in Cat.Theory.Product]
λ _ .. _ ∙ _ [in Cat.Misc.Unicode]
π₁[ _ , _ ] [in Cat.Theory.Product]
π₂[ _ , _ ] [in Cat.Theory.Product]
𝑬𝑸-𝘅 [in Cat.Category.Types_Setoids]
[ _ ⟶ _ ] [in Cat.Theory.SetoidType]
λ _ .. _ ↦ _ [in Cat.Theory.SetoidType]
[ _ ⟶ _ ⟶ _ ] [in Cat.Theory.SetoidType]
λ _ .. _ ↦₂ _ [in Cat.Theory.SetoidType]

Module Index

D

Diag [in Cat.Category.Diag]
Diag.Str [in Cat.Category.Diag]
Diag.Tri [in Cat.Category.Diag]

M

Morphism [in Cat.Theory.Comodule]
Morphism [in Cat.Theory.RelativeComonad]
Morphism [in Cat.Theory.RelativeComonadWithCut]

S

Setoid [in Cat.Theory.SetoidType]
Setoids [in Cat.Category.Setoids]
Setoids.Morphism [in Cat.Category.Setoids]
Stream [in Cat.Category.Stream.Category]
StreamAxioms [in Cat.Category.Stream.Axioms]
StreamInstance [in Cat.Category.Stream.Model]
StreamTerminal [in Cat.Category.Stream.Terminality]

T

Terminality [in Cat.Category.TriMat.Model]
Terminality [in Cat.Category.Stream.Model]
TriInstance [in Cat.Category.TriMat.Model]
TriMat [in Cat.Category.TriMat.Category]
TriMatAxioms [in Cat.Category.TriMat.Axioms]
TriMatTerminal [in Cat.Category.TriMat.Terminality]

other

Π [in Cat.Theory.SetoidType]
Π₂ [in Cat.Theory.SetoidType]

Variable Index

D

Defs.E [in Cat.Category.TriMat.Category]

S

StreamTerminal.Defs.Tr [in Cat.Category.Stream.Terminality]

T

TriMatTerminal.Defs.Tr [in Cat.Category.TriMat.Terminality]

Library Index

A

C

CartesianStrongMonoidal
Category
Category
Category
Comodule
Cut_NT

D

Diag

F

I

InitialTerminal
Isomorphism

M

N

NaturalTransformation
Notations

P

PrecompositionWithProduct
Product
PushforwardComodule

R

RComod
RComonad
RComonadWithCut
RComonad_RComonadWithCut
RelativeComonad
RelativeComonadWithCut

S

Setoids
SetoidType

T

Terminality
Terminality
Types
Types_Setoids

U

Lemma Index

C

compose_assoc [in Cat.Category.RComonadWithCut]
compose_assoc [in Cat.Category.Stream.Category]
compose_assoc [in Cat.Category.TriMat.Category]
compose_assoc [in Cat.Category.RComonad]
compose_assoc [in Cat.Category.Setoids]
compose_assoc [in Cat.Category.RComod]
compose_assoc [in Cat.Category.Types]

F

Fπ₁_φ_inv [in Cat.Theory.CartesianStrongMonoidal]
Fπ₂_φ_inv [in Cat.Theory.CartesianStrongMonoidal]

I

id [in Cat.Category.Types_Setoids]

L

left_id [in Cat.Category.RComonadWithCut]
left_id [in Cat.Category.Stream.Category]
left_id [in Cat.Category.TriMat.Category]
left_id [in Cat.Category.RComonad]
left_id [in Cat.Category.Setoids]
left_id [in Cat.Category.RComod]
left_id [in Cat.Category.Types]
lift_compose [in Cat.Theory.RelativeComonad]
lift_id [in Cat.Theory.RelativeComonad]

M

map_compose [in Cat.Category.Types_Setoids]
mlift_compose [in Cat.Theory.Comodule]
mlift_id [in Cat.Theory.Comodule]

P

product_precompose [in Cat.Theory.Product]
product_postcompose [in Cat.Theory.Product]

R

right_id [in Cat.Category.RComonadWithCut]
right_id [in Cat.Category.Stream.Category]
right_id [in Cat.Category.TriMat.Category]
right_id [in Cat.Category.RComonad]
right_id [in Cat.Category.Setoids]
right_id [in Cat.Category.RComod]
right_id [in Cat.Category.Types]

S

StreamInstance.bisim_intro [in Cat.Category.Stream.Model]
StreamInstance.bisim_tail [in Cat.Category.Stream.Model]
StreamInstance.bisim_head [in Cat.Category.Stream.Model]
StreamInstance.head_corec [in Cat.Category.Stream.Model]
StreamInstance.tail_corec [in Cat.Category.Stream.Model]
StreamTerminal.bisim_trans [in Cat.Category.Stream.Terminality]
StreamTerminal.bisim_sym [in Cat.Category.Stream.Terminality]
StreamTerminal.bisim_refl [in Cat.Category.Stream.Terminality]
StreamTerminal.eq_bisim [in Cat.Category.Stream.Terminality]
StreamTerminal.head_tau [in Cat.Category.Stream.Terminality]
StreamTerminal.head_cong [in Cat.Category.Stream.Terminality]
StreamTerminal.tail_tau [in Cat.Category.Stream.Terminality]
StreamTerminal.tail_cong [in Cat.Category.Stream.Terminality]
StreamTerminal.tau_cobind [in Cat.Category.Stream.Terminality]
StreamTerminal.tau_counit [in Cat.Category.Stream.Terminality]
StreamTerminal.tau_cong [in Cat.Category.Stream.Terminality]

T

TriInstance.bisim_intro [in Cat.Category.TriMat.Model]
TriInstance.bisim_rest [in Cat.Category.TriMat.Model]
TriInstance.bisim_top [in Cat.Category.TriMat.Model]
TriInstance.rest_corec [in Cat.Category.TriMat.Model]
TriInstance.top_corec [in Cat.Category.TriMat.Model]
TriMatTerminal.bisim_intro_bis [in Cat.Category.TriMat.Terminality]
TriMatTerminal.bisim_trans [in Cat.Category.TriMat.Terminality]
TriMatTerminal.bisim_sym [in Cat.Category.TriMat.Terminality]
TriMatTerminal.bisim_refl [in Cat.Category.TriMat.Terminality]
TriMatTerminal.cut_cong [in Cat.Category.TriMat.Terminality]
TriMatTerminal.eq_bisim [in Cat.Category.TriMat.Terminality]
TriMatTerminal.lift_ext [in Cat.Category.TriMat.Terminality]
TriMatTerminal.lift_cong [in Cat.Category.TriMat.Terminality]
TriMatTerminal.redec_cut [in Cat.Category.TriMat.Terminality]
TriMatTerminal.redec_ext [in Cat.Category.TriMat.Terminality]
TriMatTerminal.redec_cong [in Cat.Category.TriMat.Terminality]
TriMatTerminal.rest_tau [in Cat.Category.TriMat.Terminality]
TriMatTerminal.rest_redec [in Cat.Category.TriMat.Terminality]
TriMatTerminal.rest_cut [in Cat.Category.TriMat.Terminality]
TriMatTerminal.rest_cong [in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau_cobind [in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau_cut [in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau_counit [in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau_cong [in Cat.Category.TriMat.Terminality]
TriMatTerminal.top_tau [in Cat.Category.TriMat.Terminality]
TriMatTerminal.top_redec [in Cat.Category.TriMat.Terminality]
TriMatTerminal.top_cut [in Cat.Category.TriMat.Terminality]
TriMatTerminal.top_cong [in Cat.Category.TriMat.Terminality]

other

Π.cong [in Cat.Theory.SetoidType]
Π₂.cong [in Cat.Theory.SetoidType]

Constructor Index

M

mkCartesianStrongMonoidal [in Cat.Theory.CartesianStrongMonoidal]
mkCategory [in Cat.Theory.Category]
mkComodule [in Cat.Theory.Comodule]
mkFunctor [in Cat.Theory.Functor]
mkInitial [in Cat.Theory.InitialTerminal]
mkInverse [in Cat.Theory.Isomorphism]
mkIso [in Cat.Theory.Isomorphism]
mkMorphism [in Cat.Theory.Comodule]
mkMorphism [in Cat.Theory.RelativeComonad]
mkMorphism [in Cat.Theory.RelativeComonadWithCut]
mkNaturalTransformation [in Cat.Theory.NaturalTransformation]
mkProduct [in Cat.Theory.Product]
mkRelativeComonad [in Cat.Theory.RelativeComonad]
mkRelativeComonadWithCut [in Cat.Theory.RelativeComonadWithCut]
mkTerminal [in Cat.Theory.InitialTerminal]

P

product [in Cat.Theory.Product]

S

Setoids.mkMorphism [in Cat.Category.Setoids]
Setoids.mkObj [in Cat.Category.Setoids]
Setoid.mkSetoid [in Cat.Theory.SetoidType]
StreamInstance.bintro [in Cat.Category.Stream.Model]
StreamInstance.Cons [in Cat.Category.Stream.Model]
Stream.mkMorphism [in Cat.Category.Stream.Category]
Stream.mkObj [in Cat.Category.Stream.Category]

T

TriInstance.bisim_constr [in Cat.Category.TriMat.Model]
TriInstance.constr [in Cat.Category.TriMat.Model]
TriMat.mkMorphism [in Cat.Category.TriMat.Category]
TriMat.mkObj [in Cat.Category.TriMat.Category]

other

Π.mkΠ [in Cat.Theory.SetoidType]
Π₂.mkΠ₂ [in Cat.Theory.SetoidType]

Axiom Index

S

StreamAxioms.bisim [in Cat.Category.Stream.Axioms]
StreamAxioms.bisim_intro [in Cat.Category.Stream.Axioms]
StreamAxioms.bisim_tail [in Cat.Category.Stream.Axioms]
StreamAxioms.bisim_head [in Cat.Category.Stream.Axioms]
StreamAxioms.corec [in Cat.Category.Stream.Axioms]
StreamAxioms.head [in Cat.Category.Stream.Axioms]
StreamAxioms.head_corec [in Cat.Category.Stream.Axioms]
StreamAxioms.Stream [in Cat.Category.Stream.Axioms]
StreamAxioms.tail [in Cat.Category.Stream.Axioms]
StreamAxioms.tail_corec [in Cat.Category.Stream.Axioms]

T

TriMatAxioms.bisim [in Cat.Category.TriMat.Axioms]
TriMatAxioms.bisim_intro [in Cat.Category.TriMat.Axioms]
TriMatAxioms.bisim_rest [in Cat.Category.TriMat.Axioms]
TriMatAxioms.bisim_top [in Cat.Category.TriMat.Axioms]
TriMatAxioms.corec [in Cat.Category.TriMat.Axioms]
TriMatAxioms.rest [in Cat.Category.TriMat.Axioms]
TriMatAxioms.rest_corec [in Cat.Category.TriMat.Axioms]
TriMatAxioms.top [in Cat.Category.TriMat.Axioms]
TriMatAxioms.top_corec [in Cat.Category.TriMat.Axioms]
TriMatAxioms.Tri [in Cat.Category.TriMat.Axioms]

Projection Index

A

AxB [in Cat.Theory.Product]

B

bottom [in Cat.Theory.InitialTerminal]
bottom_unique [in Cat.Theory.InitialTerminal]

C

cobind [in Cat.Theory.RelativeComonad]
cobind_cobind [in Cat.Theory.RelativeComonad]
cobind_counit [in Cat.Theory.RelativeComonad]
compose [in Cat.Theory.Category]
compose_assoc [in Cat.Theory.Category]
counit [in Cat.Theory.RelativeComonad]
counit_cobind [in Cat.Theory.RelativeComonad]
cut [in Cat.Theory.RelativeComonadWithCut]
cut_cobind [in Cat.Theory.RelativeComonadWithCut]
cut_counit [in Cat.Theory.RelativeComonadWithCut]

E

empty [in Cat.Theory.InitialTerminal]

F

F [in Cat.Theory.Functor]

H

Hom [in Cat.Theory.Category]

I

id [in Cat.Theory.Category]
identity [in Cat.Theory.Functor]
iso_inverse [in Cat.Theory.Isomorphism]
iso_to [in Cat.Theory.Isomorphism]
iso_from [in Cat.Theory.Isomorphism]
iso_right [in Cat.Theory.Isomorphism]
iso_left [in Cat.Theory.Isomorphism]

L

left_id [in Cat.Theory.Category]

M

M [in Cat.Theory.Comodule]
map [in Cat.Theory.Functor]
map_compose [in Cat.Theory.Functor]
mcobind [in Cat.Theory.Comodule]
mcobind_mcobind [in Cat.Theory.Comodule]
mcobind_counit [in Cat.Theory.Comodule]

O

Obj [in Cat.Theory.Category]
one [in Cat.Theory.InitialTerminal]

P

Pmor [in Cat.Theory.Product]
Pmor_universal [in Cat.Theory.Product]
product [in Cat.Theory.Product]

R

right_id [in Cat.Theory.Category]

S

Setoids.cong [in Cat.Category.Setoids]
Setoids.is_SEquiv [in Cat.Category.Setoids]
Setoids.map [in Cat.Category.Setoids]
Setoids.SCarrier [in Cat.Category.Setoids]
Setoids.SEquiv [in Cat.Category.Setoids]
Setoid.Carrier [in Cat.Theory.SetoidType]
Setoid.Equiv [in Cat.Theory.SetoidType]
Setoid.is_Equiv [in Cat.Theory.SetoidType]
Stream.T [in Cat.Category.Stream.Category]
Stream.tail [in Cat.Category.Stream.Category]
Stream.τ [in Cat.Category.Stream.Category]
Stream.τ_commutes [in Cat.Category.Stream.Category]

T

T [in Cat.Theory.RelativeComonad]
T [in Cat.Theory.RelativeComonadWithCut]
top [in Cat.Theory.InitialTerminal]
top_unique [in Cat.Theory.InitialTerminal]
TriMat.rest [in Cat.Category.TriMat.Category]
TriMat.rest_cut [in Cat.Category.TriMat.Category]
TriMat.T [in Cat.Category.TriMat.Category]
TriMat.τ [in Cat.Category.TriMat.Category]
TriMat.τ_commutes [in Cat.Category.TriMat.Category]

other

Π.map [in Cat.Theory.SetoidType]
Π.map_proper [in Cat.Theory.SetoidType]
Π₂.map [in Cat.Theory.SetoidType]
Π₂.map_compose [in Cat.Theory.SetoidType]
α [in Cat.Theory.Comodule]
α_commutes [in Cat.Theory.Comodule]
η [in Cat.Theory.NaturalTransformation]
η_commutes [in Cat.Theory.NaturalTransformation]
π₁ [in Cat.Theory.Product]
π₁_compose [in Cat.Theory.Product]
π₂ [in Cat.Theory.Product]
π₂_compose [in Cat.Theory.Product]
τ [in Cat.Theory.RelativeComonad]
τ [in Cat.Theory.RelativeComonadWithCut]
τ_commutes [in Cat.Theory.RelativeComonad]
τ_counit [in Cat.Theory.RelativeComonad]
τ_cut [in Cat.Theory.RelativeComonadWithCut]
φ_is_inverse [in Cat.Theory.CartesianStrongMonoidal]
φ_inv [in Cat.Theory.CartesianStrongMonoidal]

Inductive Index

B

BinaryProduct [in Cat.Theory.Product]

S

StreamInstance.bisim_ [in Cat.Category.Stream.Model]
StreamInstance.Stream_ [in Cat.Category.Stream.Model]

T

TriInstance.bisim_ [in Cat.Category.TriMat.Model]
TriInstance.Tri_ [in Cat.Category.TriMat.Model]

Section Index

C

CanonicalCut [in Cat.Theory.RelativeComonadWithCut]
Commutes [in Cat.Theory.PushforwardComodule]

D

Definitions [in Cat.Category.RComonadWithCut]
Definitions [in Cat.Category.RComonad]
Definitions [in Cat.Category.RComod]
Defs [in Cat.Category.RComonad_RComonadWithCut]
Defs [in Cat.Category.Stream.Category]
Defs [in Cat.Category.TriMat.Category]
Defs [in Cat.Theory.RelativeComonadWithCut]
Defs.ExtendConstruction [in Cat.Theory.RelativeComonadWithCut]

E

equations [in Cat.Theory.CartesianStrongMonoidal]

F

Functoriality [in Cat.Theory.PushforwardComodule]
Functoriality [in Cat.Theory.Comodule]
Functoriality [in Cat.Theory.RelativeComonad]

I

induced_morphism [in Cat.Theory.PushforwardComodule]
Iso_Equivalence [in Cat.Theory.Isomorphism]

M

MDefs [in Cat.Theory.RelativeComonadWithCut]
Morphisms [in Cat.Theory.PrecompositionWithProduct]
Morphism.id_composition [in Cat.Theory.Comodule]
Morphism.id_composition [in Cat.Theory.RelativeComonad]
Morphism.id_composition [in Cat.Theory.RelativeComonadWithCut]

P

PrecompositionWithProduct [in Cat.Theory.PrecompositionWithProduct]
Product_construction [in Cat.Category.Setoids]
Pushforward_construction [in Cat.Theory.PushforwardComodule]

S

StreamTerminal.Defs [in Cat.Category.Stream.Terminality]
StrongMonoidal [in Cat.Theory.CartesianStrongMonoidal]

T

tautological_comodule [in Cat.Theory.PushforwardComodule]
TriMatTerminal.Defs [in Cat.Category.TriMat.Terminality]

Instance Index

S

Setoids.map_Proper [in Cat.Category.Setoids]
StreamTerminal.bisim_equiv [in Cat.Category.Stream.Terminality]

T

TriMatTerminal.bisim_equiv [in Cat.Category.TriMat.Terminality]

other

𝑬𝑸_SM [in Cat.Category.Types_Setoids]
𝑺𝒆𝒕𝒐𝒊𝒅_BinaryProduct [in Cat.Category.Setoids]
𝑻𝒚𝒑𝒆_BinaryProduct [in Cat.Category.Types]

Abbreviation Index

S

Setoids.Morphism.make [in Cat.Category.Setoids]
StreamTerminal.STR [in Cat.Category.Stream.Terminality]
StreamTerminal.T [in Cat.Category.Stream.Terminality]

T

TriInstance.E [in Cat.Category.TriMat.Model]
TriMatAxioms.E [in Cat.Category.TriMat.Axioms]
TriMatTerminal.coRec [in Cat.Category.TriMat.Terminality]
TriMatTerminal.E [in Cat.Category.TriMat.Terminality]
TriMatTerminal.T [in Cat.Category.TriMat.Terminality]
TriMatTerminal.TRI [in Cat.Category.TriMat.Terminality]

other

Π.make [in Cat.Theory.SetoidType]
Π₂.make [in Cat.Theory.SetoidType]
π₁ [in Cat.Theory.Category]
π₂ [in Cat.Theory.Category]

Definition Index

C

ccut [in Cat.Theory.RelativeComonadWithCut]
compose [in Cat.Category.Stream.Category]
compose [in Cat.Category.TriMat.Category]
compose [in Cat.Category.Setoids]
compose [in Cat.Category.Types]

D

Diag.𝒅𝒊𝒂𝒈 [in Cat.Category.Diag]

E

extend [in Cat.Theory.RelativeComonadWithCut]
Extend [in Cat.Theory.RelativeComonadWithCut]

F

F [in Cat.Category.Types_Setoids]

H

Hom [in Cat.Category.Types]

I

id [in Cat.Category.Stream.Category]
id [in Cat.Category.TriMat.Category]
id [in Cat.Category.Setoids]
id [in Cat.Category.Types]
induced_morphism [in Cat.Theory.PushforwardComodule]
inverse_of [in Cat.Theory.Isomorphism]

L

Lift [in Cat.Theory.RelativeComonad]
lift [in Cat.Theory.RelativeComonad]

M

map [in Cat.Category.Types_Setoids]
MLift [in Cat.Theory.Comodule]
mlift [in Cat.Theory.Comodule]
Morphism.compose [in Cat.Theory.Comodule]
Morphism.compose [in Cat.Theory.RelativeComonad]
Morphism.compose [in Cat.Theory.RelativeComonadWithCut]
Morphism.Hom [in Cat.Theory.Comodule]
Morphism.Hom [in Cat.Theory.RelativeComonad]
Morphism.Hom [in Cat.Theory.RelativeComonadWithCut]
Morphism.id [in Cat.Theory.Comodule]
Morphism.id [in Cat.Theory.RelativeComonad]
Morphism.id [in Cat.Theory.RelativeComonadWithCut]

P

precomposition_with_product_mor [in Cat.Theory.PrecompositionWithProduct]
precomposition_with_product [in Cat.Theory.PrecompositionWithProduct]
product [in Cat.Category.Setoids]
product_mor [in Cat.Category.Setoids]
prod_cat [in Cat.Theory.Category]
prod_on_arrow [in Cat.Theory.Product]
proj_r [in Cat.Category.Setoids]
proj_l [in Cat.Category.Setoids]
Pushforward [in Cat.Theory.PushforwardComodule]
pushforward [in Cat.Theory.PushforwardComodule]
pushforward_mor [in Cat.Theory.PushforwardComodule]

R

refl [in Cat.Theory.Isomorphism]

S

Setoids.Hom [in Cat.Category.Setoids]
Setoid.eq_setoid [in Cat.Theory.SetoidType]
StreamInstance.bisim [in Cat.Category.Stream.Model]
StreamInstance.corec [in Cat.Category.Stream.Model]
StreamInstance.head [in Cat.Category.Stream.Model]
StreamInstance.Stream [in Cat.Category.Stream.Model]
StreamInstance.tail [in Cat.Category.Stream.Model]
StreamTerminal.cosubst [in Cat.Category.Stream.Terminality]
StreamTerminal.STREAM [in Cat.Category.Stream.Terminality]
StreamTerminal.Tau [in Cat.Category.Stream.Terminality]
StreamTerminal.tau [in Cat.Category.Stream.Terminality]
StreamTerminal.Terminality [in Cat.Category.Stream.Terminality]
StreamTerminal.τ [in Cat.Category.Stream.Terminality]
StreamTerminal.𝑺𝑻𝑹 [in Cat.Category.Stream.Terminality]
StreamTerminal.𝑺𝒕𝒓 [in Cat.Category.Stream.Terminality]
StreamTerminal.𝑻𝒂𝒊𝒍 [in Cat.Category.Stream.Terminality]
StreamTerminal.𝒉𝒆𝒂𝒅 [in Cat.Category.Stream.Terminality]
StreamTerminal.𝒕𝒂𝒊𝒍 [in Cat.Category.Stream.Terminality]
Stream.Hom [in Cat.Category.Stream.Category]
sym [in Cat.Theory.Isomorphism]

T

tcomod [in Cat.Theory.PushforwardComodule]
trans [in Cat.Theory.Isomorphism]
TriInstance.bisim [in Cat.Category.TriMat.Model]
TriInstance.corec [in Cat.Category.TriMat.Model]
TriInstance.rest [in Cat.Category.TriMat.Model]
TriInstance.top [in Cat.Category.TriMat.Model]
TriInstance.Tri [in Cat.Category.TriMat.Model]
TriMatTerminal.cut [in Cat.Category.TriMat.Terminality]
TriMatTerminal.lift [in Cat.Category.TriMat.Terminality]
TriMatTerminal.redec [in Cat.Category.TriMat.Terminality]
TriMatTerminal.Tau [in Cat.Category.TriMat.Terminality]
TriMatTerminal.tau [in Cat.Category.TriMat.Terminality]
TriMatTerminal.Terminality [in Cat.Category.TriMat.Terminality]
TriMatTerminal.TRI [in Cat.Category.TriMat.Terminality]
TriMatTerminal.τ [in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝑪𝒖𝒕 [in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝑹𝒆𝒔𝒕 [in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝑻𝑹𝑰 [in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝑻𝒓𝒊 [in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝒓𝒆𝒔𝒕 [in Cat.Category.TriMat.Terminality]
TriMatTerminal.𝒕𝒐𝒑 [in Cat.Category.TriMat.Terminality]
TriMat.Hom [in Cat.Category.TriMat.Category]

other

Π.compose [in Cat.Theory.SetoidType]
Π.id [in Cat.Theory.SetoidType]
Π.setoid [in Cat.Theory.SetoidType]
Φ [in Cat.Theory.PushforwardComodule]
φ [in Cat.Theory.CartesianStrongMonoidal]
𝑪𝒖𝒕 [in Cat.Category.RComonad_RComonadWithCut]
𝑬𝑸 [in Cat.Category.Types_Setoids]
𝑬𝑸_prod [in Cat.Category.Types_Setoids]
𝑹𝑪𝒐𝒎𝒐𝒅 [in Cat.Category.RComod]
𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅 [in Cat.Category.RComonad]
𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅𝑾𝒊𝒕𝒉𝑪𝒖𝒕 [in Cat.Category.RComonadWithCut]
𝑺𝒆𝒕𝒐𝒊𝒅 [in Cat.Category.Setoids]
𝑺𝒕𝒓𝒆𝒂𝒎 [in Cat.Category.Stream.Category]
𝑻𝒓𝒊𝑴𝒂𝒕 [in Cat.Category.TriMat.Category]
𝑻𝒚𝒑𝒆 [in Cat.Category.Types]
𝑼 [in Cat.Category.RComonad_RComonadWithCut]

Record Index

B

BinaryProduct [in Cat.Theory.Product]

C

CartesianStrongMonoidal [in Cat.Theory.CartesianStrongMonoidal]
Category [in Cat.Theory.Category]
Comodule [in Cat.Theory.Comodule]

F

Functor [in Cat.Theory.Functor]

I

Initial [in Cat.Theory.InitialTerminal]
IsInverse [in Cat.Theory.Isomorphism]
Iso [in Cat.Theory.Isomorphism]

M

Morphism [in Cat.Theory.Comodule]
Morphism [in Cat.Theory.RelativeComonad]
Morphism [in Cat.Theory.RelativeComonadWithCut]

N

NaturalTransformation [in Cat.Theory.NaturalTransformation]

P

Product [in Cat.Theory.Product]

R

RelativeComonad [in Cat.Theory.RelativeComonad]
RelativeComonadWithCut [in Cat.Theory.RelativeComonadWithCut]

S

Setoids.Morphism [in Cat.Category.Setoids]
Setoids.Obj [in Cat.Category.Setoids]
Setoid.Setoid [in Cat.Theory.SetoidType]
Stream.Morphism [in Cat.Category.Stream.Category]
Stream.Obj [in Cat.Category.Stream.Category]

T

Terminal [in Cat.Theory.InitialTerminal]
TriMat.Morphism [in Cat.Category.TriMat.Category]
TriMat.Obj [in Cat.Category.TriMat.Category]

other

Π.Π [in Cat.Theory.SetoidType]
Π₂.Π₂ [in Cat.Theory.SetoidType]

Global Index

G

J

K

Q

V

W

X

Y

Z

_

(574 entries)

Notation Index

A

B

C

E

G

H

I

J

K

L

N

O

Q

R

U

V

W

X

Y

Z

_

(139 entries)

Module Index

A

B

C

E

F

G

H

I

J

K

L

N

O

P

Q

R

U

V

W

X

Y

Z

_

(21 entries)

Variable Index

A

B

C

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(3 entries)

Library Index

B

E

G

H

J

K

L

O

Q

V

W

X

Y

Z

_

other

(32 entries)

Lemma Index

A

B

D

E

G

H

J

K

N

O

Q

U

V

W

X

Y

Z

_

(77 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

Q

R

U

V

W

X

Y

Z

_

(29 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(20 entries)

Projection Index

D

G

J

K

N

Q

U

V

W

X

Y

Z

_

(76 entries)

Inductive Index

A

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

other

(5 entries)

Section Index

A

B

G

H

J

K

L

N

O

Q

R

U

V

W

X

Y

Z

_

other

(28 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

(6 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

U

V

W

X

Y

Z

_

(13 entries)

Definition Index

A

B

G

J

K

N

O

Q

U

V

W

X

Y

Z

_

(100 entries)

Record Index

A

D

E

G

H

J

K

L

O

Q

U

V

W

X

Y

Z

_

(25 entries)

Benedikt Ahrens and Régis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory

Table of contents

Index