The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/07/2016 12:28 PM, Gaetan Gilbert wrote:
> >For instance, one can prove forall (x:True), x = I, but not:
> >
> >Inductive Foo : unit -> Prop := foo : Foo tt.
> >
> >Goal forall (f : Foo tt), f = foo.
>
> You can actually.
>
>
> Inductive Foo : unit -> Prop := foo : Foo tt.
>
> Definition foo_transport : forall (x : unit) (y : unit), Foo x -> Foo y.
> Proof.
> intros [] [];trivial.
> Defined.
>
> Goal forall (f : Foo tt), f = foo.
> Proof.
> assert (H : forall x y (a : Foo x) (b : Foo y), foo_transport _ _ a = b).
> intros x y [] [].
> reflexivity.
> intros.
> etransitivity.
> - symmetry. apply H.
> - apply H.
> Unshelve.
> + exact tt.
> + exact f.
> Defined.
>
> Gaëtan Gilbert

OK - should have seen that coming.  That's a lot like proving UIP for unit.

What I should have said is that you can't prove:

Variable A : Set.
Variable a : A.
Inductive Foo : A -> Prop := foo : Foo a.
Goal forall (f : Foo a), f = foo.

even though there really is only the one foo : Foo a.

-- Jonathan