Examples of crazy judgmental equalities
source link: https://groups.google.com/g/homotopytypetheory/c/CMoXw0wrfx0/m/5nrdWoMxsosJ
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Examples of crazy judgmental equalities
Andrej Bauer
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
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 [email protected].
> For more options, visit https://groups.google.com/groups/opt_out.
Jason Gross
Guillaume Brunerie
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 <[email protected]>:
Michael Shulman
<[email protected]> wrote:
> (A × Unit) = A
> (Unit -> A) = A
*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
Kevin Watkins
Guillaume Brunerie
> On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie
> <[email protected]> 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.
(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
Jason Gross
Nicolai Kraus
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.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.
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
<[email protected]> wrote:
> On 2013/9/16 Michael Shulman <[email protected]> wrote:
>> On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie
>> <[email protected]> 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 [email protected].
> For more options, visit https://groups.google.com/groups/opt_out.
Bas Spitters
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
Martin Escardo
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
M.
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK