Stream: Coq users

Topic: Limits of proofs about X=X


view this post on Zulip SoundLogic (Nov 16 2023 at 06:09):

I know that without axioms one can't prove that all proofs of the type X=X are eq_refl. I know this can be proven for decidable types. I know (though haven't worked through the proof) that in HoTT with the univalence axiom (base=base)=Z for circles and such.

What other things can be proven without axioms though? In particular, I'm wondering if it can be proven that bool = bool has at most two inhabitants, one which corresponds to the identity function and definitely exists, and one of which corresponds to negation and may or may not exist. Or the possibly weaker statement of if they all map eq to eq. I'm also wondering whether or not it can be proven that all proofs of Prop = Prop map iff to iff, or if some map to things weaker than iff or stronger than iff, or if they at least only map to things along the lines of SProp squashed versions of iff or decidable only versions of iff or such, or if they can actually map to wilder things like eq or the universal relation.

And then more generally, what else can be proven about such things? Is base=base provable without axioms to be isomorphic to Z at least? That sort of thing.

view this post on Zulip Gaëtan Gilbert (Nov 16 2023 at 08:26):

if they all map eq to eq

Not sure what you mean by that

view this post on Zulip SoundLogic (Nov 16 2023 at 08:30):

As in, forall e : bool = bool, @eq bool = eq_rect bool (fun T : Type => T -> T -> Prop) (@eq bool) bool e. Which does hold and is actually easy to prove now that I look at it, since eq is itself polymorphic.

view this post on Zulip Pierre-Marie Pédrot (Nov 16 2023 at 08:38):

The circle type is not part of CIC, so the question of what base = base means without axioms is not really meaningful. Now, if you axiomatize this HIT with its constructors, recursor and equations, AFAIK it's perfectly fine to interpret it in a theory with definitional UIP just as unit. It is the trivial quotient of the unit type, which is literally the unit type.

view this post on Zulip Pierre-Marie Pédrot (Nov 16 2023 at 08:47):

As for the "at most two inhabitants", I think that this is very sensitive to the way you phrase this property. You cannot say that there are two proofs p and q s.t. for all r, p = r ∨ q = r without having a way to turn negation into an equality, and if you start saying something along the lines of "for all p q r, not all three are pairwise different" I'm willing to be that there are models negating this for sordid reasons.

view this post on Zulip SoundLogic (Nov 16 2023 at 08:47):

OK. So the circle one can't be proven without more. Huh. What about something like forall (e : Prop = Prop) (x y : Prop), eq_rect_r (fun T : Type => T) x e <-> eq_rect_r (fun T : Type => T) y e -> x <-> y? That one obviously holds classically, and in any setting where iff becomes eq it holds for the same reason as the previous. A negation transport like in the bools would imply a classical situation. A double negation as the transport would imply double negation is invertible which also implies a classical situation. I'm having trouble picturing what sort of model it could fail to hold in, the transport would have to go kind of weirdly squiggly I think?

view this post on Zulip SoundLogic (Nov 16 2023 at 08:52):

As for the inhabitants of bool = bool, I believe that would follow if showing that the function from bool = bool to (bool,bool) that transports (true,false) along the equivalence (fun e : bool = bool => eq_rect_r (fun T : Type => (T * T)%type) (true, false) e, I'm not sure if I'm phrasing this stuff right) is itself injective, or at least from showing something close to that is injective. Right?

view this post on Zulip Meven Lennon-Bertrand (Nov 16 2023 at 10:06):

For bool = bool, I'm pretty sure you can show in CIC that there are exactly two isos on bool, the identity and negation. Then you can also show that any equality e : bool = bool gives rise to an isomorphism, by transport. So if you can show that this latter map is injective, then you would obtain that there is at most two proofs of equality. Is this true though?

Or, more generally, (when) is the map to_iso : forall X : Type, (X = X) -> iso X injective? If you can, then proving things about the type of isos would give you things about the type of identifications, too…

view this post on Zulip SoundLogic (Nov 16 2023 at 10:10):

Yes. That was exactly my thought. Something like that holds in HoTT, and it trivially holds classically. But I'm not sure if it holds everywhere, or if it can be proven without axioms or extensions. It feels like it ought to, by something along the lines of a free theorem based on the fact that to_iso can be defined out of parametricity respecting components, but I played around some with some similar things and nothing came of it.

view this post on Zulip Meven Lennon-Bertrand (Nov 16 2023 at 10:14):

Btw, do you know of the HoTT zulip? There are probably more experts on this kind of questions there than here.

view this post on Zulip SoundLogic (Nov 16 2023 at 10:14):

I did not. I shall inquire there, thank you!

view this post on Zulip Li-yao (Nov 16 2023 at 12:04):

I doubt that mapping from equalities to isos can be proved to be injective in CIC. On the contrary, what could go wrong if we postulated the existence of a p : bool = bool with p <> eq_refl and to_iso p = id? There's not much we can do with such a p <> eq_refl assumption.

view this post on Zulip Kenji Maillard (Nov 17 2023 at 10:27):

You can probably cook up a model of CIC where you interpret an identity type Id A x y\texttt{Id } A~x~y as K×Id A x yK \times \texttt{Id } A~x~y where KK is an arbitrary pointed type (equipped with a distinguished element K:K\star_K : K). refl\texttt{refl} is then interpreted as (K,refl)(\star_K, \texttt{refl}), and the interpretation of the type Id Type bool bool\texttt{Id Type bool bool} has KK distinct elements (in particular it can be arbitrary large). To complete the model you need to show that the dependent eliminator (path induction) has an interpretation: I expect that it should be possible to provide one by maintaining the invariant that the first component of the pair in the interpretation of the identity type cannot be observed (using parametricity).

view this post on Zulip Gaëtan Gilbert (Nov 17 2023 at 10:37):

how does that work when we can prove UIP for eg Id unit _ _?

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2023 at 10:39):

I thought a bit about that yesterday along the lines of some parametric exceptional model but then you have to be very careful about the phrasing of having no more than n elements (hence my remark).

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2023 at 10:40):

By parametricity (depending on the details) either the only valid element is refl or the other elements are all equal to it.

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2023 at 10:42):

with the negative statement (i.e. not all n proofs of x = x are pairwise distinct you can pull this off in the pext model, I think)

view this post on Zulip Kenji Maillard (Nov 17 2023 at 14:51):

Gaëtan Gilbert said:

how does that work when we can prove UIP for eg Id unit _ _?

Indeed, what I propose would contradict Hedberg theorem. Maybe part of the idea can be salvaged by interpreting Id Type\texttt{Id Type} differently from other identity types and using in some way the fact that the universe is somewhat indiscrete in MLTT ?

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2023 at 14:57):

I'm pretty sure you can show in CIC that there are exactly two isos on bool, the identity and negation.

Reacting a bit late, but @Meven Lennon-Bertrand another respectable expert falling to the funext trap...

view this post on Zulip Meven Lennon-Bertrand (Nov 17 2023 at 15:57):

Ah, dammit, of course in vanilla CIC you are killed by this

view this post on Zulip Pierre Rousselin (Nov 17 2023 at 16:07):

Is it that there are at least fun x => x, fun x => negb x, fun x => negb (negb x), fun x => negb (negb (negb x))) and also fun x => orb x false, fun x => andb x true and all these composed for ever? :D

view this post on Zulip Meven Lennon-Bertrand (Nov 17 2023 at 16:16):

Pierre Rousselin said:

Is it that there are at least fun x => x, fun x => negb x, fun x => negb (negb x), fun x => negb (negb (negb x))) and also fun x => orb x false, fun x => andb x true and all these composed for ever? :D

Precisely :')

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2023 at 16:44):

... and potentially many more, there are many neutrals under a context of type bool. You can prove that extensionally there is only identity and negation though (i.e. any such isomorphism is pointwise equal to one of those two).


Last updated: Jun 13 2024 at 19:02 UTC