Stream: Coq users

Topic: Inversion on Sets

Li Zhou (Apr 23 2023 at 09:17):

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.

Meven Lennon-Bertrand (Apr 24 2023 at 08:30):

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.

Meven Lennon-Bertrand (Apr 24 2023 at 08:34):

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.

Meven Lennon-Bertrand (Apr 24 2023 at 08:37):

Ah nevermind, you still can

James Wood (Apr 24 2023 at 09:17):

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

Gaëtan Gilbert (Apr 24 2023 at 09:50):

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

Li Zhou (Apr 24 2023 at 10:35):

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.

Li Zhou (Apr 24 2023 at 10:50):

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.

James Wood (Apr 24 2023 at 12:31):

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.

Gaëtan Gilbert (Apr 24 2023 at 12:38):

with univalence you can use cardinals instead of empty type, eg
by univalence nat * bool = bool * nat
by injectivity bool = nat

Li Zhou (Apr 24 2023 at 13:17):

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.

Meven Lennon-Bertrand (Apr 24 2023 at 14:12):

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.

Li Zhou (Apr 24 2023 at 16:09):

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.

Meven Lennon-Bertrand (Apr 24 2023 at 16:49):

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: Oct 04 2023 at 22:01 UTC