Benedikt Ahrens and Régis Spadotti—
Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index
Notation
"
∀
x .. y , P" ≔ (
∀
x
, .. (
∀
y
,
P
) ..)
(
at
level
200,
x
binder
,
y
binder
,
right
associativity
) :
type_scope
.
Notation
"
∃
x .. y , P" ≔ (
∃
x
,
.. (
∃
y
,
P
) ..)
(
at
level
200,
x
binder
,
y
binder
,
right
associativity
) :
type_scope
.
Notation
"
x ∨ y" ≔ (
x
∨
y
) (
at
level
85,
right
associativity
) :
type_scope
.
Notation
"
x ∧ y" ≔ (
x
∧
y
) (
at
level
80,
right
associativity
) :
type_scope
.
Notation
"
x → y" ≔ (
x
→
y
)
(
at
level
90,
y
at
level
200,
right
associativity
):
type_scope
.
Notation
"
x ↔ y" ≔ (
x
↔
y
) (
at
level
95,
no
associativity
):
type_scope
.
Notation
"
¬ x" ≔ (
¬
x
) (
at
level
75,
right
associativity
) :
type_scope
.
Notation
"
x ≠ y" ≔ (
x
≠
y
) (
at
level
70) :
type_scope
.
Notation
"
'λ'
x .. y ∙ t" ≔ (
fun
x
⇒ .. (
fun
y
⇒
t
) ..)
(
at
level
200,
x
binder
,
y
binder
,
right
associativity
).
Benedikt Ahrens and Régis Spadotti—
Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index