One of the most important spaces in homotopy theory is the interval (be it the topological interval or the simplicial interval ). Thus, it is natural to ask whether there is, or can be, an “interval type” in homotopy type theory. Of course, the interval is contractible, so up to homotopy equivalence it might as well be a point, but on the “point-set level” it carries additional structure: it is the “universal space containing two points and a path between them.”
With this in mind, it is natural to define an “interval type” to be inductively generated by two elements and a path between them. The usual sort of inductive types do not allow constructors to specify elements of the path-type of the inductive type, rather than elements of the type itself, but we can envision extending the notion of inductive type to allow this. (Of course, there will be semantical and computational issues to deal with.) I think this idea is due to Peter Lumsdaine.
In general, this sort of “higher inductive type” should allow us to build “cell complexes”, including spheres of all dimensions. But right now I just want to describe the interval type I. It comes with three “constructors” zero:I, one:I, and segment: zero one. Its “elimination rule” says that given any type A with points and a path , there is a specified term such that , , and . (More generally, there should also be a “dependent elimination” property.)
Peter Lumsdaine has “implemented” the interval type in Coq, by asserting I, zero, one, segment, and Ielim as axioms. (See the “Experimental” directory of Andrej’s Github, or Peter’s Github for an older version.) Of course we can’t add new definitional equalities to Coq, but we can assert propositional versions of the computation rules , , and . (The same should be possible for any other “higher inductive type.”) This suffices to prove, for instance, that the interval is contractible.
However, if the above rules are actually definitional, then I claim that the interval type (together with the usual eta rule) implies function extensionality. The idea is quite simple: suppose we have a homotopy . Then for each we have a map . But by currying and uncurrying, that’s the same as having, for every , a map . In particular, applying this to “segment”, we should get a path in the function space from f to g. More precisely, we get a path from eta(f) to eta(g), due to the effects of the curry-uncurry; thus the eta rule finishes off the proof.
I’ve “implemented” this in Coq, insofar as is possible. The following code uses “admit” to solve two goals that ought to be automatic if the computation rules for the interval held definitionally. (It requires both the base library and Interval.v to be loaded.)
Theorem eta_implies_fe : eta_rule_statement -> function_extensionality_statement. Proof. intros etarule A B f g H. set (mate := fun (i:Interval) x => interval_path' (H x) i). path_via (mate zero). path_via (eta f). unfold eta, mate. (* This would be automatic if [interval_path_zero'] were a definitional equality (computation rule). *) admit. path_via (mate one). exact (map mate segment). path_via (eta g). unfold mate, eta. (* Ditto for [interval_path_one']. *) admit. Defined.