Information Technology Reference
In-Depth Information
The Homotopy Interpretation (Awodey-Warren)
Suppose we have terms of ascending identity types:
a, b
:
A
p, q
:
Id
A
(
a, b
)
ʱ, ʲ
:
Id
Id
A
(
a,b
)
(
p, q
)
...
:
Id
Id
Id
...
(
...
)
Consider the following interpretation:
Types
Spaces
Terms
Maps
a
:
A
Points
a
:1
→ A
p
:
Id
A
(
a, b
)
Paths
p
:
a ⃒ b
ʱ
:
Id
Id
A
(
a,b
)
(
p, q
)
Homotopies
ʱ
:
p
q
.
This extends the familiar
topological interpretation
of the
simply-typed
ʻ
-calculus:
types
spaces
terms
continuous functions
to
dependently typed ʻ
-calculus with
Id
-types, via the
basic idea
:
p
:
Id
X
(
a, b
)
p
is a path from point
a
to point
b
in
X
This forces
dependent types to be fibrations
,
Id
-types to be path spaces
,and
homotopic maps to be identical
.
The Fundamental Groupoid of a Type (Hofmann-Streicher)
Like path spaces in topology, identity types endow each type in the system with
the structure of a (higher-) groupoid:
p
p
p
a
ˑ
a
a
a
b
b
b
•
•
•
•
ʱ
•
•
ʱ
ʲ
•
q
q
