The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, January 21, 2012 03:13:25 AM AUGER Cédric wrote:
> Axiom X : Type.
> 
> Axiom X_const : ((X->Prop)->Prop) -> X.
> 
> Axiom X_rect : forall (T:X->Type), (forall f:(X->Prop)->Prop, T
> (X_const f)) -> forall x, T x.
> (*What I would expect for the record*)
> 
> Axiom X_const_inj : forall f (P:X->Prop) (Q:((X->Prop)->Prop)->Prop),
>                     forall f', (P (X_const f) -> P (X_const f')) ->
>                     Q f -> Q f'.

I would replace this with the reduction principle for what X_rect does on the 
image of X_const:

Axiom X_rect_red : forall P Pconst f,
  X_rect P Pconst (X_const f) = Pconst f.

Definition X_const_inv (x:X) :
  (X->Prop) -> Prop :=
X_rect (fun _ => (X->Prop)->Prop)
  (fun f => f) x.

Lemma X_const_inv_is_left_inv :
  forall f, X_const_inv (X_const f) = f.
Proof.
intros.
unfold X_const_inv.
rewrite X_rect_red.
reflexivity.
Qed.

Corollary X_const_injective :
  forall f g, X_const f = X_const g -> f = g.
Proof.
intros.
apply f_equal with (f:=X_const_inv) in H.
repeat rewrite X_const_inv_is_left_inv in H.
exact H.
Qed.

(* and as a bonus... *)
Lemma X_const_inv_is_right_inv :
  forall x, X_const (X_const_inv x) = x.
Proof.
induction x using X_rect.
f_equal; apply X_const_inv_is_left_inv.
Qed.
-- 
Daniel Schepler