Homotopies for Free!
Taichi Uemura


Computationally Efficient Market Simulation Tool for Future Grid Scenario Analysis
    Shariq Riaz, Graduate Student Member, IEEE,
        Gregor Verbič, Senior Member, IEEE,
        and Archie C. Chapman, Member, IEEE
Shariq Riaz, Gregor Verbič and Archie C. Chapman are with the School of Electrical and Information Engineering, The University of Sydney, Sydney, New South Wales, Australia. 	e-mails: (shariq.riaz, gregor.verbic, archie.chapman@sydney.edu.au).
Shariq Riaz is also with the Department of Electrical Engineering, University of Engineering and Technology Lahore, Lahore, Pakistan.

    December 30, 2023
==================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================


We show “free theorems” in the style of Wadler
for polymorphic functions in homotopy type theory
as consequences of the abstraction theorem.
As an application, it follows that
every space defined as a higher inductive type
has the same homotopy groups as some type of polymorphic functions
defined without univalence or higher inductive types.




§ INTRODUCTION


Given a closed term of type of polymorphic functions
defined in homotopy type theory <cit.>,
we can derive a theorem that it satisfies.
For example,
let t be a closed term of type

    t : ∏_X : ∏_x : Xx = x → x = x.

Then we have a theorem

    ∏_X, X' : ∏_f : X → X'∏_x : X∏_p : x = xt(fp) = f(tp)

in homotopy type theory, in the sense that
there is a closed term of this type.

Such theorems are “free theorems” in the style of Wadler <cit.>
for homotopy type theory.
Original free theorems for polymorphic type theory
are consequences of relational parametricity <cit.>
and have a lot of applications including
short cut fusion <cit.>,
non-definability of polymorphic equality <cit.>,
and encoding initial algebras and final coalgebras
in pure polymorphic lambda calculus <cit.>.
Recently relational parametricity and free theorems for dependent type theory
have been studied by several authors.
Atkey et al. <cit.>
constructed relationally parametric models of Martin-Löf type theory
and proved a simple free theorem
and the existence of initial algebras for indexed functors.
Takeuti <cit.> studied relational parametricity for the lambda cube
and proved adjoint functor theorem internally.
Bernardy et al. <cit.>
studied relational parametricity for pure type systems
and free theorems for dependently typed functions.

In this paper we show free theorems specific to homotopy type theory
such as the example given in the first paragraph
where the type ∏_X : ∏_x : Xx = x → x = x
seems to be trivial without homotopy-theoretic interpretation.
A difference between free theorems for homotopy type theory
and original free theorems for polymorphic type theory is that
in homotopy type theory they are represented by homotopies
instead of equalities.
This difference causes some problems
related to proof-relevance and higher dimensional homotopies.
One approach to these problems is higher dimensional parametricity
<cit.>
and to state free theorems as coherent homotopies.
Both in <cit.> and <cit.>,
the target languages are polymorphic lambda calculus
which does not have higher dimensional structures.
On the other hand, our target language, homotopy type theory,
has already higher dimensional structures,
and thus ordinary free theorems for higher dimensional types work well.

To explain this, let us see an example.
Consider a canonical embedding

    i    : A →∏_X : (A → X) → X    
    i    ≡λ a. λ (X, g).ga

for a base type A :.
In polymorphic type theory
it follows from a free theorem that i is an isomorphism.
In homotopy type theory
an immediate consequence of a free theorem is the fact that
i is 0-connected, that is, it induces
a bijection between the sets of connected components.
A 0-connected map is far from an isomorphism.
However, for each n ≥ 1 and a : A,
it follows from a free theorem for the type

    ∏_X : ∏_g : A → X^n(X, ga)

that i induces a 0-connected map

    ^n(i) : ^n(A, a) →^n(∏_X : (A → X) → X, ia)

between the n-th loop spaces.
Therefore we conclude that i is ∞-connected, that is,
it induces a bijection between the n-th homotopy groups
for each n ≥ 0.
Hence the types A and ∏_X : (A → X) → X
are equivalent from homotopical point of view.

For a concrete (higher) inductive type A,
the type ∏_X : (A → X) → X
is equivalent to a type definable in Martin-Löf type theory <cit.>
without univalence or higher inductive types.
For example,

    (∏_X : (^n→ X) → X) ≃
      (∏_X : ∏_x : X^n(X, x) → X)

where ^n is the n-dimensional sphere.
The right hand side of this equivalence
is the Church encoding of n-sphere,
proposed by Shulman[<https://homotopytypetheory.org/2011/04/25/higher-inductive-types-via-impredicative-polymorphism/>].
It follows from the previous paragraph that
every space can be identified via an ∞-connected map
with its Church encoding.
The Church encoding of a space suggests that
generators of its homotopy groups are definable without univalence or higher inductive types.
For example the generator of π_3(^2)
can be defined as polymorphic functions of type
∏_X : ∏_x : X^2(X, x) →^3(X, x).
We can say that the univalence axiom and higher inductive types
are used only for proving that π_3(^2) is the integers
but not needed for creating the generator of π_3(^2).

Free theorems for general open terms in homotopy type theory
should follow from relational parametricity,
but it seems to be hard to axiomatize relational parametricity for homotopy type theory.
Thus we focus on free theorems for closed terms
as the first step to understanding relational parametricity
for homotopy type theory,
because free theorems for closed terms follow from Reynolds's abstraction theorem <cit.>
without any assumptions.
Informally, it says that terms evaluated under related environments yield related values.
We show the abstraction theorem for homotopy type theory
via a syntactic transformation of a term in homotopy type theory to another.
The key to prove the abstraction theorem is the fact that
binary type families in homotopy type theory form a model of homotopy type theory
which we call the relational model.
Then the abstraction theorem is the soundness of the interpretation
of types as binary type families.
There is a category-theoretic proof of this fact
using Shulman's inverse diagrams of type-theoretic fibration categories <cit.>
or fibred type-theoretic fibration categories introduced by the author <cit.>.
In this paper we give a syntactic proof
in order to make the paper self-contained.
We also show a new result on inductive data types:
for a type theory with indexed -types,
originally called general trees <cit.>,
the relational model has indexed -types.
The construction of indexed -types in the relational model
is essentially same as that of -types in the gluing construction
for a cartesian functor between Π-pretoposes
<cit.>.

The study of relational parametricity via syntactic transformations is not new.
Abadi et al. <cit.> and
Plotkin and Abadi <cit.>
introduced logic for parametricity
where the abstraction theorem is the soundness of
the interpretations of terms in System F as proofs in their logic.
Wadler pointed out that
Reynolds's abstraction theorem can be seen as
a transformation of a term in System F to a proof in second-order logic
<cit.>.
Takeuti <cit.> and
Bernardy et al. <cit.>
studied relational parametricity for the lambda cube
and pure type systems respectively
via syntactic transformations of a term in one type theory to another.
Since homotopy type theory, even Martin-Löf type theory,
is powerful enough to express predicates
(reflective in terms of <cit.>),
we can transform a term in homotopy type theory
to another in homotopy type theory itself.
Our contribution is to give transformations of
identity types, the univalence axiom and some higher inductive types.

Organization.
We begin in Section <ref>
by recalling some important types and functions in homotopy type theory.
Section <ref> and <ref>
are the core of this paper.
In Section <ref>
we explain what the abstraction theorem is.
In Section <ref>,
we give some free theorems as corollaries of the abstraction theorem.
In Section <ref>,
we discuss Church encodings of higher inductive types
and give the generator of π_3(^2)
as a polymorphic function.
We prove the abstraction theorem
in Section <ref>, <ref> and <ref>.



§ PRELIMINARIES ON HOMOTOPY TYPE THEORY



We recall some types and functions in homotopy type theory
which are used in Section <ref> and <ref>.
See <cit.> for details.

The key idea of homotopy type theory is to identify types as spaces,
elements as points and equalities as paths.
We think of an identity type x : A, y : A ⊢ x = y
as the space of paths from x to y.
Under this identification,
reflexivity, transitivity and symmetry
correspond to constant path _x : x = x,
path concatenation (-)  (-) : x = y → y = z → x = z
and path inversion (-)^-1 : x = y → y = x respectively.
A function f : A → B acts on paths as
(f, -) : x = y → fx = fy for all x, y : A,
and we will often write (f, p) as fp for p : x = y.
Corresponding to indiscernability of identicals,
there is a function ^C(p, -) : C(x) → C(y)
for x : A ⊢ C(x), x, y : A and p : x = y.
Since the symbol “=” is reserved for identity types,
we write a ≡ b when expressions a and b
are judgmentally or definitionally equal.

A function f : A → B also acts on higher dimensional paths.
For x_1, y_1 : A, x_2, y_2 : x_1 = y_1,
…, x_n, y_n : x_n - 1 = y_n - 1,
we define _n(f, -) : x_n = y_n→_n - 1(f, x_n) = _n - 1(f, y_n)
as _0(f, z) ≡ fz and
_n(f, p) ≡(_n - 1(f, -), p).
We often write _n(f, p) as fp.
There are compositions of higher dimensional paths.
For x_0, y_0 : A, x_1, y_1 : x_0 = y_0,
…, x_n, y_n : x_n - 1 = y_n - 1, σ : x_n = y_n,
p : x' = x_0 and q : y_0 = y',
we set p lσ≡_n(λ s.p  s, σ)
and σr q ≡_n(λ s.s  q, σ).
These operations l and r are called whiskering.

A pointed type is a pair (A, a)
of type A and its inhabitant a : A called a base point.
For a pointed type (A, a) and a natural number n ≥ 0,
the n-th loop space ^n(A, a) of A at a
is a pointed type defined inductively as
^0(A, a) ≡ (A, a) and
^n + 1(A, a) ≡^n(a = a, _a).
Write ^n_a : ^n(A, a) for the base point of ^n(A, a).
A function f : A → B acts on loop spaces
as _n(f, -) : ^n(A, a) →^n(B, fa).

A path space of a product space A × B
is a product of path spaces:
(a, b = a', b') ≃ (a = a') × (b = b')
for a, a' : A and b, b' : B.
We think of a pair p, q of paths p : a = a' and q : b = b'
as a path a, b = a', b' in A × B.
Similarly, we regard a pair l, k
of n-loops l : ^n(A, a) and k : ^n(B, b)
as an n-loop in A × B at a, b.

Let x : A ⊢ B(x) be a type family.
For a path p : a = a' in A and points b : B(a) and b' : B(a'),
the path space from b to b' over p,
written b =_p b', is the type ^B(p, b) = b'.
For an n-loop l : ^n(A, a) and a point b : B(a),
the n-th loop space of B at b over l,
written _l^n(B, b),
is the type _n - 1(λ p.^B(p, b), l) = ^n - 1_b.



§ ABSTRACTION THEOREM EXPLAINED



The abstraction theorem for polymorphic type theory
is explained in terms of set-theoretic relations.
For dependent type theory,
we use type-theoretic relations, namely binary type families.

For a binary type family x : A, x' : A' ⊢A(x, x'),
a family on A is a triple of
x : A ⊢ B(x), x' : A' ⊢ B'(x') and
x : A, x' : A', x : A(x, x'), y : B(x), y' : B'(x')
  ⊢B(x, y, y'),
written x : A⊢B(x)
in short.
Note that B depends on x : A and x' : A' implicitly.

Let x : A⊢B(x)
be a family on a binary type family A.
The dependent product of B over A is the binary type family

    f : ∏_x : AB(x), f' : ∏_x' : A'B'(x') ⊢∏_x : A∏_x' : A'∏_x : A(x, x')B(x, fx, f'x')  .

The dependent sum of B over A is the binary type family

    z : ∑_x : AB(x), z' : ∑_x' : A'B'(x') ⊢∑_x : A(_1(z), _1(z'))B(x, _2(z), _2(z'))  .


For a binary type family A,
the path space of A is the family

    x_0 : A, x'_0 : A', x_0 : A(x_0, x'_0),
    x_1 : A, x'_1 : A', x_1 : A(x_1, x'_1), 
        p : x_0 = x_1, p' : x'_0 = x'_1⊢x_0 =_p, p'x_1

on two copies of A.

A universe of binary type families is a binary type family

    X : , X' : ⊢ X → X' →

where ⊢ is a universe of types.

For each type constant C (for example, , , ,
, ^1, ^2 and so on),
we associate it with a binary type family

    c : C, c' : C ⊢ c = c'  .

Then, by induction, we can associate each type family x : X ⊢ A(x)
with a family of binary type families

    x : X, x' : X, x : X(x, x'), a : A(x),
      a' : A(x') ⊢A(x, a, a')  .

Now the abstraction theorem can be described as follows:

[Abstraction Theorem]
For each term x : X ⊢ t(x) : A(x),
there exists a term

    x : X, x' : X', x : X(x, x') ⊢t̂(x) : A(x, t(x), t(x')).

In particular, for each closed term ⊢ t : A,
there exists a closed term

    ⊢t̂ : A(t, t).





§ ABSTRACTION THEOREM APPLIED






 §.§ Concatenation of a Loop



Let t be a closed term of type

    t : ∏_X : ∏_x : Xx = x → x = x.

One might guess that t is an iterated concatenation of a loop,
that is,

    t(p) ≡p … p_n times

for a fixed integer n,
where negative n means (-n) times concatenation of the inversion of p.
In fact any closed term of this type
must be homotopic to some iterated concatenation of a loop,
but one can derive a theorem without this fact.
We show that the type

    ∏_X, X' : ∏_f : X → X'∏_x : X∏_p : x = xt(fp) = f(tp)

is inhabited.
From the abstraction theorem we have a closed term

    t̂ : ∏_(X : , X' : , X : X → X' →)∏_(x : X, x' : X', x : X(x, x'))∏_(p : x = x, p' : x' = x', p : x =_p, p'x)x =_tp, tp'x.

For a function f : X → X' of -small types,
let X(x, x') ≡ fx = x'.
One can prove that, for p : x = x, p' : x' = x' and x : fx = x',
the type x =_p, p'x is equivalent to
the type x p' = fp x.
Letting x' ≡ fx and x≡_fx,
we have an inhabitant of the type

    ∏_p : x = x, p' : fx = fx, p : p' = fp
       tp' = f(tp).

Finally we set p' ≡ fp and p≡_fp.
Then we have an inhabitant of the type

    ∏_x : X∏_p : x = xt(fp) = f(tp).




 §.§ Loop Operations



The example in Section <ref> can be generalized.
Let n and k be natural numbers
and t a closed term of type

    t : ∏_X : ∏_x : X^n(X, x) →^k(X, x).

The example in Section <ref>
is the case when n = k = 1.
This type represents the k-th loop space of n-sphere,
discussed in Section <ref>,
and thus we could not guess what function t is.
However, we can derive a theorem about t.
We show that the type

    ∏_X, X' : ∏_f : X → X'∏_x : X∏_p : ^n(X, x)
       t(fp) = f(tp)

is inhabited.
From the abstraction theorem we have a closed term

    t̂ : ∏_(X : , X' : , X : X → X' →)∏_(x : X, x' : X', x : X(x, x'))∏_(p : ^n(X, x), p' : ^n(X, x'), p : ^n_p, p'(X, x))^k_tp, tp'(X, x).

For a function f : X → X' of -small types,
let X(x, x') ≡ fx = x'.
One can prove that, for p : ^n(X, x),
p' : ^n(X, x') and x : fx = x',
the type ^n_p, p'(X, x) is equivalent to
the type xl p' = fp rx.
Letting x' ≡ fx, x≡_fx,
p' ≡ fp and p≡_fp,
we have an inhabitant of the type
∏_x : X∏_p : ^n(X, x)t(fp) = f(tp).



 §.§ Action on Loops


Let t be a closed term of type

    t : ∏_X, Y : ∏_f : X → Y∏_x : Xx = x → fx = fx.

One might guess that t(f, p) ≡(f, p).
Of course, t could be another function, for example,
t(f, p) ≡(f, p  p).
However, intuitively only (f, p)
is an interesting function of this type,
because (f, p  p) is a composition of (f, p)
and a loop concatenation, and the latter does not use f.

Let us to formulate this intuition.
We show that the type

    ∏_X, Y : ∏_f : X → Y∏_x : X∏_p : x = x
       t(f, p) = f(t(𝕀_X, p))

is inhabited.
This means that, for any t,
t(f, -) is a composition of (f, -)
after a loop operation t(𝕀_X, -) : x = x → x = x.
From the abstraction theorem we have an inhabitant of the type

    ∏_X', X, Y', Y : ∏_g : X' → X∏_h : Y' → Y∏_f' : X' → Y'∏_f : X → Y∏_σ : ∏_x' : X'f(gx') = h(f'x')
       ∏_x' : X'∏_p' : x' = x'
    t(f, gp') σ(x') = σ(x')  h(t(f', p')).

Letting X' ≡ Y' ≡ X, h ≡ f,
f' ≡ g ≡𝕀_X and σ≡λ x._fx,
we have

    ∏_X, Y : ∏_f : X → Y∏_x : X∏_p : x = x
       t(f, p) = f(t(𝕀_X, p)).

Note that, from Section <ref>,
we also have f(t(𝕀_X, p)) = t(𝕀_Y, fp).



 §.§ An Embedding



For a base type A : such as  and ^1,
let A≡∏_X : (A → X) → X.
There are back and forth functions between the types
A and A as follows:

    i     : A →∏_X : (A → X) → X    
    i    ≡λ(a : A).λ(X : , g : A → X).ga 
    
    j     : (∏_X : (A → X) → X) → A    
    j    ≡λ(φ : ∏_X : (A → X) → X).φ_A(𝕀_A).

Clearly j ∘ i ≡𝕀,
but i ∘ j ≡𝕀 or even i ∘ j ∼𝕀
does not hold.
However, given a closed term t : A,
we can construct a closed term of type

    ∏_X : ∏_g : A → X(i(jt))g = tg.

To show this, let t : A be a closed term.
From the abstraction theorem we can get a closed term of type
∏_X_0, X : ∏_f : X_0→ X∏_g : A → X_0f(tg) = t(f ∘ g).
Taking X_0≡ A and g ≡𝕀_A,
we get an inhabitant of the type f(t(𝕀_A)) = t(f).
Now, for X : and g : A → X, we have
(i(jt))g = g(jt) = g(t(𝕀_A)) = t(g).



 §.§ An ∞-Connected Map



For a type A, let π_0(A) be the set of
homotopy equivalence classes of closed terms of A
which we call the 0-th homotopy group of A.
For a point a : A and a natural number n,
the n-the homotopy group of A at a, written π_n(A, a),
is the set π_0(^n(A, a)).
From Section <ref>,
we get a bijection π_0(A) →π_0(A).
We can extend this result to all homotopy groups.
We show that i : A →A is ∞-connected
in the sense that it induces a bijection between the n-th homotopy groups
for each n ≥ 0.

For a pointed types (A, a) : _,
A has a base point
a≡λ(X : , g : A → X).ga.
The maps i and j preserve base points,
and thus they induce maps
^n(i) : ^n(A, a) →^n(A, a)
and ^n(j) : ^n(A, a) →^n(A, a).
Identifying ^n(A, a) with
∏_X : ∏_g : A → X^n(X, ga)
by the functional extensionality,
we get:

    ^n(i)     : ^n(A, a) →∏_X : ∏_g : A → X^n(X, ga)    ^n(i)     =
    λ p.λ(X, g).gp 
    ^n(j)     : (∏_X : ∏_g : A → X^n(X, ga)) →^n(A, a)    ^n(j)     =
    λφ.φ_A(𝕀_A).

Then we have ^n(j) ∘^n(i) = 𝕀_^n(A, a).
For a closed term t : ^n(A, a),
we can construct a closed term of type

    ∏_X : ∏_g : A → X
       (^n(i)(^n(j)t))g = tg

in a similar way to Section <ref>.
Thus we conclude that the map i induces a bijection

    π_n(A, a) →π_n(A, a)

for each n ≥ 0.



 §.§ Free Theorems for Open Terms



In the reflexive graph model of Atkey et al. <cit.>,
free theorems can be derived not only for closed terms
but also for open terms.
In our framework,
we cannot derive free theorems for open terms in general.
Indeed, the negation of the free theorem for some open term is provable.

Assuming the law of excluded middle for propositions in a universe ,
one can construct a function t : ∏_X : X → X
such that t_(0) = 1 and t_(1) = 0
where 0 : and 1 : are the constructors
of the two point type : <cit.>.
Note that recently Booij et al. has pointed out that, conversely,
the existence of a non-trivial polymorphic endofunction
implies the law of excluded middle <cit.>.
Since the law of excluded middle for propositions in 
can be expressed by some closed type _,
t can be regarded as an open term

    l : _⊢ t : ∏_X : X → X.

For this open term the free theorem

    ∏_X, X' : ∏_f : X → X'∏_x : Xt(fx) = f(tx)

fails by taking f ≡λ x.0 : →.
Since the law of excluded middle is consistent,
the free theorem for t is not provable.



§ CHURCH ENCODINGS OF SPACES




In Section <ref>,
for each type A : we have an ∞-connected map
i : A →A
where A≡∏_X : (A → X) → X.
For a concrete (higher) inductive type A,
using the recursion principle of A
we have the Church encoding of A
in Martin-Löf type theory without univalence or higher inductive types.
If A has a base point a_0 : A,
The Church encoding of A is of the form

    ∏_X : ∏_x : XF_A(X, x) → X

and its n-th loop space is

    ∏_X : ∏_x : XF_A(X, x) →^n(X, x),

where F_A(X, x) is a type defined from X and x
using only dependent products, dependent sums and path spaces.
The Church encoding of a type A
suggests that we can construct generators of homotopy groups of A
without univalence or higher inductive types,
although we need univalence and higher inductive types
to prove that they are actually generators of homotopy groups.

In this section we describe Church encodings
of some higher inductive types.
We also define the Hopf map
and give a generator of the third homotopy group of 2-sphere
as a polymorphic function.



 §.§ The Circle


The circle ^1 is a higher inductive type
generated by a point constructor _1 : ^1
and a path constructor _1 : _1 = _1.
It has a recursion principle

    (^1→ X) ≃∑_x : Xx = x.

Therefore

    ^1≃∏_X : ∏_x : Xx = x → X.

The constructors are defined as polymorphic functions

    _1   ≡λ (X, x, p).x :
    ∏_X : ∏_x : Xx = x → X 
    _1   ≡λ (X, x, p).p :
    ∏_X : ∏_x : Xx = x → x = x




 §.§ Spheres


For a natural number n,
the n-sphere ^n
is a higher inductive type generated by
a point constructor _n : ^n
and a path constructor _n : ^n(^n, _n).
We have

    ^n≃∏_X : ∏_x : X^n(X, x) → X.

The constructors are defined as polymorphic functions

    _n   ≡λ (X, x, p).x :
    ∏_X : ∏_x : X^n(X, x) → X 
    _n   ≡λ (X, x, p).p :
    ∏_X : ∏_x : X^n(X, x) →^n(X, x)

The k-th loop space of ^n
is ∏_X : ∏_x : X^n(X, x) →^k(X, x)
studied in Section <ref>.



 §.§ Suspensions


For a type A, the suspension A of A
is a higher inductive type generated by
point constructors :  A and :  A
and a path constructor : A → =.
We have

    A≃∏_X : ∏_x, y : X(A → x = y) → X.




 §.§ Joins


For types A and B,
the join A  B of A and B
is a higher inductive type generated by
point constructors : A → A  B and : B → A  B
and a path constructor : ∏_a : A∏_b : B(a) = (b).
We have

    A  B≃∏_X : ∏_s : A → X∏_t : B → X
       (∏_a : A∏_b : Bsa = tb) → X.




 §.§ The Hopf Map


The Hopf map is a function ^3→^2
whose fiber at the base point is ^1.
Identifying ^3≃^1^1
and ^2≃^1,
the Hopf map h : ^1^1→^1
is defined as
h((x)) ≡,
h((y)) ≡,
and h((x, y) = (h_1(x, y)),
where
h_1 : ^1→^1→^1
is a function defined as
h_1(_1, y) ≡ y,
h_1(_1, _1) = _1^-1,
and h_1(_1, _1) is given by a proof of
_1^-1_1 = __1 = _1_1^-1.

We define the Hopf map as a polymorphic function.
Observe that

    ^1^1→ X 
    ≃∑_f, g : ^1→ X∏_x, y : ^1fx = gy 
    ≃   ∑_x : X∑_l : x = x∑_y : X∑_k : y = y∑_p : x = y∑_α : l  p = p∑_β : p  k = p(αr k) β = (l lβ) α

and

    ^1→ X
       ≃∑_x, y : X^1→ x = y
       ≃∑_x, y : X∑_p : x = yp = p.

Then we define

    h :     (∏_X : ∏_x, y : X∏_l : x = x∏_k : y = y∏_p : x = y∏_α : l  p = p∏_β : p  k = p
    (αr k) β = (l lβ) α→ X) 
       → (∏_X : ∏_x, y : X∏_p : x = yp = p → X) 
    
    h(f) ≡   λ (X, x, y, p, α).
    f(X, x, y, _x, _y, p, α^-1, α, α̌)

where α̌ is a proof of α^-1α = _p = αα^-1.



 §.§ A Generator of π_3(^2)


The Hopf map is a generator of π_3(^2).
We describe the generator as a polymorphic function.

First we define a 3-loop of ^1^1
as a polymorphic function.
We have to construct a function

    l_3 : ∏_X : ∏_x, y :X∏_l : x = x∏_k : y = y∏_p : x = y∏_α : l  p = p∏_β : p  k = p
       (αr k) β = (l lβ) α→^3(X, x).

By path induction on p,
we can assume y ≡ x and p ≡_x.
Then the goal becomes

    l'_3 : ∏_X : ∏_x : X∏_l, k : x = x∏_α : l = _x∏_β : k = _x
       (αr k) β = (l lβ) α→^3(X, x).

For σ : (αr k) β = (l lβ) α,
define l'_3(σ) : ^2_x = ^2_x
as the following concatenation:

    ^2_x
       = (β^-1 (αr k)^-1)
        ((αr k) β)
       E, σ= (α^-1 (l lβ)^-1)
        ((l lβ) α)
       = ^2_x

where E ≡ E(α, β) : β^-1 (αr k)^-1
   = α^-1 (l lβ)^-1
is the path described in Figure <ref>,
also defined as E(^2_x, ^2_x) ≡^3_x
by path induction on α and β.


Now we can define a 3-loop of ^1
in a similar way to the Hopf map:

    c     : ∏_X : ∏_x, y : X∏_p : x = yp = p →^3(X, x) 
    
    c    ≡λ (X, x, y, p, α).
    l_3(X, x, y, _x, _y, p, α^-1, α, α̌).

We can also define it as an element of ^3(^2):

    c     : ∏_X : ∏_x : X^2(X, x) →^3(X, x) 
    
    c    ≡λ (X, x, α).
    l_3(X, x, x, _x, _x, _x, α^-1, α, α̌).

In fact c(α) is the concatenation of paths

    ^2_x = αα^-1E=α^-1α = ^2_x

where E comes from the commutativity of concatenation of higher loops.

Here is a natural question.


Is any generator of a homotopy group of a space
definable as a polymorphic function without univalence or higher inductive types?


This question is important because
it measures power of univalence and higher inductive types.
If the answer to the question is yes,
we can say, informally, that univalence and higher inductive types
give proofs that some elements are different
but do not generate new elements,
although there is a problem
which terms we should think of as proofs,
because in dependent type theory elements and proofs are not distinguished.



§ HOMOTOPY TYPE THEORY



In the rest of this paper we prove the abstraction theorem.
We begin with a quick review of homotopy type theory <cit.>.

In this paper we consider the Martin-Löf's dependent type theory
T with countably many univalent universes

    _0 : _1 : _2 : …,

an empty type : _0,
a one point type : _0,
a two point type : _0,
indexed -types [t, A, B]
and n-spheres ^n : _0.
The existence of ordinary -types is not enough to construct -types in the relational model,
and we require indexed -types.
In extensional type theory
the existence of -types implies the existence of indexed -types
<cit.>,
but in intensional type theory this does not hold
due to the lack of equalizers.
Also to construct general higher inductive types in the relational model
we need some class of indexed higher inductive types,
but we do not know such a class of higher inductive types.
Therefore we deal with only constant higher inductive types ^n.

For a type family i : I, x : A(i) ⊢ B(x)
and a function i : I, x : A(i), y : B(x) ⊢ t(y) : I,
the -type [t, A, B] of B on A indexed over t
is an inductive type family i : I ⊢[t, A, B](i)
with a single constructor

    i : I, a : A(i), f : ∏_y : B(a)[t, A, B](ty)
      ⊢_[t, A, B](a, f) : [t, A, B](i).

We often omit the subscript _[t, A, B] of the constructor and
write it simply as .
The indexed -type has an induction principle:
given a type family i : I, w : [t, A, B](i) ⊢ D(w)
and a term

    i : I, a : A(i), f : ∏_y : B(a)[t, A, B](ty),
      g : ∏_y : B(a)D(fy) ⊢ d(a, f, g) : D((a, f)),

we get a term

    i : I, w : [t, A, B](i) ⊢_[t, A, B]^D(d, w) : D(w)

together with a computational rule

    _[t, A, B]^D(d, (a, f)) ≡ d(a, f, λ(y : B(a))._[t, A, B]^D(d, fy)).

There are projections

    i : I ⊢_1 : [t, A, B](i) → A(i) 
        i : I ⊢_1((a, f)) ≡ a 
        i : I ⊢_2 : ∏_w : [t, A, B](i)∏_y : B(_1(w))[t, A, B](ty) 
        i : I ⊢_2((a, f)) ≡ f.


Some important types are definable from these types.
Ordinary -types _x : AB(x) are -types indexed over
the function B →.
The type  of natural numbers is defined as

    ≡_x : _(, , x),

where _(, ) : →_0 is a function defined by recursion
as _(, , 0_) ≡ and
_(, , 1_) ≡.
A coproduct A + B of two types A, B : is defined as

    A + B ≡∑_x : _(A, B, x).


For a function f : A → B, define

    (f) ≡(∑_g : B → A∏_a : Ag(fa) = a)
      ×(∑_h : B → A∏_b : Bf(hb) = b)

and (A ≃ B) ≡∑_f : A → B(f).
For types A, B :, define a function _A, B : A = B → A ≃ B by path induction
as (_A) is the identity function on A.
The univalence axiom is the axiom that  is an equivalence:

    _ : ∏_A, B : (_A, B).




§ RELATIONAL MODEL



The key to prove the abstraction theorem is the fact that
binary type families x : A, x' : A' ⊢A(x, x')
form a model (T) of homotopy type theory
which we call the relational model.

Families x : A⊢B(x)
of binary type families
are defined in Section <ref>.
A term of a family x : A⊢B(x)
is a triple of terms
x : A ⊢ b(x) : B(x), x' : A' ⊢ b'(x') : B'(x') and
x : A, x' : A', x : A(x, x') ⊢b(x) : B(x, b, b'),
written x : A⊢b(x) : B(x)
in short.
In Section <ref>,
we defined dependent products, dependent sums,
path spaces and universes of binary type families.
It remains to construct other types and check the univalence axiom.

For a type constant C ≡, , , ^n,
the binary type family c : C, c' : C ⊢ c = c'
has the same constructors and
satisfies the same induction principle as those of C.
For example, c : , c' : ⊢ c = c'
has two constructors (0_, 0_, _0_)
and (1_, 1_, _1_).
To see the induction principle of two point type,
let c : , c' : , c : c = c', x : A(c), x' : A'(c') ⊢A(c, x, x')
be a family on c = c' and
(a_0 : A(0_), a'_0 : A'(0_), a_0 : A(_0_, a_0, a'_0))
and (a_1 : A(1_), a'_1 : A'(1_), a_1 : A(_1_, a_1, a'_1))
be elements of A.
We have to construct terms
c : ⊢ f(c) : A(c),
c' : ⊢ f'(c') : A'(c') and
c : , c' : , c : c = c' ⊢f(c) : A(c, f(c), f'(c'))
such that f(0_) ≡ a_0, f(1_) ≡ a_1,
f'(0_) ≡ a'_0, f'(1_) ≡ a'_1,
f(_0_) ≡a_0 and
f(_1_) ≡a_1.
Define f and f' by -induction.
By path induction,
to construct f it suffices to give a term
c : ⊢f(_c) : A(_c, f(c), f'(c)),
which is given by -induction.

To define indexed -types,
suppose that we get a family of binary type families
i : I, x : A(i)
  ⊢B(x)
and a term
i : I, x : A(i),
  y : B(x) ⊢t(y) : I.
First we have indexed -types
i : I ⊢[t, A, B](i)
and i' : I' ⊢[t', A', B'](i')
which we refer to as W(i) and W'(i') respectively.
We have to construct a type
i : I, i' : I', i : I(i, i'),
  w : W(i), w' : W'(i') ⊢W(i, w, w').
Let J ≡∑_i : I∑_i' : I'I(i, i') × W(i) × W'(i').
Define type families j : J ⊢Ǎ(j) and
j : J, x : Ǎ(j) ⊢B̌(x) as

    Ǎ(i, w, w')    ≡A(i, _1(w), _1(w')) 
    B̌((i, w, w'), a)    ≡∑_b : B(_1(w))∑_b' : B'(_1(w'))B(a, b, b').

Define a term j : J, x : Ǎ(j), y : B̌(x) ⊢ť(y) : J as

    ť((i, w, w'), x, (b, b', b)) ≡
      (t(b), t'(b'), t(b), _2(w)(b), _2(w')(b')).

Then we set

    W(i, w, w') ≡[ť, Ǎ, B̌](i, w, w').

We have a constructor

    i : I, i' : I', i : I(i, i'),
    a : A(i), a' : A'(i'), a : A(i, a, a'), 
        f : ∏_y : B(a)W(t(y)),
    f' : ∏_y' : B'(a')W'(t'(y')),
    f : ∏_y : B(a)∏_y' : B'(a')∏_y : B(a, y, y')W(t(y), f(y), f'(y')) 
       ⊢_[ť, Ǎ, B̌](a, f) :
    W(i, _[t, A, B](a, f), _[t', A', B'](a', f')).

One can check the induction principle of indexed -type.
Note that we have formalized, in Agda[<http://wiki.portal.chalmers.se/agda/>],
the construction of indexed -types
in the relational model[<https://gist.github.com/uemurax/040d22a4c037f5323ed26fbee6420544>].

We give a sketch of a proof that
a universe X : , X' : ⊢ X → X' →
of binary type families satisfies the univalence axiom.
Recall that  satisfies the univalence axiom if and only if
the canonical function

    e     : →∑_X, X' : X ≃ X'    
    e(X)    ≡ (X, X, 𝕀_X)

is an equivalence.
Observe that in (T)
a function f : A→B
is an equivalence if and only if
f : A → B and f' : A' → B' are equivalences and
f(x, x') : A(x, x') →B(fx, f'x')
is an equivalence for all x : A and x' : A'.
Therefore, to show that X → X' → is univalent,
it suffices to see that

    e : (X → X' →) →∑_X, Y : X → X' →∏_x : X∏_x' : X'X(x, x') ≃Y(x, x')

is an equivalence for all X, X' :.
There is an equivalence

    (∑_X, Y : X → X' →∏_x : X∏_x' : X'X(x, x') ≃Y(x, x'))
      ≃(X → X' →∑_X, Y : X≃Y),

and e is homotopic to

    (X → X' → e) : (X → X' →) →
      (X → X' →∑_X, Y : X≃Y)

along this equivalence.
The function (X → X' → e) is an equivalence
by univalency of .



§ THE ABSTRACTION THEOREM



In Section <ref>
we see that the binary type families form a model (T)
of Martin-Löf's dependent type theory
with countable univalent universes, an empty type,
a one point type, a two point type, indexed -type and n-spheres.
Thus we have an interpretation - : T→(T).
- takes a type judgment x : X ⊢ A(x)
to a type judgment

    x : X, x' : X, x : X,
      a : A(x), a' : A(x') ⊢A(x, a, a')

and a term judgment x : X ⊢ t(x) : A(x)
to a term judgment

    x : X, x' : X, x : X⊢t(x) : A(x, t(x), t(x')).

Now the abstraction theorem is proved by taking t̂≡t.


For each term x : X ⊢ t(x) : A(x),
there exists a term

    x : X, x' : X', x : X(x, x') ⊢t̂(x) : A(x, t(x), t(x')).






