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 $\texttt{Id } A~x~y$ as $K \times \texttt{Id } A~x~y$ where $K$ is an arbitrary pointed type (equipped with a distinguished element $\star_K : K$). $\texttt{refl}$ is then interpreted as $(\star_K, \texttt{refl})$, and the interpretation of the type $\texttt{Id Type bool bool}$ has $K$ 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 $\texttt{Id Type}$ 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 also`fun 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: Jun 13 2024 at 19:02 UTC