Judgemental equality crisis

[Martin Escardo]

This list has been dormant for a while, and so I thought I should pick
your brains.

In Martin-Loef type theory, of any variety:

Given the path induction principle J, we can construct another path
induction principle J', such that:

(0) J and J' have the same type, definitionally (=judgementally).

(1) J' satisfies the "computation rule", a definitional equality,
that specifies J, again definitionally.

(2) There is a path from J to J' (a point of the type Id _ J J').

(3) But J is not definitionally the same as J'.

(4) In particular, there is a non-trivial path from J to J.

Question (that just occurred to me before I tried to think about it):

Is the type of J a proposition? It should be, but this was never
questioned or proved (as far as I am aware). Is the path induction
principle J (homotopy) unique?

Vladimir makes the point that the type of univalence is a proposition,
on the grounds that an axiom should not admit more than one
realizer. Shouldn't we require the same for J, even if it is not an
axiom? Particularly in cubicaltt, where J is not inductively defined,
but is instead derived from other stuff?

And: Does it matter whether J satisfies the computational rule? This
question is not original with me, but is related to the above
questions. The cubicaltt J does not satisfy the computation rule
definitionally, in which case the above question becomes more
pressing.

Martin

[Jason Gross]

    Is the type of J a proposition? It should be, but this was never

    questioned or proved (as far as I am aware). Is the path induction

    principle J (homotopy) unique?

If you also assume the propositional computation rule, yes.  Is the computation rule derivable from the path induction principle itself?

Require Import HoTT.Basics HoTT.Types HoTT.Tactics.

Lemma J_hprop `{Funext}

: forall (J1 J2 : forall {A} (x : A) (P : forall y, x = y -> Type) (k : P x idpath),

                    { J : forall y (p : x = y), P y p | J x idpath = k } ),

  forall A x P k,

    (@J1 A x P k) = (@J2 A x P k).

Proof.

  intros.

  apply path_sigma_uncurried.

  refine (_; _).

  { repeat (apply path_forall; intro).

    path_induction.

    transitivity k.

    { exact (J1 A x P k).2. }

    { symmetry; exact (J2 A x P k).2. } }

  { simpl.

    transport_path_forall_hammer.

    simpl.

    rewrite transport_paths_l.

    rewrite inv_pV.

    rewrite concat_pp_p.

    rewrite concat_Vp.

    rewrite concat_p1.

    reflexivity. }

Defined.

Martin

--
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/d/optout.

[Jon Sterling]

Interesting question! I am not fully familiar with what things satisfy
which computation rules in the various incarnations of HoTT, so you will
have to forgive the fact that I will try and refer only to standard type
theory and not use HoTT as an example; but presumably, the insights from
how TT works in a realizability-based setting may transfer over to HoTT
if it becomes possible to understand HoTT in that light.

I think it is certainly not necessary for two realizers of an induction
principle to be definitionally (intensionally) equal, at least from a
type-theoretic perspective. Of course, it is probably reasonable to
expect that all realizers of an induction principle be computationally
equal (i.e. p ~ p' according to Howe's bisimulation[1]), and from this,
it follows that they should be propositionally equal, because
computational equivalence is a congruence.

From a Brouwerian realizability perspective, having intensionally
different realizers for an induction principle is inevitable, since at
any time, I may add a new non-canonical operator to the theory along
with a computation rule. (For instance, one realizer might be general
recursion, and another may be implemented using structural recursion; it
is probably even possible to consider the possibility of a realizer is
an oracle, i.e. defined individually on every natural number as an
infinitely wide term). So, there may be infinitely many operators
"natrec" which realize the induction principle for the natural numbers,
but they should be computationally equivalent (and thence
propositionally equivalent).

The intensional equality that allows you to distinguish two different
implementations of the J realizer is really something that just
shouldn't be accessible in type theory at all. Requiring the judgemental
equality to be decidable leads to other counter-intuitive things, like
the fact that a unicity principle for the induction principle of the
naturals may not be admitted. In Nuprl, the finest-grained equality that
you can access is Howe's computational equality, which seems to
establish once and for all a minimum acceptable level of abstraction. I
think something similar may be accomplished for HoTT using an HTS-style
approach, where the judgemental equality is repaired to establish the
bare minimum level of abstraction, and the identification types are used
to express truly non-trivial equivalences.

My best wishes,
Jon

[1]
http://www.cs.cornell.edu/info/Projects/Nuprl/documents/howe/EqualityinLazy_LICS89.pdf

[Martin Escardo]

Nice.

No, the computation rule is not derivable from the type of J, because in
cubicaltt there is a J that satisfies the "computation rule" up to a
path but not definitionally. (And I doubt that some magic could cook up
a new J' of the same type that does satisfy the computation rule.)

Martin

> <mailto:HomotopyTypeTheory%2Bunsu...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.
>
>

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Andrea Vezzosi]

On Tue, Jun 30, 2015 at 9:40 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Nice.
>
> No, the computation rule is not derivable from the type of J, because in
> cubicaltt there is a J that satisfies the "computation rule" up to a
> path but not definitionally. (And I doubt that some magic could cook up
> a new J' of the same type that does satisfy the computation rule.)

The question is about propositional equality though, Jason proof shows
that knowing that two combinators J1 and J2 come with a proof of "Id
(P x) (J x refl) x" is enough to prove they are equal, using funext.

I don't think there's a way to implement a function with the type of J
that does not have that property, because of parametricity, but I
would also be surprised if we can prove that it always holds.

Best,
Andrea

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[Gershom B]

Hi Martin.

The construction you describe, which “takes a J” and “generates an imposter J” sounds interesting but I can’t quite envision it, especially such that it holds “in MLTT of any variety”. (Who is to say we can’t have an MLTT that computes this on the nose?).

Could you pass along the code that illustrates this?

Thanks,
Gershom

[Dan Licata]

Hi Martin,

I think this is the comment "Condition (i) is also a mere proposition, but we will not prove this." after Theorem 5.8.2 in the book:
- For any pointed type (A,a0) and pointed family (R : A -> Type, r0 : R a0), a witness that R is an identity system (def 5.8.1) is a "J rule" for R with a "propositional beta" saying that the "J rule" takes r0 to the point you give it.
- The comment after the theorem is that being an identity system is a mere proposition, which means that any two "J rules with propositional beta rules" for R are propositionally equal.

Though there is no proof in the book, I just proved it here:
https://github.com/dlicata335/hott-agda/blob/master/misc/JUnique.agda
by showing that Theorem 5.8.2(i) (i.e. the type of identity systems on R) and Theorem5.8.2(iv) (i.e. the type of witnesses that Sigma R is contractible) are in fact equivalent (the theorem in the book is just logical equivalence) and then using univalence and the fact that (iv) is an hprop (because it's contractibility of something). Though the equivalence of (i) and (iv) is for any identity system, you need identity types to define "propositional beta rule" for (i) and "contractible" for (iv), so I should say that this is done in Agda with univalence and funext and an identity type with a definitional computation rule on refl. However, I'd guess that basically the same proof would work in cubical type theory, too.

Specializing this to the identity type, we get

overall : (A : Type) (a0 : A)
-> HProp ((C : (Σ a.Id a0 a) → Type)
(b0 : C (a0 , refl)) →
Σ (λ (PI : (p : Σ a. Id a0 a) → C p) →
Id (PI (a0 , refl)) b0))

so the type of "J's with a propositional computation rule" is an hprop.

Another route to the same result would be to show that Theorem 5.8.2(i) and Theorem 5.8.2(ii) are equivalent, which would be showing that "R has J+propositional beta" is equivalent to "R is a homotopy-initial fibration generated by a point over a0", which is analogous the theorems Kristina Sojokova et al. have proved about W-types and higher inductive types. I tried this first, but it seemed more annoying to prove than the (i)-(iv) equivalence.

-Dan

[Martin Escardo]

On 30/06/15 21:33, Gershom B wrote:> Hi Martin.

> The construction you describe, which “takes a J” and “generates an
> imposter J” sounds interesting but I can’t quite envision it,
> especially such that it holds “in MLTT of any variety”. (Who is to
> say we can’t have an MLTT that computes this on the nose?).
> Could you pass along the code that illustrates this?

It is here: http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda2.html

The more general question is what judgemental equality gives you.
Sometimes it is a lot: For example, the judgemental equality of the
-1-truncation HIT gives you function extensionality,

But if you assume propositional resizing, you can show that
-1-truncations exist (with the required judgemental equality) iff
function extensionality holds. So this judgemental equality gives you
no more than function extensionality.

I wonder if an analogous result holds for "weak" J, namely a J that
works as usual, but with its computation rule replaced by a path
(either axiomatized, like in HoTT, or proved/constructed, like in
cubicaltt).

I am undecided about this question.

But I definitely regard the notion of judgemental equality as rather
fishy (and I gather that I am not the only one, by many personal
discussions with many of you). It doesn't make part of my conception
of mathematical objects that exist (for example in my mind) before I
attempt to formalize them (in a paper, in a talk, in Agda, in
cubicaltt, or even set theory (if I am pressed by somebody to code my
thoughts in ZFC)).

Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

On 30/06/15 21:33, Gershom B wrote:
> Hi Martin.
>
> The construction you describe, which “takes a J” and “generates an imposter J” sounds interesting but I can’t quite envision it, especially such that it holds “in MLTT of any variety”. (Who is to say we can’t have an MLTT that computes this on the nose?).
>
> Could you pass along the code that illustrates this?

It is here: http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda2.html

The more general question is what judgemental equality gives you.
Sometimes it is a lot: For example, the judgemental equality of the
-1-truncation HIT gives you function extensionality,

But if you assume propositional resizing, you can show that
-1-truncations exist (with the required judgemental equality) iff
function extensionality holds.

I wonder if an analogous result holds for "weak" J, namely a J that
works as usual, but with its computation rule replaced by a path (either
axiomatized, like in HoTT, or proved/constructed, like in cubicaltt).

I am undecided about this question.

But I definitely regard the notion of judgemental equality as rather
fishy. It doesn't make part of my conception of mathematical objects
that exist before I attempt to formalize them.

Martin

[Martin Escardo]

Nice. Thanks for the discussion and the code. Martin