Benedikt Ahrens and Régis Spadotti—
Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index
Notation
"
⊤" ≔
True
.
Notation
"
⊥" ≔
False
.
Notation
"
_⟨⊎⟩_" ≔
sum
(
only
parsing
).
Infix
"
⟨⊎⟩" ≔
sum
(
at
level
25,
left
associativity
).
Infix
"
⟨×⟩" ≔
prod
(
at
level
20,
left
associativity
).
Notation
"
_⟨×⟩_" ≔
prod
(
only
parsing
).
Force coercion to Type (used with program)
Notation
"
‵ T ′" ≔ (
T
:
Type
) (
only
parsing
).
Reserved Notation
"A ⇒ B" (
at
level
30,
right
associativity
).
Reserved Notation
"f ∘ g" (
at
level
40,
left
associativity
).
Reserved Notation
"⟨ f , g ⟩" (
at
level
0,
no
associativity
).
Benedikt Ahrens and Régis Spadotti—
Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index