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.
if they all map eq to eq
Not sure what you mean by that
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.
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.
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.
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?
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?
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…
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.
Btw, do you know of the HoTT zulip? There are probably more experts on this kind of questions there than here.
I did not. I shall inquire there, thank you!
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.
You can probably cook up a model of CIC where you interpret an identity type as where is an arbitrary pointed type (equipped with a distinguished element ). is then interpreted as , and the interpretation of the type has 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).
how does that work when we can prove UIP for eg Id unit _ _
?
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).
By parametricity (depending on the details) either the only valid element is refl or the other elements are all equal to it.
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)
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 differently from other identity types and using in some way the fact that the universe is somewhat indiscrete in MLTT ?
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...
Ah, dammit, of course in vanilla CIC you are killed by this
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
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 alsofun x => orb x false
,fun x => andb x true
and all these composed for ever? :D
Precisely :')
... 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: Oct 13 2024 at 01:02 UTC