Library axiomtypes

Require Export types.

Require Import Setoid.
Require Import Coq.Classes.Morphisms.

Axiom maptype_application: prop_maptype_application.
Axiom maptype_application_t: prop_maptype_application_t.
Axiom maptype_trans: prop_maptype_trans.

Theorem maptype_rect: type_maptype_rect.
Theorem maptype_rect_r: type_maptype_rect_r.
Theorem maptype_rect_t: type_maptype_rect_t.
Theorem maptype_rect_tr: type_maptype_rect_tr.
Theorem maptype_ind: prop_maptype_ind.
Theorem maptype_ind_t: prop_maptype_ind_t.

Lemma maptype_rectX: prop_maptype_rectX.

Theorem maptype_returnpi: prop_maptype_returnpi.

Theorem maptype_sym: prop_maptype_sym.

Theorem sym_eqtype: prop_sym_eqtype.

Theorem trans_eqtype: prop_trans_eqtype.

Theorem maptype_proof_irrelevance: prop_maptype_proof_irrelevance.

Theorem maptype_selfany: prop_maptype_selfany.


Add Parametric Relation (A : Type) : A (@eqtype A A)
 reflexivity proved by (ref_eqtype A)
 symmetry proved by (sym_eqtype A A)
 transitivity proved by (trans_eqtype A A A)
as eqtype_as_eq.



Add Parametric Morphism (A:Type) (P:A->A): P with
signature (@eqtype A A) ==> (@eqtype A A) as eqtype_self2.
Qed.

Add Parametric Morphism (A:Type) (P:A->A->A): P with
signature (@eqtype A A) ==> (@eqtype A A) ==> (@eqtype A A) as eqtype_self3.
Qed.


Theorem transform: forall (A B:Type) (E:A=B) (x:A),
{y:B | x==y}.
Implicit Arguments transform [A B].

Theorem typerewrite_Prop: forall (A B:Type) (E:A=B)
(P:A->Prop) (x:A), P x ->
{y:B & {Q:B->Prop | x==y /\ P==Q /\ Q y}}.

Theorem typerewrite_simple: forall (A B:Type) (a x:A) (y:B),
a=x -> x==y -> a==y.

Lemma maptype_undo: forall (A B:Type) (E:A=B) (x y:A),
maptype E x=maptype E y -> x=y.

Theorem maptype_fun : forall (A B C:Type)
(E:B=C) (F:(A->C)=(A->B)) (f:A->C) (x:A),
maptype E ((maptype F f) x) = f x.

Theorem maptype_fun_t : forall (A B C:Type)
(E:B=C) (F:(A->B)=(A->C)) (f:A->B) (x:A),
maptype E (f x) = (maptype F f) x.

Theorem maptype_identity: forall (A B:Type)
(E:A=B) (EB:(A->A)=(A->B)) (x:A),
maptype EB (fun x:A=>x) x=maptype E x.

Theorem maptype_constant: forall (A B C:Type) (E:A=B)
(EC:(A->C)=(B->C)) (x:B) (y:C),
maptype EC (fun x:A => y) x=y.

Theorem maptype_dependent_g: forall (A B:Type) (E:A=B)
(g:A->Type) (x y:A) (EA:x=y) (Eg:(g x)=(g y))
(f:forall a:A,g a),
maptype Eg (f x)=f y.

Theorem maptype_dependent: forall (A B C:Type) (E:A=B)
(F:(A->C)=(B->C)) (f:forall X:Type,X->C),
maptype F (f A)=f B.

Theorem maptype_mapproduct: forall (A B C:Type) (a:A) (b:B)
(f:forall (X:Type), X->C), a==b -> f A a=f B b.

Theorem maptype_square: forall (A B C D:Type) (AB:A=B) (CD:C=D)
(ACBD:(A->C)=(B->D)) (ACAD:(A->C)=(A->D)) (f:A->C) (x:A),
(maptype ACBD f) (maptype AB x)=(maptype ACAD f) x.

Theorem eqtype_to_eq: prop_eqtype_to_eq.