Examples of crazy judgmental equalities

[Andrej Bauer]

Last semester at IAS there was much discussion about extending type
theory with "questionable" judgmental equalities, such as
extensionality for natural numbers. What are some other examples that
would be desirable to have? I am asking so that it is easier to think
about proof assistants that would support such black magic.

With kind regards,

Andrej

[Steve Awodey]

definitional computation rules for the generating paths in HITs.

S

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.

[Jason Gross]

I'd be interested in seeing the following as judgemental equalities:

A generalized generalized eta rule that [match] commutes with any function which is polymorphic over the indices of the inductive data type.  So, for example, with [paths] which has two parameters ([A : Type] and [x : A]) and one index (of type A), the rule is

  ∀ A (x y : A) (P : ∀ a, x = a → Type) (f : ∀ a (p : x = a), P a p) (p : x = y),

    f _ p

    = match p as p0 in (_ = y0) return (P y0 p0) with

        | idpath ⇒ f _ idpah

      end.

and for [JMeq], the rule is

  ∀ A (x : A) (P : ∀ B (b : B), JMeq x b → Type) (f : ∀ B (y : B) (p : JMeq x y) → P B y p) B (y : B) (p : JMeq x y),

    f _ _ p

    = match p as p0 in (@JMeq _ _ B0 y0) return (P B0 y0 p0) with

        | JMeq_refl ⇒ f _ _ JMeq_refl

      end.

and for [sum], the rule is

  ∀ A B (P : A + B → Type) (f : ∀ x, P x) (x : A + B),

    f x

    = match x as x0 return P x0 with

        | inl a ⇒ f (inl a)

        | inr b ⇒ f (inr b)

      end.

By combining the case that [f] is a constructor applied to projections with the case that [f] is the identity, I think this rule suffices to obtain eta for records.

(I shudder a bit to think how hard this would be make normalizing.)  (I've submitted a feature request for this for Coq, at https://coq.inria.fr/bugs/show_bug.cgi?id=3119)

----------------------

[transport_compose : ∀ {A B x y} (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)), transport (fun x0 => P (f x0)) p z = transport P (ap f p) z], or, in [match]es,

  match p in (_ = x0) return (P (f x0)) with

    | idpath => z

  end

  = match (match p in (_ = x0) return (f x = f x0) with idpath => idpath end) in (_ = fx0) return (P fx0) with

        | idpath => z

      end

----------------------

I'd also like to see a generalization of transport_compose, which I haven't figured out the details of yet, which makes [inverse (inverse p) = p] a judgemental equality for all paths p.

----------------------

The following (partial) computation rule for matching on higher inductive types:

Given a higher inductive type [T] and a path constructor [p : a = b], any match of the form

  match p in (_ = y) return (P (match y with a => c | b => d | p => f end)) with

    | idpath => g

  end

should be convertible with

  match f in (_ = y) return (P y) with

    | idpath => g

  end

In terms of [transport : ∀ {A} (P : A → Type) {x y} (p : x = y), P x → P y], this says that

  transport (fun y : T => P (T_elim (a_case := c) (b_case := d) (p_case := f) y) p

should be convertible with

  transport (fun y => P y) f

----------------------

I might like some sort of judgemental rule about what to do if the argument to the return clause of a match/the argument to the first non-implicit argument to transport is used multiple times, as in "transport (fun y => y x = y z) ...", and how to split this up into multiple nested matches over the same path.  I wonder if something like this would make, e.g., "projT1_path_sigma : forall {A} {P : A -> Type} {u v : exists x, P x} (p : u .1 = v .1) (q : transport P p u .2 = v .2), (path_sigma P u v p q) ..1 = p" a judgemental equality.  But I haven't thought about this one enough to say much.

-Jason

[Guillaume Brunerie]

A while ago, Vladimir sent an email to the Coq mailing list containing
several interesting examples of "crazy" definitional equalities, for
instance
(A × Unit) = A
(Unit -> A) = A

We can invent more like that, for instance (Empty -> A) = Unit, or
(Bool -> Bool) = (Bool × Bool).

Guillaume

2013/9/16 Jason Gross <jason...@gmail.com>:

[Michael Shulman]

On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie
<guillaume...@gmail.com> wrote:
> (A × Unit) = A
> (Unit -> A) = A

Personally, my initial reaction is that equalities of this sort would
*not* be "desirable". I feel like they would probably subvert some of
the value of type theory as an organizing structure for mathematics.

One which hasn't been mentioned yet, though, is judgmental univalence:

Id_Type(A,B) = Equiv(A,B)

and similarly, judgmental funext:

Id_{A\to B)(f,g) = Pi_{a:A} Id_B(fa,ga)

and so on for a lot of the other theorems in chapter 2 (including I
think some of Jason's proposals). These go along with the expectation
of a "computational" meaning of HoTT.

[Steve Awodey]

right - that's what makes them "crazy".

[Kevin Watkins]

Regarding Michael's examples, I guess I would have expected that in a computationally adequate system, there would be coercions between the types on either side that would judgmentally be inverses, rather than that the types would be judgmentally equal.

[Guillaume Brunerie]

On 2013/9/16 Michael Shulman <shu...@sandiego.edu> wrote:
> On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie
> <guillaume...@gmail.com> wrote:
>> (A × Unit) = A
>> (Unit -> A) = A
>
> Personally, my initial reaction is that equalities of this sort would
> *not* be "desirable". I feel like they would probably subvert some of
> the value of type theory as an organizing structure for mathematics.

I agree with you, but isn’t that precisely what Andrej is looking for
(he said "crazy" judgemental equalities)? In my opinion, having a type
theory where type checking is not decidable is not desirable already
anyway and I think Andrej’s question is more about judgemental
equalities that do not preserve decidability of type checking in
general.
For computation rules of HITs or judgemental univalence, there is some
hope that we won’t need any black magic there because they should be
part of the computational interpretation of HoTT (which should have
decidable type checking).
For extensionality for natural numbers, as far as I understand we
cannot hope to have decidable type checking so we have to use the kind
of black magic Andrej is talking about.

Guillaume

[Michael Shulman]

His subject line said "crazy", but the text of his email asked "What

are some other examples that would be desirable to have?"

On Mon, Sep 16, 2013 at 9:01 AM, Guillaume Brunerie

[Jason Gross]

Generalizing the idea of equality reflection for nat, it might be interesting/useful to have a built-in type of "types with decidable equality", and then grant equality reflection for anything of that type.  Perhaps it should be possible to construct such a type by giving a type together with a function that decides equality on that type.

More decidably, it might be nice to be able declare that some finite set of symbols (e.g., "+", "*", "-", "S", "O") are mutually decidable, provide a normalizer for terms which use only those symbols (and possibly have to proof the relevant features of your normalization procedure so that it plays well with the rest of the kernel), and then get equality reflection for any terms that normalize to the same thing.  (I think I might have gotten this idea from Paolo Capriotti, whom I think mentioned to me at OPLSS the suggestion that the typechecker has a ring solver built into it, and any equations this solver can solve can be taken as judgemental.)

-Jason 

[Nicolai Kraus]

On 16/09/13 20:26, Jason Gross wrote:

Generalizing the idea of equality reflection for nat, it might be interesting/useful to have a built-in type of "types with decidable equality", and then grant equality reflection for anything of that type. �Perhaps it should be possible to construct such a type by giving a type together with a function that decides equality on that type.

That one sounds dangerous. Given any a:A, the type� Sigma (b : A). a = b� trivially has decidable equality, but you don't want to grant equality reflection to it: If you make (a,refl) and (b,p) judgmentally equal, you also make their first projection judgmentally equal. I learnt this argument from Peter L in a similar discussion.
The other ideas sound interesting though.
Nicolai

More decidably, it might be nice to be able declare that some finite set of symbols (e.g., "+", "*", "-", "S", "O") are mutually decidable, provide a normalizer for terms which use only those symbols (and possibly have to proof the relevant features of your normalization procedure so that it plays well with the rest of the kernel), and then get equality reflection for any terms that normalize to the same thing. �(I think I might have gotten this idea from�Paolo Capriotti, whom I think mentioned to me at OPLSS the suggestion that the typechecker has a ring solver built into it, and any equations this solver can solve can be taken as judgemental.)

-Jason�

On Monday, September 16, 2013, Michael Shulman wrote:

His subject line said "crazy", but the text of his email asked "What
are some other examples that would be desirable to have?"

On Mon, Sep 16, 2013 at 9:01 AM, Guillaume Brunerie
<guillaume...@gmail.com> wrote:
> On 2013/9/16 Michael Shulman <shu...@sandiego.edu> wrote:
>> On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie
>> <guillaume...@gmail.com> wrote:

>>> (A � Unit) = A

>>> (Unit -> A) = A
>>
>> Personally, my initial reaction is that equalities of this sort would

>> *not* be "desirable". �I feel like they would probably subvert some of

>> the value of type theory as an organizing structure for mathematics.
>

> I agree with you, but isn�t that precisely what Andrej is looking for

> (he said "crazy" judgemental equalities)? In my opinion, having a type
> theory where type checking is not decidable is not desirable already

> anyway and I think Andrej�s question is more about judgemental

> equalities that do not preserve decidability of type checking in
> general.
> For computation rules of HITs or judgemental univalence, there is some

> hope that we won�t need any black magic there because they should be

> part of the computational interpretation of HoTT (which should have
> decidable type checking).
> For extensionality for natural numbers, as far as I understand we
> cannot hope to have decidable type checking so we have to use the kind
> of black magic Andrej is talking about.
>
> Guillaume
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.

[Bas Spitters]

This is the sort of thing Pierre Yves Strub is trying to do with Coq
modulo theory.

http://pierre-yves.strub.nu/coqmt/

http://hal.inria.fr/inria-00583136/en/

The project may be somewhat stalled since he is now doing interesting
things related to security.

[Jason Gross]

In case any are interested: I was talking with Bruno, and after a bit of pushing, came up with the following generalization of transport_compose, which expresses that you can de-nest matches:

Set Implicit Arguments.

Section ex4.

  Variable T0 : Type.

  Variable T1 : Type.

  Variables t0 t1 : T0.

  Let T := @eq T0 t0. (* must be an inductive type with all parameters filled in, but no indices filled in *)

  Variables f g : forall x : T0, T x -> T1.

  Let P0 x H := @eq T1 (@f x H). (* must end up with an inductive type with all parameters but no indices filled in; must quantify over a [T _], and the arguments to it *)

  Let P x H := @P0 x H (@g x H). (* we get to fill in the indices for [P0] with whatever expression of [x] and [H] we like *)

  Variable Q : forall x H y, @P0 x H y -> Type. (* must take as arguments all arguments to [P0], and all parameters to the relevant inductive type *)

  Goal forall (x : T t1) (y : @P t0 eq_refl) (z : @Q t1 x (@f t1 x) eq_refl),

         match (match x as x' in (_ = u) return @P u x' with

                  | eq_refl => y

                end) as x' in (_ = Px') return (@Q t1 x Px' x') with

           | eq_refl => z

         end

         = match x as x' in (_ = u) return @Q u x' (@f u x') eq_refl

                                           -> @Q u x' (@g u x') (match x' as x'' in (_ = u') return (@P u' x'') with

                                                                   | eq_refl => y

                                                                 end) with

             | eq_refl => fun z => match y as y' in (_ = u) return @Q t0 eq_refl u y' with

                                     | eq_refl => z

                                   end

           end z.

  Proof.

    compute in *; clear.

    destruct x.

    intros.

    destruct y.

    reflexivity.

  Qed.

End ex4.

It might not be confluent, or easy to turn into a reduction rule, though.

-Jason

[Martin Escardo]

The craziest judgemental equalities are of course those of extensional
MLTT (every propositional equality is judgemental).

The craziest judgemental equality I can imagine in HoTT is declaring
that all elements of the hpropositional truncation || X || of a type X
are judgementally equal. How crazy is that? (We had a little
discussion about that in the Agda mailing list some months ago.)

It is not clear to me what the boundary between "questionable" and
"desirable" is. Do you have a criterion?

It is worth remarking that, without univalence, adding certain
judgemental equalities, for example those of the HoTT book for the
type || 2 ||, give function extensionality, and so they are "very
powerful" (going beyond mere convenience in a proof assistant).

Which judgemental equalities can one add (1) without contradicting
univalence, (2) without contradicting the potential computational
content of univalence, and (3) without destroying decidability of
type-checking?

Martin

[Martin Escardo]

And (4) being conservative in a suitable sense.

M.