The infinite dimensional sphere is contractible

[Guillaume Brunerie]

Hi everyone,

I’m a young French student (I should start a PhD thesis next year) very interested in homotopy type theory. Some of you may already know me, I was at the "Homotopy and equality in type theory" working group in Marseille a few months ago.

In the last few months I played a lot with Coq and HoTT and I proved a few results that could be interesting to share.
In particular I managed to define the infinite dimensional sphere (using higher inductive types) and I proved its contractibility.
The idea of the definition is that you can construct the (n+1)-sphere as the suspension of the n-sphere. You can then define by induction a dependent type [nat -> Type] giving the spheres in every dimension. The total space of this dependent type is the disjoint union of all spheres. It is then easy to define an application of type [forall n : nat, ndim_sphere n -> ndim_sphere (S n)] and you just have to use this application and another HIT to glue all the spheres together.
The contractibility is proven using the fact that the infinite dimensional sphere can also be seen as an infinite dimensional ball which is easily shown to be contractible.

The code is available in my GitHub clone of the HoTT repository [1], and everything I’ve done (except for one or two functions) is in the "Coq/Experimental" directory (see in particular the file "InfiniteSphere.v" for the infinite dimensional sphere).


And here is a fun exercice about higher inductive types (it may sound stupid but it’s not that easy without the computation rules being definitional equalities), my proof is in the CircleWellDefined.v file, if you have a different/better proof I’ll be happy to see it :-) :

Let’s define [circle1] and [circle2] with
Inductive circle1 :=
 | base1 : circle1
 | loop1 : base1 ~~> base1

 

Inductive circle2 :=
 | base2 : circle2
 | loop2 : base2 ~~> base2

 

Prove that [circle1] and [circle2] are equivalent.

NB: I’m using a slightly different (but completely equivalent) type for the computation rules for paths and the proof of the non-dependent computation rule from the dependent one is now much shorter (compare "Coq/HIT/Circle.v" and "Coq/Experimental/Circle.v").


Best regards,

Guillaume Brunerie


[1] : https://github.com/guillaumebrunerie/HoTT

[Peter LeFanu Lumsdaine]

On Mon, Oct 3, 2011 at 9:42 PM, Guillaume Brunerie
<guillaume...@gmail.com> wrote:

> In particular I managed to define the infinite dimensional sphere (using
> higher inductive types) and I proved its contractibility.

Ah, that’s very nice!

> NB: I’m using a slightly different (but completely equivalent) type for the
> computation rules for paths and the proof of the non-dependent computation
> rule from the dependent one is now much shorter (compare "Coq/HIT/Circle.v"
> and "Coq/Experimental/Circle.v").

Hmmm, that’s interesting! (Code excerpted below for comparison.)
Yes, it does simplify the proofs — and also, perhaps, would be better
than our older one if one did want to make this rule an actual
computation rule, since it better fits the general pattern that a
computation rule should be of the form:

(eliminator applied to intro form) → stuff

If I recall correctly, the older form in Coq/HIT/Circle.v was dimly
motivated by the idea that a computation rule should be of the form:

(stuff involving an eliminator applied to intro form) → an input of
the eliminator

which was perhaps mistaken. Comparing them like this, the former
seems to make much more sense, and like it would have a much better
chance of giving good computational properties (some kind of
normalisation, etc.).

Cheers,
–p.

====8<----
-- Guillaume’s version, from Coq/Experimental/Circle.v:
Axiom compute_loop : forall P pt lp,
map_dep (circle_rect P pt lp) loop
~~> map (transport loop) (compute_base P pt lp) @ lp @ !compute_base P pt lp.

-- Older version, from Coq/HIT/Circle.v:
Axiom compute_loop' :
forall (P : circle -> Type) (pt : P base) (lp : transport loop pt ~~> pt),
(! map (transport loop) (compute_base P pt lp)
@ (map_dep (circle_rect P pt lp) loop)
@ (compute_base P pt lp))
~~> lp.
====8<----

[Guillaume Brunerie]

Le 5 oct. 2011 22:37, "Peter LeFanu Lumsdaine"
<p.l.lu...@gmail.com> a écrit :

>
> On Mon, Oct 3, 2011 at 9:42 PM, Guillaume Brunerie
> <guillaume...@gmail.com> wrote:
>
> > In particular I managed to define the infinite dimensional sphere (using
> > higher inductive types) and I proved its contractibility.
>
> Ah, that’s very nice!

Thanks :-)

> > NB: I’m using a slightly different (but completely equivalent) type for the
> > computation rules for paths and the proof of the non-dependent computation
> > rule from the dependent one is now much shorter (compare "Coq/HIT/Circle.v"
> > and "Coq/Experimental/Circle.v").
>
> Hmmm, that’s interesting!  (Code excerpted below for comparison.)
> Yes, it does simplify the proofs — and also, perhaps, would be better
> than our older one if one did want to make this rule an actual
> computation rule, since it better fits the general pattern that a
> computation rule should be of the form:
>
> (eliminator applied to intro form) → stuff
>
> If I recall correctly, the older form in Coq/HIT/Circle.v was dimly
> motivated by the idea that a computation rule should be of the form:
>
> (stuff involving an eliminator applied to intro form) → an input of
> the eliminator
>
> which was perhaps mistaken.  Comparing them like this, the former
> seems to make much more sense, and like it would have a much better
> chance of giving good computational properties (some kind of
> normalisation, etc.).

Yes, while proving various things about higher inductive types I
noticed that it was a lot easier to use the computation rules for
paths as rules saying what [map_dep (eliminator) constructor] should
reduce to.
Also, when proving (for instance) that two HIT are equivalent, the
same pattern is used everytime:
* reduce the innermost [map] with the computation rule for paths
* push every [map] and [!] inside the concatenations
* simplify stuff depending on what you’re trying to prove
* repeat the three previous steps one time
* now try to convince Coq that the result is now obvious (for example
with [cancel_opposites], unfortunately this tactic almost never works
on big lambda terms)
In particular the two first steps really look like a normalisation process.
If I have time and if I understand how tactics work, I'll try to write
tactics to do this automatically.

There is also another pattern present everywhere: when you want to
prove something about the circle (or any other HIT), you want to find
a section of a fibration [P_something : circle -> Type]. You then need
to prove it for the points and the paths of the HIT.
For the points you just prove it as you can, but for the paths you
need to prove something of the form [transport (P := P_something) loop
x ~~> y] where [x] and [y] are instances of what you just proved for
the points and [loop] is a path constructor of the HIT.
But given that you don’t know anything about [loop], it seems that the
only way to prove it is to prove the following lemma first:

Lemma something_transp : forall u v : circle, forall p : u ~~> v,
forall q : P_something u,
transport (P := P_something) p q ~~> {result}.

"{result}" is a term of type [P_something v] and can usually easily be
found (at least if [P_something] is simple), and there is probably
even an algorithm computing it automatically from [P_something], and
the lemma is usually trivial to prove (it’s just [path_induction]
followed by [cancel_units]).

After that, you can apply [something_transp] to the special case [p :=
loop] [q := x] and try to prove that the result is equal to [y].

I noticed this when I tried to prove that there is a group structure
on the circle because there are many small results to prove and I was
always using this method (it isn’t yet on my GitHub because it’s a
mess and it’s not finished at all, but I’ll try to put it soon).

Cheers,

Guillaume

> Cheers,
> –p.
>
> ====8<----
> -- Guillaume’s version, from Coq/Experimental/Circle.v:
> Axiom compute_loop : forall P pt lp,
>  map_dep (circle_rect P pt lp) loop
>  ~~> map (transport loop) (compute_base P pt lp) @ lp @ !compute_base P pt lp.
>
> -- Older version, from Coq/HIT/Circle.v:
> Axiom compute_loop' :
>  forall (P : circle -> Type) (pt : P base) (lp : transport loop pt ~~> pt),
>    (! map (transport loop) (compute_base P pt lp)
>      @ (map_dep (circle_rect P pt lp) loop)
>      @ (compute_base P pt lp))
>    ~~> lp.
> ====8<----
>

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To post to this group, send email to HomotopyT...@googlegroups.com.
> To unsubscribe from this group, send email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/HomotopyTypeTheory?hl=en.
>

[Vladimir Voevodsky]

Hi Guillaume,

I would like to understand better the developments happening in the higher inductive types. Could you write explicitly the introduction/elimination/computation rules which you think one should associate with 2-sphere?

Vladimir.

[Peter LeFanu Lumsdaine]

On Thu, Oct 6, 2011 at 8:13 AM, Guillaume Brunerie
<guillaume...@gmail.com> wrote:

> There is also another pattern present everywhere: when you want to
> prove something about the circle (or any other HIT), you want to find
> a section of a fibration [P_something : circle -> Type]. You then need

> […] to prove the following lemma first:

>
> Lemma something_transp : forall u v : circle, forall p : u ~~> v,
> forall q : P_something u,
>    transport (P := P_something) p q ~~> {result}.
>
> "{result}" is a term of type [P_something v] and can usually easily be
> found (at least if [P_something] is simple), and there is probably
> even an algorithm computing it automatically from [P_something], and
> the lemma is usually trivial to prove (it’s just [path_induction]
> followed by [cancel_units]).

Yes — I’ve found this sort of lemma coming up all the time too, not
just with higher inductive types, but for all sorts of fibrations. I
think you’re right that there should be an algorithm for it: modulo
technical differences in the setting, it should be something like a
version of the “observational equality” of Altenkirch, McBride, Oury,
Swirstra (and others?), which implements equality types and their
elimination rules as constructed types/terms using other constructors;
their clauses for implementing the elimination rule should give us
clauses for working out how transport/subst will act on constructed
fibrations.

I wonder if this could somehow be implemented as a tactic in Coq —
taking a fibration, and using an OTT-like algorithm to (partially?)
unwind what transport will look like in it. It would need some fairly
sophisticated Ltac, I think, but would be very handy indeed.

–p.

[Michael Shulman]

On Thu, Oct 6, 2011 at 12:25 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> it should be something like a version of the “observational
> equality” of Altenkirch, McBride, Oury, Swirstra (and others?),
> which implements equality types and their elimination rules as
> constructed types/terms using other constructors; their clauses for
> implementing the elimination rule should give us clauses for working
> out how transport/subst will act on constructed fibrations.

Do you think this could also tell us how to add HITs to the
"computational univalence" setting of Harper and Licata?

Mike

[Guillaume Brunerie]

2011/10/6 Vladimir Voevodsky <vlad...@ias.edu>:

> Hi Guillaume,
>
> I would like to understand better the developments happening in the higher inductive types. Could you write explicitly the introduction/elimination/computation rules which you think one should associate with 2-sphere?

(a working Coq version of the rules given below is available at

https://github.com/guillaumebrunerie/HoTT/blob/master/Coq/Experimental/2Sphere.v )

Hi Vladimir,

Higher inductive types are a way to translate a (nice) cell decomposition of a topological space into a type in homotopy type theory.
For the 2-sphere, let’s take the following cell decomposition:
The 2-sphere is the topological space freely generated by
* two points [pt0] and [pt1]
* two paths [lp0] and [lp1], both from [pt0] to [pt1]
* two (endpoints preserving) homotopies [sf0] and [sf1] from [lp0] to [lp1] (that is paths from [lp0] to [lp1] in the type [pt0 ~~> pt1])
(there are probably shorter definitions of the 2-sphere, but I find this one better to understand what’s going on)

Hence the pseudo-Coq notation for the 2-sphere is

Inductive sphere : Type :=
  | pt0 : sphere
  | pt1 : sphere
  | lp0 : pt0 ~~> pt1
  | lp1 : pt0 ~~> pt1
  | sf0 : lp0 ~~> lp1
  | sf1 : lp0 ~~> lp1

(where [x ~~> y] is a notation for [paths x y])

And the introduction rules are:

(* Introduction rules *)
sphere : Type
pt0 : sphere
pt1 : sphere
lp0 : pt0 ~~> pt1
lp1 : pt0 ~~> pt1
sf0 : lp0 ~~> lp1
sf1 : lp0 ~~> lp1

For the elimination rule, we are given a fibration [P : sphere -> Type] and we want to know which conditions are needed to construct a section of [P] (and there will be one such condition per introduction rule).

For [pt0] and [pt1], the condition is just that we need to have some [x0] of type [P pt0] and some [x1] of type [P pt1].
* x0 : P pt0
* x1 : P pt1

For [lp0] and [lp1], we would like something like [p0 : x0 ~~> x1], but this is not well typed because [x0 : P pt0] and [x1 : P pt1] do not have the same type. But [lp0] or [lp1] are paths from [pt0] to [pt1], so we can transport [x0] along one of these paths in the fibration [P] and ask for a path between this "new [x0]" (which is now living in [P pt1]) and [x1].
Hence we have to ask for the following (where [transport P p x] is the result of transporting [x] in the fibration [P] along the path [p]) :
* p0 : transport P lp0 x0 ~~> x1
* p1 : transport P lp1 x0 ~~> x1

For [sf0] and [sf1], we would like again something like [s0 : p0 ~~> p1], but this is still not well typed, so we have to transport [p0] along [sf0] (or [sf1]) in order to get something of the same type than [p1]. But the fibration in which we want to transport [p0] is not [P] anymore, but [fun a => transport P a x0 ~~> x1]. This gives the following conditions:
* s0 : transport (fun a => transport P a x0 ~~> x1) sf0 p0 ~~> p1
* s1 : transport (fun a => transport P a x0 ~~> x1) sf1 p0 ~~> p1

Putting all this together, we have the following dependent elimination rule:

(* Elimination rule *)
sphere_rect :
   forall P : sphere -> Type,
   forall x0 : P pt0,
   forall x1 : P pt1,
   forall p0 : transport P lp0 x0 ~~> x1,
   forall p1 : transport P lp1 x0 ~~> x1,
   forall s0 : transport (fun a => transport P a x0 ~~> x1) sf0 p0 ~~> p1,
   forall s1 : transport (fun a => transport P a x0 ~~> x1) sf1 p0 ~~> p1,
   (forall x : sphere, P x).

Now we come to the computation rules.
The computation rules should be roughly of the form "[sphere_rect] applied to some constructor (introduction rule) should reduce to one input of [sphere_rect]".
The first two cases are easy.

(* Computation rules for points *)
(sphere_rect P x0 x1 p0 p1 s0 s1) pt0 == x0
(sphere_rect P x0 x1 p0 p1 s0 s1) pt1 == x1

(where everything at the left is supposed to be well typed and [==] represents definitional equality)

For the paths, you cannot do the same thing, because [lp0] is not an element of type [sphere], so you cannot apply [sphere_rect] to it. But [lp0] is a path between elements of type [sphere] and with the [map_dep] function, you can send paths in [sphere] to paths in the fibration.
(if [P] is a fibration, [f] a section of [P] and [p : x ~~> y] a path in the base space of [P], then [map_dep P f p] is of type [transport P p (f x) ~~> f y])

(* Computation rules for paths *)
map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1) lp0 == p0
map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1) lp1 == p1

Note that we need to have definitional equalities in the computation rules for the points in order to have well typed computation rules for paths, more on this later.

For the 2-paths, it’s the same idea, it will just be a little more complicated. You should get something like this:

(* Computation rules for 2-paths *)
map_dep (fun a => transport P a x0 ~~> x1) (map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1)) sf0 == s0
map_dep (fun a => transport P a x0 ~~> x1) (map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1)) sf1 == s1

Here again you can notice that you need both the computation rules for points and for paths to hold definitionally in order to have something well typed.

Ok, now that I have completely described the introduction/elimination/computation rules for the 2-sphere, there is another problem: how to implement this in Coq?

For the introduction and elimination rules, this is easy, you can just use axioms and the exact form given earlier.

But for the computation rules, you cannot assert new definitional equalities in Coq, so the best you can do is to have computation rules that are only propositional equalities (because we can assert new propositional equalities as axioms).

For the points, this does not change anything.

(* Propositional computation rules for points *)
compute_pt0 : forall P x0 x1 p0 p1 s0 s1, (sphere_rect P x0 x1 p0 p1 s0 s1) pt0 ~~> x0
compute_pt1 : forall P x0 x1 p0 p1 s0 s1, (sphere_rect P x0 x1 p0 p1 s0 s1) pt1 ~~> x1

But for the paths, remember that the computation rules for paths are well typed only if the computation rules for points hold definitionally, and this is not the case here.

More precisely, [map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1) lp0] is of type [transport P lp0 ((sphere_rect P x0 x1 p0 p1 s0 s1) pt0) ~~> (sphere_rect P x0 x1 p0 p1 s0 s1) pt1] and [p0] is of type [transport P lp0 x0 ~~> x1]. These two types should be equal, but for Coq they are not.

So in order to be able to assert the computation rules for paths in Coq, we need to add explicitely the (propositional) computation rules for points where needed. This gives the following :

(* Propositional computation rules for paths *)
compute_lp0 : forall P x0 x1 p0 p1 s0 s1,

  map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1) lp0 ~~>

    map (transport P lp0) (compute_pt0 P x0 x1 p0 p1 s0 s1)

    @ p0

    @ !compute_pt1 P x0 x1 p0 p1 s0 s1

 

compute_lp1 : forall P x0 x1 p0 p1 s0 s1,

  map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1) lp1 ~~>

    map (transport P lp1) (compute_pt0 P x0 x1 p0 p1 s0 s1)

    @ p1 

    @ !compute_pt1 P x0 x1 p0 p1 s0 s1

(where [@] is concatenation of paths and [!] the opposite)

Finally, we also want of course the propositional computation rules for 2-paths. This is usually very problematic because the types are becoming very ugly, but I took my courage in both hands and I finally managed to write it completely. So here are the propositional computation rules for 2-paths:

(* Propositional computation rules for 2-paths *)
compute_sf0 : forall P x0 x1 p0 p1 s0 s1,
  map_dep (fun a => transport P a x0 ~~> x1)
    (fun a => !map (transport P a) (compute_pt0 P x0 x1 p0 p1 s0 s1)
              @ map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1) a
              @ compute_pt1 P x0 x1 p0 p1 s0 s1) sf0
  ~~> map (transport (fun a => transport P a x0 ~~> x1) sf0)
           (compute_lp0' P x0 x1 p0 p1 s0 s1)
      @ s0
      @ !compute_lp1' P x0 x1 p0 p1 s0 s1. 

 

compute_sf1 : forall P x0 x1 p0 p1 s0 s1,
  map_dep (fun a => transport P a x0 ~~> x1)
    (fun a => !map (transport P a) (compute_pt0 P x0 x1 p0 p1 s0 s1)
              @ map_dep P (sphere_rect P x0 x1 p0 p1 s0 s1) a
              @ compute_pt1 P x0 x1 p0 p1 s0 s1) sf1
  ~~> map (transport (fun a => transport P a x0 ~~> x1) sf1)
           (compute_lp0' P x0 x1 p0 p1 s0 s1)
      @ s1
      @ !compute_lp1' P x0 x1 p0 p1 s0 s1.

Finally I would like to add that there are ways to get a 2-sphere that do not involve ugly terms like the previous two.

For example you can first define the suspension of a type with the following (parametrized) higher inductive type:

Inductive suspension (A : Type) : Type :=
  | north_susp : suspension A
  | south_susp : suspension A
  | paths_susp : A -> (north_susp ~~> south_susp).

 

This is a higher inductive type with only points and paths, so this is not difficult to deduce the introduction/elimination/computation rules (you can find them in my GitHub if you want), and you can then define [sphere := suspension (suspension (suspension empty))] where [empty] is the empty type and you have a 2-sphere which is only defined in terms of points and paths, so it will probably be easier to work with this definition.

Guillaume

[Dan Licata]

Just to check that I've understood correctly: if the beta-rule for
circle_rect on the point were definitional, rather than propositional,
then we could use

Axiom compute_loop : forall P pt lp,
map_dep (circle_rect P pt lp) loop

~~> lp.

Yes?

So the question is, which side should the coercions go on when the
beta-rule for points is propositional?

-Dan

On Oct05, Peter LeFanu Lumsdaine wrote:
> On Mon, Oct 3, 2011 at 9:42 PM, Guillaume Brunerie
> <guillaume...@gmail.com> wrote:
>
> > In particular I managed to define the infinite dimensional sphere (using
> > higher inductive types) and I proved its contractibility.
>
> Ah, that’s very nice!
>
> > NB: I’m using a slightly different (but completely equivalent) type for the
> > computation rules for paths and the proof of the non-dependent computation
> > rule from the dependent one is now much shorter (compare "Coq/HIT/Circle.v"
> > and "Coq/Experimental/Circle.v").
>
> Hmmm, that’s interesting! (Code excerpted below for comparison.)
> Yes, it does simplify the proofs — and also, perhaps, would be better
> than our older one if one did want to make this rule an actual
> computation rule, since it better fits the general pattern that a
> computation rule should be of the form:
>
> (eliminator applied to intro form) → stuff
>
> If I recall correctly, the older form in Coq/HIT/Circle.v was dimly
> motivated by the idea that a computation rule should be of the form:
>
> (stuff involving an eliminator applied to intro form) → an input of
> the eliminator
>
> which was perhaps mistaken. Comparing them like this, the former
> seems to make much more sense, and like it would have a much better
> chance of giving good computational properties (some kind of
> normalisation, etc.).
>

> ====8<----
> -- Guillaume#s version, from Coq/Experimental/Circle.v:

[Dan Licata]

Hi Guillaume, Peter, and everyone,

Let me try to recast your comments in indexed categories terminology, as
opposed to fibrations, to see if I've understood. If I'm reading your
Coq code correctly, then the 'something_transp' lemma is expanding the
definition of the functorial action on morphisms of P_something.
Whenever you have a family of types P : A -> type, 'transport' (derived
from J) postulates an action on morphisms (paths in A). But when P is
built out of known type constructors, you know how the functorial action
is defined. For example:

x : A |- B1 x B2 type the functorial action is given by applying the
functorial action of B1 to the first component of the pair, and
the functorial action of B2 to the second component of the pair

x : A |- B1 -> B2 type the functorial action is given by
precomposing with the functorial action of B1 (on !p) and post-composing
with the functorial action of B2

x : A |- C type, x not free in C the functorial action is the identity,
because C is a constant functor

etc.

So, I agree with Peter that there should be a 'something_transp' lemma
whenever P_something is built out of known type constructors, because we
know what the functorial action of each type constructor is.

In fact, Bob Harper and I have a recent paper
(http://www.cs.cmu.edu/~drl/pubs/lh112tt/lh112tt.pdf) showing that these
equations (plus some others) are sufficient to prove a canonicity result
for a 2-dimensional type theory with a simple universe of sets
considered modulo isomorphism. 'something_transp' shows up in the
0-resp rules on pages 4 and 13 (2TT is somewhat stricter than
intensional type theory, in that we take these equations to be
equalities, rather than equivalences).

From a computational perspective, the need for the 'something_transp'
lemmas is clear: In intensional type theory,
'transport (P := P_something) p q' only computes when 'p' is
reflexivity.
But higher-dimensional types add new ways to construct paths (e.g. 'p'
might be an application of univalence), so with only the computation
rule for reflexivity, 'transport' sometimes gets stuck.
In 2TT, transport additionally computes based on the structure of P,
using the definition of the functorial action of each type constructor.
There are similar rules saying that what you call 'map' (and we call
'resp') computes based on the structure of the term being congruenced on
to both sides of the path. These rules suffice to get all transport's
and map's out of your way in a closed term, in the sense that every
closed term of type boolean is definitionally equal to either true or
false.

2TT essentially ports the constructs and equations of Hofmann and
Streicher's groupoid interpretation into the syntax of a type theory.
We thought this made a nice first step towards addressing the harder
question of the computational interpretation of the infinite-dimensional
univalence axiom.

-Dan

[Dan Licata]

Hi Mike,

I don't have the rules written up in a document, but you can add, say,
the interval or the circle to 2TT fairly easily. But 2TT is
2-dimensional, and very strict, so you just take all of the beta-rules
(for points and for paths) as definitional equalities. I'm not sure
what you'd do in a weaker or higher-dimensional setting.

-Dan

[Michael Shulman]

Well, it's a start.

[Steve Awodey]

On Oct 11, 2011, at 11:19 PM, Dan Licata wrote:

> Just to check that I've understood correctly: if the beta-rule for
> circle_rect on the point were definitional, rather than propositional,
> then we could use
>
> Axiom compute_loop : forall P pt lp,
> map_dep (circle_rect P pt lp) loop
> ~~> lp.
>
> Yes?

yes