The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Suppose for example that T= Prop. Then, a function from I1 to T should  
be a triple (P_1, P_2, prf) where P_1, P_2: Prop and prf: P_1 <-> P_2  
is a proof of their equivalence.

V.


On Oct 10, 2009, at 7:28 PM, Thorsten Altenkirch wrote:

> On 11 Oct 2009, at 00:23, Vladimir Voevodsky wrote:
>
> > Excuse me, there was a typo. The correct text is:
> >
> > > > Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
> >
> > What I want here is a type  such that for any type T, a function I1  
> > -> T is given by a triple -- t1:T (its value on x0), t2:T (its  
> > value on x1) and e : eq t1 t2 .
>
> Assuming that eq means equals, aren't two values which are the same  
> not the same as one value?
>
> T.
>
>
> > Also, the definition of Impl given below is meaningless.
> >
> > V.
> >
> >
> >
> > On Oct 10, 2009, at 5:42 PM, Adam Chlipala wrote:
> >
> > > Vladimir Voevodsky wrote:
> > > > Is there a way in Coq to make definitions such as:
> > > >
> > > > Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
> > > >
> > > > or
> > > >
> > > > Inductive Impl : Type := P1: Prop | P2: Prop | impl: P1 -> P2 .
> > >
> > > Neither of these fits the spirit of inductive definitions.  In  
> > > each example, you might want to assert the final "constructor" as  
> > > an [Axiom] instead, but there is almost always a better way to do  
> > > such things.  We can't comment on the better way(s) for your  
> > > specific situation without more background.
> > >
> > > --------------------------------------------------------
> > > Bug reports: http://logical.saclay.inria.fr/coq-bugs
> > > Archives: http://pauillac.inria.fr/pipermail/coq-club
> > >      http://pauillac.inria.fr/bin/wilma/coq-club
> > > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.saclay.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >       http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your computer  
> system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club