CODEWITHSUNDEEP
coqdependent-type
tlon
tlon

Reputation: 423

tricky dependent pattern match without axioms

Suppose I have the following type:

Inductive foo : Type -> Type :=
  | A : forall X, Empty_set -> foo X
  | B : foo unit.

Can I prove the following:

Lemma obv : forall x : foo unit, x = B.

without axioms? The dependent destruction tactic takes care of it pretty easily, but that introduces the axiom JMeq_eq. I found this article, but it doesn't seem applicable in this case, since Type doesn't have UIP.

Upvotes: 3

Views: 101

Answers (1)

Jason Gross
Jason Gross

Reputation: 6128

No, this is not provable without something like univalence or UIP. The type foo unit is isomorphic to the type unit = unit, so proving that all inhabitants of foo unit are equal to B is the same as proving that all inhabitants of unit = unit are equal to eq_refl, and this cannot be proven without axioms, in Coq.

Upvotes: 3

Related Questions