The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi Gert,

I don't think it is a silly question at all.

The eliminator for an inductive type is the answer to the question: How
can we define a function out of it. So for example in the case of the
natural numbers which are defined via the constructors 0 : Nat and suc :
Nat -> Nat, how can we define a function f : (n : Nat) -> M n where M :
Nat -> Type? The answer is by giving

f 0 = z
f (suc n) = s n (f n)

where z : M 0 and s : (n : Nat) -> M n -> M (suc n).

We ask the same question for the equality type a =_A b where a,b :  A
which is inductively defined via refl : (x : A) -> x =_A x: how can we
define a function 
f : (x y : A)(p : x =A y) -> M x y p with M : (x y : A) -> x =_A y ->
Type? Again the answer is by giving (J)

f x x (refl x) = r x

where r : (x : A) -> M x x (refl x)

However, in this case we may think that the scheme isn't general enough
because we may want to define a function f : (x : A)(p : x = x) -> M x p
where M : (x : A) -> (x = x) -> Type. It seems enough to provide (K)

f x (refl x) = r x

where r : (x : A) -> M x (refl x)

The result due to Hofmann & Streicher shows that the 2nd scheme is not
derivable from the first by showing that the first can be interpreted in
the groupoid model but not the 2nd.

At the time I thought this was a good justification to add the 2nd scheme
(K). Indeed Conor McBride showed that this is enough, once we have K we
can derive all pattern matching definitions. I never understood why it
wasn't added to Coq. When I asked Christine Pauline-Mohring, she said that
they viewed the eliminator for equality just as an instance of a general
scheme and she didn't know how to extend the scheme so that it would cover
K and on the other hand she didn't want to add an ad hoc eliminator just
for equality.

In my view there is one good reason not to add K and this hasn't much to
do with geometry (homotopy theory) but with extensionality. By
extensionality I mean that we view mathmeatical objects how they are used
and not how they are defined. Now given this, answer the question what is
equality of types? If we want to be extensional we cannot refer to the
elements globally. The first approximation is to say that two types are
equal if there is a one-to-one correspondence between their elements.
However, it is this idea which is incompatible with the 2nd eliminator
(K), because there often is more than one 1-1 correspondence between
types, e.g. there are 2 between Bool and itself.

As an aside, once we accept that equality is proof relevant, we have to be
careful with how we define concepts we are used to. So for example: what
is a 1-1 corespondence. We may say that a function f : A -> B is a 1-1
correspondence, iff for every b : B there is a unique a : A such that f a
=_B b. We overlook that while we ask for a unique a we still have a choice
of the equality proof (Indeed this would make the theory inconsistent).
Hence, instead we say that there is a unique a:A, p : f a = b.

Thorsten




On 05/05/2018, 10:30, 
"coq-club-request AT inria.fr
 on behalf of Gert Smolka"
<coq-club-request AT inria.fr
 on behalf of 
smolka AT ps.uni-saarland.de>
 wrote:

>Sorry for the silly question, the answer can be found here, for instance:
>https://homotopytypetheory.org/2011/04/10/just-kidding-understanding-ident
>ity-elimination-in-homotopy-type-theory/
>In short: UIP does not follow from the elimination scheme from eq, as
>proved by Hofmann and Streicher.
>A surprising and counterintuitive fact at first, one could call
>Streicher’s paradox.
>
>Gert
>
>> On 4. May 2018, at 17:01, Gert Smolka 
>> <smolka AT ps.uni-saarland.de>
>>  wrote:
>> 
>> I have a historical question regarding elimination
>> for inductive predicates with indices in Coq.
>> What was the reason for providing only weak elimination that,
>> for instance, cannot derive UIP?
>> 
>> I know that UIP conflicts with univalence, but univalence wasn’t there
>> when Coq was designed.
>> 
>> Thanks for answers,
>> Gert
>> 
>> PS: Two example may help to make my point:
>> 
>> Section UIP.
>>  Variable X: Type.
>>  Variable x: X.
>> 
>>  Inductive eq : X -> Prop := Q : eq x.
>> 
>>  Goal forall p: eq x -> Type,
>>      p Q -> forall y, p y.
>>  Proof.
>>    refine (fun p H y => match y with Q => _ end).
>>  Abort all.
>> End UIP.     
>> 
>> but the following goes through:
>> 
>> Inductive unit: Prop := U: unit.
>> 
>> Goal forall p: unit -> Type,
>>    p U -> forall x, p x.
>> Proof.
>>  refine (fun p H x => match x with U => _ end).
>>  exact H.
>> Qed.
>




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.