Library maptype_standard

Require Import types.

Definition identitytype_ind
 (f:forall (A B:Type), A->B):=
forall (A B:Type) (x:A) (P:A->Prop),
A=B->
(P x<->(f (A->Prop) (B->Prop) P)(f A B x)).

Definition identitytype_ind_t
 (f:forall (A B:Type), A->B):=
forall (A B:Type) (x:A) (P:B->Prop),
A=B->
(P (f A B x)<->(f (B->Prop) (A->Prop) P) x).

Definition identitytype_trans
 (f:forall (A B:Type), A->B):=
forall (A B C:Type) (x:A),
A=B-> B=C -> (f B C (f A B x)=f A C x).

Definition identitytype
 (f:forall (A B:Type), A->B):=
identitytype_ind f /\
identitytype_ind_t f /\
identitytype_trans f.

Definition maptype (A:Type) (B:Type) (EQ:A=B) (x:A):B.
Defined.
Implicit Arguments maptype [A B].
Definition maptype2 (A:Type) (B:Type) (EQ:A=B) (x:A):B.
Defined.

Definition maptypeformula (A:Type) (B:Type) (EQ:A=B)
(P:A->Prop):B->Prop:=maptype (formulae_typeeq EQ) P.
Implicit Arguments maptypeformula [A B].

Definition maptypecompose (A:Type) (B:Type) (C:Type)
(EAB:A=B) (EBC:B=C) (x:A):C.
Defined.
Print maptypecompose.
Eval compute in maptypecompose.
Eval compute in eq_rect.




Theorem maptype_self: forall (A:Type) (x:A),
maptype (refl_equal A) x=x.

Definition prop_proof_irrelevance:=
forall (A : Prop) (a1 a2 : A), a1 = a2.

Inductive eqtype (A B:Type) (x:A):B->Prop:=
refl_equaltype: forall (E:A=B), eqtype A B x (maptype E x).
Implicit Arguments eqtype [A B].
Notation "x == y :> A B":= (@eqtype A B x y) (at level 70, y at next level, no associativity).
Notation "x == y" := (@eqtype _ _ x y) (at level 70, no associativity).

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

Theorem eq_to_eqtype: forall (A:Type) (x y:A),
x=y -> x==y.

Theorem ref_eqtype: forall (A:Type) (x:A), x==x.

Definition prop_eqtype_to_eq:=
forall (A:Type) (x y:A),x==y -> x=y.

Theorem proof_irrelevance_TO_eqtype_to_eq:
prop_proof_irrelevance -> prop_eqtype_to_eq.

Lemma eqtype_rewrite: forall (A:Type) (B:Type) (P:B->Prop)
(x:A) (y:B), x==y -> P y -> {E:A=B| P (maptype E x)}.

Definition prop_eqtype_proof_irrelevance:=
forall (A:Type) (x y:A) (Exy:x=y) (Exx:x=x),Exy==Exx.

Definition prop_maptype_selfany:=
forall (A:Type) (EQ:A=A) (x:A), maptype EQ x=x.

Definition prop_maptype_return:=
forall (A B:Type) (EQ:A=B) (x:A),
maptype (sym_eq EQ) (maptype EQ x)=x.

Definition prop_maptype_returnpi:=
forall (A B:Type) (E:A=B) (F:B=A) (x:A),
maptype F (maptype E x)=x.

Definition prop_maptype_trans:=
forall (A B C:Type) (EQAB:A=B) (EQBC:B=C)
(x:A), maptype EQBC (maptype EQAB x)=
maptype (trans_eq EQAB EQBC) x.

Definition prop_sym_eqtype:= forall (A B:Type) (x:A) (y:B),
x==y -> y==x.

Definition prop_trans_eqtype:=
forall (A B C:Type) (x:A) (y:B) (z:C),
x == y -> y == z -> x == z.

Definition prop_maptype_eqmapped:=
forall (A B:Type) (EQ:A=B) (x:A),
maptype EQ x==x.

Definition prop_maptype_sym:=
forall (A B:Type) (E:A=B) (F:B=A) (x:A) (y:B),
x=maptype F y -> y=maptype E x.

Definition prop_maptype_proof_irrelevance:=
forall (A B:Type) (E F:A=B) (x:A),
maptype E x=maptype F x.

Definition prop_maptype_ind:= forall (A B:Type)
(E:A=B) (EP:(A->Prop)=(B->Prop)) (x:A) (P:A->Prop),
P x<->(maptype EP P)(maptype E x).

Definition prop_maptype_ind_t:= forall (A B:Type)
(E:A=B) (EP:(B->Prop)=(A->Prop)) (x:A) (P:B->Prop),
P (maptype E x)<->(maptype EP P) x.

Definition type_maptype_rect:= forall (A B:Type)
(E:A=B) (EP:(A->Type)=(B->Type)) (x:A) (P:A->Type),
P x->(maptype EP P)(maptype E x).

Definition type_maptype_rect_r:= forall (A B:Type)
(E:A=B) (EP:(A->Type)=(B->Type)) (x:A) (P:A->Type),
(maptype EP P)(maptype E x)->P x.

Definition type_maptype_rect_t:= forall (A B:Type)
(E:A=B) (EP:(B->Type)=(A->Type)) (x:A) (P:B->Type),
P (maptype E x)->(maptype EP P) x.

Definition type_maptype_rect_tr:= forall (A B:Type)
(E:A=B) (EP:(B->Type)=(A->Type)) (x:A) (P:B->Type),
(maptype EP P) x->P (maptype E x).

Definition prop_maptype_rectX:=
(exists RECT:type_maptype_rect, True) /\
(exists RECTR:type_maptype_rect_r, True) /\
(exists RECTT:type_maptype_rect_t, True) /\
(exists RECTTR:type_maptype_rect_tr, True).

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

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

Definition prop_maptype_applicationpt:=
prop_maptype_application /\ prop_maptype_application_t.


Lemma eq_leibnitz: forall (A:Type) (x y:A),
(forall (P:A->Prop), P x<->P y) -> x=y.

Theorem prop_maptype_selfany_to_prop_maptype_returnpi:
prop_maptype_selfany->prop_maptype_returnpi.

Theorem prop_maptype_selfany_to_eqtype_JMeqtype:
forall (A B:Type) (x:A) (y:B) (S:prop_maptype_selfany),
eqtype x y->JMeq x y.
Print Assumptions prop_maptype_selfany_to_eqtype_JMeqtype.

Theorem eqtype_JMeqtype_to_prop_maptype_selfany:
forall (A B:Type) (x:A) (y:B) (S:prop_maptype_selfany),
JMeq x y->eqtype x y.
Print Assumptions prop_maptype_selfany_to_eqtype_JMeqtype.

Theorem prop_maptype_selfany_to_JMeq_eq: forall (A : Type)
(x y : A) (S:prop_maptype_selfany), JMeq x y -> x = y.
Print Assumptions prop_maptype_selfany_to_eqtype_JMeqtype.


Theorem maptype_application_to_ind:
prop_maptype_application -> prop_maptype_ind.

Theorem maptype_application_t_to_ind_t:
prop_maptype_application_t -> prop_maptype_ind_t.

Theorem maptype_application_to_rect:
prop_maptype_application -> type_maptype_rect.

Theorem maptype_application_to_rect_r:
prop_maptype_application -> type_maptype_rect_r.

Theorem maptype_application_t_to_rect_t:
prop_maptype_application_t -> type_maptype_rect_t.

Theorem maptype_application_t_to_rect_tr:
prop_maptype_application_t -> type_maptype_rect_tr.

Theorem maptype_sym_to_sym_eqtype:
prop_maptype_sym -> prop_sym_eqtype.

Theorem mappiandsym_eqtype_to_maptype_sym:
prop_maptype_proof_irrelevance -> prop_sym_eqtype -> prop_maptype_sym.

Theorem maptype_indpt_to_maptype_return:
prop_maptype_ind -> prop_maptype_ind_t -> prop_maptype_return.

Theorem maptype_indpt_to_maptype_returnpi:
prop_maptype_ind -> prop_maptype_ind_t -> prop_maptype_returnpi.

Theorem maptype_rectX_to_maptype_returnpi:
prop_maptype_rectX -> prop_maptype_returnpi.

Theorem piandmaptype_return_to_maptype_sym:
prop_maptype_proof_irrelevance -> prop_maptype_return -> prop_maptype_sym.

Theorem maptype_proof_irrelevance_to_maptype_selfany:
prop_maptype_proof_irrelevance-> prop_maptype_selfany.

Theorem maptype_returnpi_to_maptype_sym:
prop_maptype_returnpi -> prop_maptype_sym.

Theorem maptype_indpt_to_maptype_sym:
prop_maptype_ind -> prop_maptype_ind_t -> prop_maptype_sym.

Theorem maptype_rectX_to_maptype_sym:
prop_maptype_rectX -> prop_maptype_sym.

Theorem maptype_indpt_to_maptype_proof_irrelevance:
prop_maptype_ind -> prop_maptype_ind_t
-> prop_maptype_proof_irrelevance.

Theorem maptype_rectX_to_maptype_proof_irrelevance:
prop_maptype_rectX -> prop_maptype_proof_irrelevance.

Lemma rect_to_ind_g: forall (A:Type)
(R:(A->Type)->Type) (Q:(A->Type)->Type),
(forall (P:A->Type), R P ->Q P)->
(forall (P:A->Prop), R P ->Q P).

Lemma rect_to_ind: forall (A:Type)
(R:(A->Type)->Type),
(forall (P:A->Type), R P ->forall x:A, P x)->
(forall (P:A->Prop), R P ->forall x:A, P x).

Lemma nat_rect_prod: forall P : nat -> Type,
prod (P 0) ((forall n : nat, P n -> P (S n))) -> forall n : nat, P n.

Lemma nat_ind2: forall P : nat -> Prop,
P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n.



Theorem prop_maptype_sym_to_prop_sym_eqtype:
prop_maptype_sym -> prop_sym_eqtype.

Theorem maptype_eqmapped_to_sym_eqtype:
prop_maptype_eqmapped -> prop_sym_eqtype.

Theorem sym_eqtype_to_maptype_eqmapped:
prop_sym_eqtype -> prop_maptype_eqmapped.

Theorem maptype_symandtrans_to_trans_eqtype:
prop_sym_eqtype -> prop_maptype_trans -> prop_trans_eqtype.

Theorem maptype_eqandtrans_to_trans_eqtype:
prop_maptype_eqmapped -> prop_maptype_trans -> prop_trans_eqtype.