slides - Dan Licata - Wesleyan University

Programming and Proving with
Higher Inductive Types
Dan Licata
Wesleyan University
Department of Mathematics and Computer Science
Constructive Type Theory
[Martin-Löf]
Three senses of constructivity:
2
Constructive Type Theory
[Martin-Löf]
Three senses of constructivity:
Non-aﬃrmation of certain classical principles
provides axiomatic freedom
2
Synthetic geometry
Euclid’s postulates
1. To draw a straight line from any point
to any point.
2. To produce a finite straight line continuously
in a straight line.
3. To describe a circle with any center and distance.
4. That all right angles are equal to one another.
5. Given a line and a point not on it, there is exactly
one line through the point that does not intersect
the line
3
Synthetic geometry
Cartesian
Euclid’s postulates
1. To draw a straight line from any point
to any point.
2. To produce a finite straight line continuously
in a straight line.
3. To describe a circle with any center and distance.
4. That all right angles are equal to one another.
5. Given a line and a point not on it, there is exactly
one line through the point that does not intersect
the line
3
Synthetic geometry
Cartesian
Euclid’s postulates
models
1. To draw a straight line from any point
to any point.
2. To produce a finite straight line continuously
in a straight line.
3. To describe a circle with any center and distance.
4. That all right angles are equal to one another.
5. Given a line and a point not on it, there is exactly
one line through the point that does not intersect
the line
3
Synthetic geometry
Cartesian
Euclid’s postulates
models
1. To draw a straight line from any point
to any point.
2. To produce a finite straight line continuously
in a straight line.
3. To describe a circle with any center and distance.
4. That all right angles are equal to one another.
3
Synthetic geometry
Cartesian
Euclid’s postulates
models
1. To draw a straight line from any point
to any point.
2. To produce a finite straight line continuously
in a straight line.
3. To describe a circle with any center and distance.
4. That all right angles are equal to one another.
Spherical
3
Synthetic geometry
Cartesian
Euclid’s postulates
models
1. To draw a straight line from any point
to any point.
2. To produce a finite straight line continuously
in a straight line.
3. To describe a circle with any center and distance.
4. That all right angles are equal to one another.
5. Two distinct lines meet at two antipodal points.
Spherical
3
Synthetic mathematics
Type theory
1.τ ::= b | τ1 → τ2
2.e ::= x | e1 e2 | λx.e
3.(λx.e)e2 = e[e2/x]
4
Synthetic mathematics
Set-theoretic
functions
Type theory
1.τ ::= b | τ1 → τ2
2.e ::= x | e1 e2 | λx.e
3.(λx.e)e2 = e[e2/x]
4
Synthetic mathematics
Set-theoretic
functions
Type theory
1.τ ::= b | τ1 → τ2
2.e ::= x | e1 e2 | λx.e
3.(λx.e)e2 = e[e2/x]
Domain-theoretic
functions
4
Synthetic mathematics
Set-theoretic
functions
Type theory
1.τ ::= b | τ1 → τ2
2.e ::= x | e1 e2 | λx.e
3.(λx.e)e2 = e[e2/x]
4.Y(f) = f(Y(f))
Domain-theoretic
functions
4
Constructive Type Theory
Three senses of constructivity:
5
Constructive Type Theory
Three senses of constructivity:
Non-aﬃrmation of certain classical principles
provides axiomatic freedom
5
Constructive Type Theory
Three senses of constructivity:
Non-aﬃrmation of certain classical principles
provides axiomatic freedom
Computational interpretation supports software
verification and proof automation
5
Computational Interpretation
There is an algorithm that,
given a closed term e : bool,
computes either
an equality e = true, or
an equality e = false.
6
Computational Interpretation
There is an algorithm that,
given a closed term e : bool,
computes either
an equality e = true, or
an equality e = false.
Requires functions with arbitrary domain/
range to be computable, but stating
theorem for bool oﬀers some flexibility
6
Computational Interpretation
There is an algorithm that,
given a closed term e : bool,
computes either
an equality e = true, or
an equality e = false.
Requires functions with arbitrary domain/
range to be computable, but stating
theorem for bool oﬀers some flexibility
Basis for software verification and
proof automation
6
Constructive Type Theory
Three senses of constructivity:
Non-aﬃrmation of certain classical principles
provides axiomatic freedom
Computational interpretation supports software
verification and proof automation
7
Constructive Type Theory
Three senses of constructivity:
Non-aﬃrmation of certain classical principles
provides axiomatic freedom
Computational interpretation supports software
verification and proof automation
Props-as-types allows proof-relevant mathematics
7
Proof relevance
x : A
8
Proof relevance
x : A
x =A y
8
equality type
Proof relevance
x : A
p : x =A y
8
equality type
Proof relevance
x : A
p : x =A y
Any structure or property C can be
transported along an equality
8
equality type
Proof relevance
x : A
p : x =A y
Any structure or property C can be
transported along an equality
transportC(p) : C(x) ! C(y)
8
equality type
Proof relevance
x : A
p : x =A y
Any structure or property C can be
transported along an equality
transportC(p) : C(x) ! C(y)
8
equality type
Leibniz’s
indiscernability
of identicals
Proof relevance
x : A
p : x =A y
Any structure or property C can be
transported along an equality
transportC(p) : C(x) ! C(y)
by a function: can it do real work?
8
equality type
Leibniz’s
indiscernability
of identicals
Proof relevance
x : A
p : x =A y
9
equality type
Proof relevance
x : A
p : x =A y
p1 =x=y p2
9
equality type
Proof relevance
x : A
p : x =A y
q : p1 =x=y p2
9
equality type
Proof relevance
x : A
p : x =A y
q : p1 =x=y p2
q1 =p1=p2 q2
9
equality type
Proof relevance
x : A
p : x =A y
q : p1 =x=y p2
r : q1 =p1=p2 q2
9
equality type
Proof relevance
x : A
p : x =A y
equality type
q : p1 =x=y p2
r : q1 =p1=p2 q2
...
higher equalities radically expand the kind of
math that can be done synthetically…
9
Homotopy Type Theory
type theory
category theory
homotopy theory
[Hofmann,Streicher,Awodey,Warren,Voevodsky
Lumsdaine,Gambino,Garner,van den Berg]
10
Types as spaces
α
M
N
11
Types as spaces
type A is a space
α
M
N
11
Types as spaces
type A is a space
α
M
N
programs
M:A
are points
11
Types as spaces
type A is a space
α
M
programs
M:A
are points
N
proofs of equality
α : M =A N
are paths
11
Types as spaces
type A is a space
path operations
α
M
programs
M:A
are points
N
proofs of equality
α : M =A N
are paths
11
Types as spaces
type A is a space
id
M
programs
M:A
are points
path operations
id
α
N
proofs of equality
α : M =A N
are paths
11
: M = M (refl)
Types as spaces
type A is a space
id
M
programs
M:A
are points
α
α -1
path operations
id
α-1
N
proofs of equality
α : M =A N
are paths
11
: M = M (refl)
: N = M (sym)
Types as spaces
type A is a space
id
M
α
α -1
path operations
id
: M = M (refl)
α-1
: N = M (sym)
β o α : M = P (trans)
N
β
P
programs
M:A
are points
proofs of equality
α : M =A N
are paths
11
Homotopy
Deformation of one path into another
α
β
12
Homotopy
Deformation of one path into another
α
β
12
Homotopy
Deformation of one path into another
α
β
= 2-dimensional path between paths
12
Homotopy
Deformation of one path into another
α
δ : α =x=y β
β
= 2-dimensional path between paths
12
Homotopy
Deformation of one path into another
α
δ : α =x=y β
β
= 2-dimensional path between paths
Then homotopies between homotopies ….
12
Types as spaces
type A is a space
id
M
α
α -1
path operations
id
: M = M (refl)
α-1
: N = M (sym)
β o α : M = P (trans)
N
β
P
homotopies
programs
M:A
are points
ul : id o α =M=N α
il : α-1 o α =M=M id
proofs of equality
α : M =A N
are paths
asc : γ o (β o α)
=M=P (γ o β) o α
13
Homotopy Type Theory
type theory
category theory
homotopy theory
[Hofmann,Streicher,Awodey,Warren,Voevodsky
Lumsdaine,Gambino,Garner,van den Berg]
14
Types as ∞-groupoids
type A is an ∞-groupoid
morphisms
id
: M = M (refl)
α-1
: N = M (sym)
β o α : M = P (trans)
infinite-dimensional
algebraic structure,
with morphisms,
morphisms between
morphisms, ...
morphisms between morphisms
ul : id o α
each level has a
groupoid structure,
and they interact
=M=N α
il : α-1 o α =M=M id
asc : γ o (β o α)
=M=P (γ o β) o α
15
Path induction
Type of paths
from a to somewhere
is inductively
generated by
y2
p2
y1
p1
a
p3
id
y3
a
16
Path induction
Type of paths
from a to somewhere
is inductively
generated by
y2
p2
y1
p1
a
p3
id
y3
a
Fix a type A with element a:A.
For a family of types C(y:A, p:a=y),
to give an element of
C(y,p) for all y and p:a=y,
suﬃces to give an element of
C(a,id)
16
Type theory is a
synthetic theory of
spaces/∞-groupoids
17
Homotopy Type Theory
type theory
new programs
and types
category theory
homotopy theory
18
Univalence [Voevodsky]
19
Univalence [Voevodsky]
Equivalence of types is a generalization to
spaces of bijection of sets
19
Univalence [Voevodsky]
Equivalence of types is a generalization to
spaces of bijection of sets
Univalence axiom:
equality of types (A =Type B) is (equivalent to)
equivalence of types (Equiv A B)
19
Univalence [Voevodsky]
Equivalence of types is a generalization to
spaces of bijection of sets
Univalence axiom:
equality of types (A =Type B) is (equivalent to)
equivalence of types (Equiv A B)
∴ all structures/properties respect equivalence
19
Univalence [Voevodsky]
Equivalence of types is a generalization to
spaces of bijection of sets
Univalence axiom:
equality of types (A =Type B) is (equivalent to)
equivalence of types (Equiv A B)
∴ all structures/properties respect equivalence
Not by collapsing equivalence,
but by exploiting proof-relevant equality:
transport does real work
19
Higher inductive types
[Bauer,Lumsdaine,Shulman,Warren]
New way of forming types:
Inductive type specified by generators
not only for points (elements), but also for paths
20
Constructivity
Non-aﬃrmation of classical principles
✓
Computational interpretation
?
Proof-relevant mathematics
✓
21
Homotopy Type Theory
type theory
new possibilities
for computerchecked proofs
new programs
and types
category theory
homotopy theory
22
Outline
1.Certified homotopy theory
2.Certified software
23
Outline
1.Certified homotopy theory
2.Certified software
24
Homotopy Theory
A branch of topology,
the study of spaces and continuous deformations
[image from wikipedia]
25
Homotopy in HoTT
π1(S1) = ℤ
Freudenthal
Van Kampen
πk<n(Sn) = 0
πn(Sn) = ℤ
Covering spaces
Hopf fibration
K(G,n)
π2(S2) = ℤ
Cohomology
axioms
π3(S2) = ℤ
James
Construction
π4(S3) = ℤ?
Whitehead
for n-types
Blakers-Massey
[Brunerie, Finster, Hou,
Licata, Lumsdaine, Shulman]
26
Homotopy in HoTT
π1(S1) = ℤ
Freudenthal
Van Kampen
πk<n(Sn) = 0
πn(Sn) = ℤ
Covering spaces
Hopf fibration
K(G,n)
π2(S2) = ℤ
Cohomology
axioms
π3(S2) = ℤ
James
Construction
π4(S3) = ℤ?
Whitehead
for n-types
Blakers-Massey
[Brunerie, Finster, Hou,
Licata, Lumsdaine, Shulman]
26
Homotopy Groups
Homotopy groups of a space X:
π1(X) is fundamental group (group of loops)
π2(X) is group of homotopies (2-dimensional loops)
π3(X) is group of 3-dimensional loops
…
27
Telling spaces apart
=|
28
Telling spaces apart
=|
fundamental group
is non-trivial (ℤ × ℤ)
fundamental group
is trivial
28
The Circle
Circle S1 is a higher inductive type
generated by
loop
base
29
The Circle
Circle S1 is a higher inductive type
generated by
base : S1
loop : base = base
29
loop
base
The Circle
Circle S1 is a higher inductive type
generated by
point
base : S1
loop : base = base
29
loop
base
The Circle
Circle S1 is a higher inductive type
generated by
point
path
base : S1
loop : base = base
29
loop
base
The Circle
Circle S1 is a higher inductive type
generated by
point
path
base : S1
loop : base = base
loop
-1
id
loop
base
Free type: equipped with structure
id
inv : loop o loop-1 = id
loop-1
...
loop o loop
29
The Circle
Circle recursion:
function S1 ! X determined by
base’ : X
loop’ : base’ = base’
30
loop
base
base’
loop’
The Circle
Circle recursion:
function S1 ! X determined by
base’ : X
loop’ : base’ = base’
loop
base
base’
loop’
Circle induction: To prove a predicate P for all points
on the circle, suﬃces to prove P(base),
continuously in the loop
30
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
loop
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
loop
loop-1
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
loop
loop-1
loop o loop
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
loop
loop-1
loop o loop
loop-1 o loop-1
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
loop
loop-1
loop o loop
loop-1 o loop-1
loop o loop-1
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
loop
loop-1
loop o loop
loop-1 o loop-1
loop o loop-1
= id
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
0
id
loop
loop-1
loop o loop
loop-1 o loop-1
loop o loop-1
= id
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
0
loop
1
loop-1
loop o loop
loop-1 o loop-1
loop o loop-1
= id
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
0
loop
1
loop-1
-1
loop o loop
loop-1 o loop-1
loop o loop-1
= id
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
0
loop
1
loop-1
-1
loop o loop
2
loop-1 o loop-1
loop o loop-1
= id
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
0
loop
1
loop-1
-1
loop o loop
2
loop-1 o loop-1
-2
loop o loop-1
= id
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
0
loop
1
loop-1
-1
loop o loop
2
loop-1 o loop-1
-2
loop o loop-1
0
= id
31
loop
base
Fundamental group of circle
How many diﬀerent loops are there on
the circle, up to homotopy?
id
0
loop
1
loop-1
-1
loop o loop
2
loop-1 o loop-1
-2
loop o loop-1
0
= id
31
loop
base
integers are “codes”
for paths on the
circle
Fundamental group of circle
Definition. Ω(S1) is the type of loops at base
i.e. the type (base =S1 base)
32
Fundamental group of circle
Definition. Ω(S1) is the type of loops at base
i.e. the type (base =S1 base)
Theorem. Ω(S1) is equivalent to ℤ,
by a map that sends o to +
32
Fundamental group of circle
Definition. Ω(S1) is the type of loops at base
i.e. the type (base =S1 base)
Theorem. Ω(S1) is equivalent to ℤ,
by a map that sends o to +
Corollary: Fundamental group
of the circle is isomorphic to ℤ
32
Fundamental group of circle
Definition. Ω(S1) is the type of loops at base
i.e. the type (base =S1 base)
Theorem. Ω(S1) is equivalent to ℤ,
by a map that sends o to +
Corollary: Fundamental group
of the circle is isomorphic to ℤ
0-truncation (set of connected components)
of Ω(S1)
32
Fundamental group of circle
Theorem. Ω(S1) is equivalent to ℤ
Proof (Shulman, L.): two mutually inverse functions
wind
: Ω(S1) ! ℤ
loop- : ℤ ! Ω(S1)
33
Fundamental group of circle
Theorem. Ω(S1) is equivalent to ℤ
Proof (Shulman, L.): two mutually inverse functions
wind
: Ω(S1) ! ℤ
loop- : ℤ ! Ω(S1)
loop0 = id
loop+n = loop o loop o … loop
(n times)
loop-n = loop-1 o loop-1 o … loop-1 (n times)
33
Universal Cover
wind : Ω(S1) ! ℤ
defined by lifting a loop
to the cover, and giving
the other endpoint of 0
34
Universal Cover
wind : Ω(S1) ! ℤ
defined by lifting a loop
to the cover, and giving
the other endpoint of 0
lifting is functorial
34
Universal Cover
wind : Ω(S1) ! ℤ
defined by lifting a loop
to the cover, and giving
the other endpoint of 0
lifting is functorial
lifting loop adds 1
34
Universal Cover
wind : Ω(S1) ! ℤ
defined by lifting a loop
to the cover, and giving
the other endpoint of 0
lifting is functorial
lifting loop adds 1
lifting loop-1 subtracts 1
34
Universal Cover
wind : Ω(S1) ! ℤ
defined by lifting a loop
to the cover, and giving
the other endpoint of 0
Example:
wind(loop o loop-1)
= 0 + 1 - 1
= 0
lifting is functorial
lifting loop adds 1
lifting loop-1 subtracts 1
34
Universal Cover
35
Universal Cover
Cover : S1 ! Type
Cover(base) := ℤ
Cover1(loop) :=
ua(successor) : ℤ = ℤ
35
Universal Cover
defined by circle
recursion
Cover : S1 ! Type
Cover(base) := ℤ
Cover1(loop) :=
ua(successor) : ℤ = ℤ
35
Universal Cover
defined by circle
recursion
Cover : S1 ! Type
Cover(base) := ℤ
Cover1(loop) :=
ua(successor) : ℤ = ℤ
interpret loop as
“add 1” bijection
35
Universal Cover
defined by circle
recursion
Cover : S1 ! Type
Cover(base) := ℤ
Cover1(loop) :=
ua(successor) : ℤ = ℤ
univalence
35
interpret loop as
“add 1” bijection
Winding number
wind : Ω(S1) ! ℤ
wind(p) = transportCover(p,0)
36
lift p to cover,
starting at 0
Winding number
wind : Ω(S1) ! ℤ
wind(p) = transportCover(p,0)
wind(loop-1 o loop)
36
lift p to cover,
starting at 0
Winding number
wind : Ω(S1) ! ℤ
wind(p) = transportCover(p,0)
wind(loop-1 o loop)
= transportCover(loop-1 o loop, 0)
36
lift p to cover,
starting at 0
Winding number
wind : Ω(S1) ! ℤ
wind(p) = transportCover(p,0)
lift p to cover,
starting at 0
wind(loop-1 o loop)
= transportCover(loop-1 o loop, 0)
= transportCover(loop-1, transportCover(loop,0))
36
Winding number
wind : Ω(S1) ! ℤ
wind(p) = transportCover(p,0)
lift p to cover,
starting at 0
wind(loop-1 o loop)
= transportCover(loop-1 o loop, 0)
= transportCover(loop-1, transportCover(loop,0))
= transportCover(loop-1, 1)
36
Winding number
wind : Ω(S1) ! ℤ
wind(p) = transportCover(p,0)
=
=
=
=
lift p to cover,
starting at 0
wind(loop-1 o loop)
transportCover(loop-1 o loop, 0)
transportCover(loop-1, transportCover(loop,0))
transportCover(loop-1, 1)
0
36
Fundamental group of the circle
The HoTT book
Agda
37
n
πn(S )
in HoTT
n-dimensional sphere
kth homotopy group
[image from wikipedia]
38
n
πn(S )
in HoTT
n-dimensional sphere
kth homotopy group
[image from wikipedia]
38
n
πn(S )
= ℤ for n≥1
Proof: Induction on n
Base case: π1(S1) = ℤ
Inductive step: πn+1(Sn+1) = πn(Sn)
39
n
πn(S )
= ℤ for n≥1
Proof: Induction on n
Base case: π1(S1) = ℤ
Inductive step: πn+1(Sn+1) = πn(Sn)
Key lemma: |Sn|n = |Ω(Sn+1)|n
39
n
πn(S )
= ℤ for n≥1
Proof: Induction on n
Base case: π1(S1) = ℤ
Inductive step: πn+1(Sn+1) = πn(Sn)
Key lemma: |Sn|n = |Ω(Sn+1)|n
n-truncation:
best approximation of a type such
that all (n+1)-paths are equal
39
n
πn(S )
= ℤ for n≥1
Proof: Induction on n
Base case: π1(S1) = ℤ
Inductive step: πn+1(Sn+1) = πn(Sn)
Key lemma: |Sn|n = |Ω(Sn+1)|n
n-truncation:
best approximation of a type such
that all (n+1)-paths are equal
39
higher inductive type
generated by
basen : Sn
loopn : Ωn(Sn)
n
|S |n
=
n+1
|Ω(S )|
n
n-truncation of Sn is the type of “codes” for loops on Sn+1
40
n
|S |n
=
n+1
|Ω(S )|
n
n-truncation of Sn is the type of “codes” for loops on Sn+1
Decode: promote n-dimensional loop on Sn
to n+1-dimensional loop on Sn+1
40
n
|S |n
=
n+1
|Ω(S )|
n
n-truncation of Sn is the type of “codes” for loops on Sn+1
Decode: promote n-dimensional loop on Sn
to n+1-dimensional loop on Sn+1
Encode: define fibration Code(x:Sn+1) with
Code(basen+1) := |Sn|n
∼ |Sn|n
Code(loopn+1) := equivalence |Sn|n →
“rotating by loopn”
40
2
π2(S ):
Hopf fibration
41
Synthetic homotopy theory
Gap between informal and formal proofs is small
Proofs are constructive*: can run them
Results apply in a variety of settings,
from simplicial sets (hence topological spaces)
to Quillen model categories and ∞-topoi*
New type-theoretic proofs/methods
*work in progress
42
43
Outline
1.Certified homotopy theory
2.Certified software
44
Patches
Patch
diff
a
b
c
a
d
c
=
Version control
Collaborative editing
45
2c2
<b
-->d
a
b
c
id
a
b
c
id
a
b
c
a
b
c
a
b
c
p
a
d
c
q
a
d
e
id
a
b
c
a
b
c
qop
a
b
c
p
a
d
c
q
a
d
e
id
a
b
c
a
b
c
p
a
b
c
a
d
c
qop
a
b
c
p
a
d
c
q
a
d
e
id
a
b
c
a
b
c
p
a
b
c
a
d
c
!p
qop
a
b
c
p
a
d
c
q
a
d
e
id
a
b
c
a
b
c
p
a
b
c
!p
undo/rollback
qop
a
b
c
p
a
d
c
a
d
c
q
a
d
e
Patches are paths
id
a
b
c
a
b
c
p
a
b
c
!p
undo/rollback
qop
a
b
c
p
a
d
c
a
d
c
q
a
d
e
Merging
p
a
b
c
q
a
b
e
a
d
c
47
Merging
p
a
b
c
q
a
b
e
a
d
c
q’
a
d
e
47
p’
Merging
p=b d at 1
p
a
b
c
q
q=c e at 2
a
b
e
a
d
c
q’
a
d
e
47
p’
Merging
p=b d at 1
p
a
b
c
q
q=c e at 2
a
b
e
a
d
c
q’
a
d
e
47
p’
p’=p
q’=q
Merging
p=b d at 1
p
a
d
c
a
b
c
q
a
b
e
=
q’
a
d
e
47
q=c e at 2
p’
p’=p
q’=q
Merging
merge : (p q : Patch)
! Σq’,p’:Patch.
Maybe(q’ o p =
p’ o q)
48
Merging
merge : (p q : Patch)
! Σq’,p’:Patch.
Maybe(q’ o p =
p’ o q)
Equational theory of patches
= paths between paths
48
Basic Patches
f
i
b
r
a
f
i
a
t
i
o
b @ 2
b
f
a
n
b @ 2
49
i
a
Basic Patches
“Repository” is a char vector of length n
f
i
b
r
Basic patch is a
i
t
i
o
n
b @ i where i<n
a
f
a
b @ 2
b
f
a
b @ 2
49
i
a
Patches as a HIT
Repos:Type
50
Patches as a HIT
Repos:Type
doc[n]
points describe
repository contents
50
Patches as a HIT
Repos:Type
a b@i
doc[n]
points describe
repository contents
paths are patches
50
Patches as a HIT
Repos:Type
compressed
a b@i
doc[n]
points describe
repository contents
paths are patches
50
Patches as a HIT
Repos:Type
compressed
gzip
points describe
repository contents
paths are patches
50
a b@i
doc[n]
Patches as a HIT
Repos:Type
compressed
gzip
points describe
repository contents
paths are patches
50
a b@i
doc[n]
Patches as a HIT
Repos:Type
compressed
gzip
a b@i
doc[n]
points describe
repository contents
doc[n]
doc[n]
doc[n]
paths are patches
doc[n]
50
Patches as a HIT
Repos:Type
compressed
gzip
points describe
repository contents
a b@i
doc[n]
a b@i
doc[n]
c d@j
doc[n]
doc[n]
paths are patches
c d@j
a b@i
doc[n]
50
Patches as a HIT
Repos:Type
compressed
gzip
points describe
repository contents
a b@i
doc[n]
a b@i
doc[n]
c d@j
doc[n]
doc[n]
paths are patches
c d@j
paths between paths are
equations between patches
a b@i
doc[n]
50
Patches as a HIT
Repos:Type
compressed
gzip
points describe
repository contents
a b@i
doc[n]
a b@i
doc[n]
c d@j
doc[n]
doc[n]
paths are patches
c d@j
paths between paths are
equations between patches
a b@i
doc[n]
i≠j
50
Generators for HIT
51
Generators for HIT
Repos : Type
51
Generators for HIT
Repos : Type
doc[n]
: Repos
compressed : Repos
51
Generators for HIT
Repos : Type
doc[n]
: Repos
compressed : Repos
(a b@i) : doc[n] = doc[n] if a,b:Char, i<n
gzip : doc[n] = compressed
51
Generators for HIT
Repos : Type
doc[n]
: Repos
compressed : Repos
(a b@i) : doc[n] = doc[n] if a,b:Char, i<n
gzip : doc[n] = compressed
commute:
(a b at i)o(c d at j)
=(c d at j)o(a b at i)
51
if i ≠ j
Type: Patch
Type: Repos
Elements:
Points:
Paths:
doc[n]
a b@i
Equality:
Paths between paths:
(a b at i)o(c d at j)=
commute :
(a b at i)o(c d at j)=
(c d at j)o(a b at i)
...
id o p = p = p o id
(c d at j)o(a b at i)
po(qor) = (poq)or
!p o p = id = p o !p
p=p
p=q if q=p
p=r if p=q and q=r
!p = !p’ if p = p’
p o q = p’ o q’ if p = p’ and q = q’
52
Repos recursion
To define a function Repos ! A
it suﬃces to
53
Repos recursion
To define a function Repos ! A
it suﬃces to
map the element generators of Repos
to elements of A
53
Repos recursion
To define a function Repos ! A
it suﬃces to
map the element generators of Repos
to elements of A
map the equality generators of Repos
to equalities between the corresponding elements of A
53
Repos recursion
To define a function Repos ! A
it suﬃces to
map the element generators of Repos
to elements of A
map the equality generators of Repos
to equalities between the corresponding elements of A
map the equality-between-equality generators to
equalities between the corresponding equalities in A
53
Repos recursion
To define a function Repos ! A
it suﬃces to
map the element generators of Repos
to elements of A
map the equality generators of Repos
to equalities between the corresponding elements of A
map the equality-between-equality generators to
equalities between the corresponding equalities in A
All functions on Repos respect patches
All functions on patches respect patch equality
53
Interpreter
Goal is to define:
interp : doc[n] = doc[n]
! Bijection (Vec Char n) (Vec Char n)
54
Interpreter
Goal is to define:
interp : doc[n] = doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(id) = (λx.x, …)
interp(q o p) = (interp q) ob (interp p)
interp(!p) = !b (interp p)
interp(a b@i) = swapat a b i
54
Interpreter
Goal is to define:
interp : doc[n] = doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(id) = (λx.x, …)
interp(q o p) = (interp q) ob (interp p)
interp(!p) = !b (interp p)
interp(a b@i) = swapat a b i
But only tool available is RepoDesc recursion:
no direct recursion over paths
54
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(a b at i) = swapat a b i
Need to pick A and define
I(doc[n]) := … : A
I1(a b@i) := … : I(doc[n]) = I(doc[n])
I2(compose) := …
55
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(a b at i) = swapat a b i
Key idea: pick A = Type and define
I(doc[n]) := … : Type
I1(a b@i) := … : I(doc[n]) = I(doc[n])
I2(compose) := …
56
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(a b at i) = swapat a b i
Key idea: pick A = Type and define
I(doc[n]) := Vec Char n : Type
I1(a b@i) := … : I(doc[n]) = I(doc[n])
I2(compose) := …
57
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(a b at i) = swapat a b i
Key idea: pick A = Type and define
I(doc[n]) := Vec Char n : Type
I1(a b@i) := … : Vec Char n = Vec Char n
I2(compose) := …
58
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(a b at i) = swapat a b i
Key idea: pick A = Type and define
I(doc[n]) := Vec Char n : Type
I1(a b@i) := ua(swapat a b i)
: Vec Char n = Vec Char n
I2(compose) := …
59
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(a b at i) = swapat a b i
Key idea: pick A = Type and define
I(doc[n]) := Vec Char n : Type
I1(a b@i) := ua(swapat a b i)
: Vec Char n = Vec Char n
I2(compose) := …
univalence
59
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(a b at i) = swapat a b i
Key idea: pick A = Type and define
I(doc[n]) := Vec Char n : Type
I1(a b@i) := ua(swapat a b i)
: Vec Char n = Vec Char n
I2(compose) := <proof about swapat>
60
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(p) = ua-1(I1(p))
Key idea: pick A = Type and define
I(doc[n]) := Vec Char n : Type
I1(a b@i) := ua(swapat a b i)
: Vec Char n = Vec Char n
I2(compose) := <proof about swapat>
61
interp : doc[n]=doc[n]
! Bijection (Vec Char n) (Vec Char n)
interp(p) = ua-1(I1(p))
Satisfies the desired equations (as propositional equalities):
interp(id) = (λx.x, …)
interp(q o p) = (interp q) ob (interp p)
interp(!p) = !b (interp p)
interp(a b@i) = swapat a b i
62
Summary
I : Repos ! Type interprets Repos as Types,
patches as bijections, satisfying patch equalities
Higher inductive elim. defines functions that respect equality:
you specify what happens on the generators;
homomorphically extended to id,o,!,...
Univalence lets you give a computational model of equality
proofs (here, patches); guaranteed to satisfy laws
Shorter definition and code:
1 basic patch & 4 basic axioms of equality, instead of
4 patches & 14 equations
63
Operational semantics
Can’t quite run these programs yet
Some special cases known, some recent progress:
Licata&Harper, ’12
Coquand&Barras, ’13
Shulman, ’13
Bezem&Coquand&Huber, ’13
64
Homotopy Type Theory
type theory
new certified
programs and
proofs
new programs
and types
category theory
homotopy theory
65
Reading list
1.The HoTT Book
2.Homotopy theory in Agda:
Fundamental group of the circle [LICS’13]
πn(Sn) = ℤ [proceedings]
github.com/dlicata335/
3.Blog: homotopytypetheory.org
66

Download Report