Hi, I'm wondering if it's reasonable to do inversion on Sets, e.g., assuming

```
Goal forall (A B C D : Set), (A * B)%type = (C * D)%type -> A = B /\ C = D.
```

It contradicts HoTT or the univalent principle, but does it raise other inconsistencies with standard coq, functional/propositional extensionality, or constructive indefinite description (cid)?

Generally, inversion on types does not work, e.g.,

```
Goal forall (A B C D : Type), (A * B)%type = (C * D)%type -> A = B /\ C = D.
```

One reason is that the above goal contradicts propositional extensionality (prop-ext), which is assumed in many projects/libraries. `(True * False)%type = (False * True)%type`

is provable with prop-ext, but we don't want to have `True = False`

.

This kind of injectivity of type constructors is reasonable, it is how Observational Equality works on types. Since OE also validates function extensionality, your inversion + funext + standard Coq should be consistent. I don't know about cid, though… You can go look up Loic Pujet's PhD if you want to see a system which has such injectivities.

Also, it is not entirely clear to me that

```
Goal forall (A B C D : Type), (A * B)%type = (C * D)%type -> A = B /\ C = D.
```

is inconsistent with propext. Indeed, together they only imply `True = False`

*as types*, ie `@eq Type True False`

, and while it is trivial to derive an inconsistency out of `@eq Prop True False`

, I am not sure you can derive one out of the equality only at the `Type`

level.

Ah nevermind, you still can

In case you haven't come across it, it's also worth noting that injectivity of type constructors is anti-classical.

Meven Lennon-Bertrand said:

Also, it is not entirely clear to me that

`Goal forall (A B C D : Type), (A * B)%type = (C * D)%type -> A = B /\ C = D.`

is inconsistent with propext. Indeed, together they only imply

`True = False`

as types, ie`@eq Type True False`

, and while it is trivial to derive an inconsistency out of`@eq Prop True False`

, I am not sure you can derive one out of the equality only at the`Type`

level.

`@eq Type True False`

implies `True -> False`

ie `False`

, propext is only needed to produce the hypothesis `True * False = False * True`

James Wood said:

In case you haven't come across it, it's also worth noting that injectivity of type constructors is anti-classical.

Thanks for the reference! So, generally, the injectivity of type constructors is inconsistent with Coq; in particular, Prop is coerced to Set, so even the injectivity of set constructors is also weird.

What I'm trying to understand is:

Do these **only** come from the inversion on empty types (False or empty set)? If so, what about restricting ourselves to non-empty types, say:

```
(* restrict to inhabited types that has at least one element *)
Definition ihbType := IhbType {
T : Type;
ihb : T;
}.
Goal forall (A B C D : ihbType), (A * B)%type = (C * D)%type -> A = B /\ C = D.
```

Meven Lennon-Bertrand said:

This kind of injectivity of type constructors is reasonable, it is how Observational Equality works on types. Since OE also validates function extensionality, your inversion + funext + standard Coq should be consistent. I don't know about cid, though… You can go look up Loic Pujet's PhD if you want to see a system which has such injectivities.

Thank you for pointing out OE; I'll read Loic Pujet's thesis.

It's not inconsistent with basic Coq, but yeah, it's inconsistent with several common axioms used in Coq – namely univalence, more specifically proposition extensionality when propositions embed into types (as they do in Coq), and excluded middle. And yes, in the examples I've seen, there's always a crucial use of an uninhabited type.

with univalence you can use cardinals instead of empty type, eg

by univalence `nat * bool = bool * nat`

by injectivity `bool = nat`

Yes, my understanding is that: empty types allow us to forget everything, i.g., the proofs, the dependent parameters, etc., and thus, doing inversions on empty types contradicts some commonly used axioms. Except for univalence (or HoTT) with further axioms on proving the equality of types, Coq + Classical logic seems consistent with the injectivity of inhabited type constructors, and I hope this is true.

Currently, our project is not based on univalence(nor HoTT), and we focus on inhabited types (and make use of mathcomp and mathcomp/analysis, so classical logic is assumed). As such, I'll try to find out if any further weird things occur if only focused on inhabited types.

Note that part (or all ?) of the problem with injectivity of type constructors comes from size considerations (this is described later in the discussion on Coq-club). So it might be perfectly fine to assume injectivity of type constructors as long as an inductive type lives in a universe level higher than that of all its parameters, which is not the case in current Coq If I'm not mistaking, only constructor arguments are taken into account, and indices if the `indices-matter`

flag is enabled. Said flag was introduced while developing the HoTT library, exactly to avoid similar size issues.

Meven Lennon-Bertrand said:

Note that part (or all ?) of the problem with injectivity of type constructors comes from size considerations (this is described later in the discussion on Coq-club). So it might be perfectly fine to assume injectivity of type constructors as long as an inductive type lives in a universe level higher than that of all its parameters, which is not the case in current Coq If I'm not mistaking, only constructor arguments are taken into account, and indices if the

`indices-matter`

flag is enabled. Said flag was introduced while developing the HoTT library, exactly to avoid similar size issues.

Really helps. With enabling `indices-matter`

, the codes discussed in injectivity of type constructors is anti-classical won't work anymore.

so it seems safe to assume injectivity of type constructors then, and also, for different type constructors, they are not equal.

Pujet constructs a set-theoretic model which validates such injectivity/non-confusion of type constructors in their PhD, to model Observational Equality. While the model is not scaled to arbitrary datatypes (yet), I guess it should in principle be reasonable to extend it, under the stronger size restrictions on parameters

Last updated: Jun 24 2024 at 12:02 UTC