Library JMeqmaptype

Require Export JMeq.
Require Export types_base.

Notation "x == y :> A B":= (@JMeq A x B y) (at level 70, y at next level, no associativity).
Notation "x == y" := (@JMeq _ x _ y) (at level 70, no associativity).

Lemma eq_JMeq: forall (A:Type) (x y:A), x=y -> x==y.

Theorem JMex: forall (A B:Type) (E:A=B) (x:A),
{y:B|x == y}.
Tactic Notation "JMex" constr(x) constr(E) "as" ident(y) ident(H):=
 destruct (JMex _ _ E x) as [y H].

Tactic Notation "JMex" constr(x) constr(E):=
 let a:=fresh x "'" with b:=fresh x "H" in
 destruct (JMex _ _ E x) as [a b].

Definition maptype: forall (A B:Type) (E:A=B) (x:A), B.
Defined.
Implicit Arguments maptype [A B].

Lemma maptype_JMeq: forall (A B:Type) (E:A=B) (x:A),
x==(maptype E x).

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

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

Theorem JMeq_maptype_eq: forall (A B:Type) (x:A) (y:B),
x==y-> {E:A=B|y=maptype E x}.
Implicit Arguments JMeq_maptype_eq [A B x y].
Ltac JMdestruct hyp:=
let a:=fresh hyp "eq" with b:=fresh hyp "map"
in destruct (JMeq_maptype_eq hyp) as [a b].

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

Theorem maptype_selfany: forall (A:Type) (E:A=A) (x:A), maptype E x=x.

Theorem f_JMequal: forall (A B C:Type)
(E:B=C) (f:A->B) (g:A->C) (x:A),
f==g -> (f x)==(g x).

Theorem f2_JMequal: forall (A B C:Type)
(E:A=B) (f:A->C) (g:B->C) (x:A) (y:B),
f==g -> x==y -> (f x)=(g y).

Theorem f3_JMequal: forall (A B C D:Type)
(AB:A=B) (CD:C=D) (f:A->C) (g:B->D) (x:A) (y:B),
JMeq f g -> JMeq x y -> JMeq (f x) (g y).
Print Assumptions f3_JMequal.

Theorem 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.
Print Assumptions maptype_application.

Theorem 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.
Print Assumptions maptype_application_t.

Theorem maptype_returnpi: forall (A B:Type) (E:A=B) (F:B=A) (x:A),
maptype F (maptype E x)=x.

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

Theorem maptype_proof_irrelevance: forall (A B:Type) (E F:A=B) (x:A),
maptype E x=maptype F x.
Definition maptype_pi:=maptype_proof_irrelevance.

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

Theorem 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.
Print Assumptions maptype_trans.

Theorem JMeq_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),
f x==f 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_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.
Print Assumptions maptype_fun.

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_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 maptype_square2: forall (A B C D:Type) (AB:A=B) (CD:C=D)
(ACBD:(A->C)=(B->D)) (f:A->C) (x:A),
(maptype ACBD f) (maptype AB x)=(maptype CD (f x)).

Theorem maptype_preserveidentity: forall (A B:Type) (E:A=B)
(F:(A->A)=(B->B)) (x:B), (maptype F (@id A)) x=id x.

Theorem maptype_combine_l: forall (A B C D:Type)
(AB:A=B) (CD:C=D) (ACBC:(A->C)=(B->C))
(BCBD:(B->C)=(B->D)) (ACBD:(A->C)=(B->D)) (f:A->C),
(maptype BCBD (maptype ACBC f))= (maptype ACBD f).

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

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

Theorem maptype_compose: forall (A B C D E:Type)
(AD:A=D) (CE:C=E)
(ACDE:(A->C)=(D->E)) (BCBE:(B->C)=(B->E)) (ABDB:(A->B)=(D->B))
(f:B->C) (g:A->B) (x:D),
(maptype ACDE (compose f g)) x=
(compose (maptype BCBE f) (maptype ABDB g)) x.

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_binary: forall (A B C D E F:Type) (AB:A=B) (CD:C=D)
(EF:E=F) (ACEBDF:(A->C->E)=(B->D->F)) (f:A->C->E) (x:A) (y:C),
(maptype ACEBDF f) (maptype AB x) (maptype CD y)=
maptype EF (f x y).

Theorem f3_JMequal2: forall (A1 A2 B1 B2 C D:Type)
(AB1:A1=B1) (AB2:A2=B2) (CD:C=D) (f:A1->A2->C)
(g:B1->B2->D) (x1:A1) (y1:B1) (x2:A2) (y2:B2),
f==g -> x1==y1 -> x2==y2 -> f x1 x2== g y1 y2.

Theorem f3_JMequal3: forall (A1 A2 A3 B1 B2 B3 C D:Type)
(AB1:A1=B1) (AB2:A2=B2) (AB3:A3=B3) (CD:C=D)
(f:A1->A2->A3->C) (g:B1->B2->B3->D)
(x1:A1) (y1:B1) (x2:A2) (y2:B2) (x3:A3) (y3:B3),
f==g -> x1==y1 -> x2==y2 -> x3==y3 -> f x1 x2 x3== g y1 y2 y3.

Theorem f3_JMequal4: forall (A1 A2 A3 A4 B1 B2 B3 B4 C D:Type)
(AB1:A1=B1) (AB2:A2=B2) (AB3:A3=B3) (AB4:A4=B4) (CD:C=D)
(f:A1->A2->A3->A4->C) (g:B1->B2->B3->B4->D)
(x1:A1) (y1:B1) (x2:A2) (y2:B2) (x3:A3) (y3:B3) (x4:A4) (y4:B4),
f==g -> x1==y1 -> x2==y2 -> x3==y3 -> x4==y4 ->
f x1 x2 x3 x4== g y1 y2 y3 y4.

Lemma JMfunctional3_extensionality: forall (A B C D:Type) (AB:A=B)
(CD:C=D) (f : A -> C) (g:B->D)
(EXT: forall (A B:Type) (f g:A->B),(forall x,f x=g x)->f=g),
(forall x y,x==y-> f x == g y) -> f == g.

Lemma JMfunctional_extensionality: forall (A B C:Type) (E:B=C)
(f : A -> B) (g:A->C)
(EXT: forall (A B:Type) (f g:A->B),(forall x,f x=g x)->f=g),
(forall x, f x == g x) -> f == g.

Lemma JMfunctional2_extensionality: forall (A B C:Type) (E:A=B)
(f : A -> C) (g:B->C)
(EXT: forall (A B:Type) (f g:A->B),(forall x,f x=g x)->f=g),
(forall x y,x==y-> f x = g y) -> f == g.

Lemma JMfunctional3_extensionality_dep:
forall (A B:Type) (C:A->Type) (D:B->Type) (AB:A=B) (CD:C==D)
(f : forall x:A, C x)
(g : forall x:B, D x)
(EXTD: forall (A:Type) (B:A->Type) (f g:forall x:A, B x),
 (forall x,f x=g x)->f=g),
(forall x y, x==y-> f x == g y) -> f == g.

Lemma f_JMequal_dependent_base: forall (A B C:Type) (E:A=B)
(f:forall X:Type,X->C), f A==f B.

Theorem f_JMequal_dependent: forall (A B C:Type) (E:A=B)
(f:forall X:Type,X->C) (x:A) (y:B),
x==y-> f A x=f B y.

Corollary f_JMequal_dependent_Prop: forall (A B:Type) (E:A=B)
(P:forall X:Type,X->Prop) (x:A) (y:B),
x==y-> P A x->P B y.

Theorem f_JMequal_dependent_g: forall (A B:Type) (g:A->Type)
(f:forall t:A, g t->B) (tx ty:A) (E:tx=ty) (x:g tx) (y:g ty),
x==y->f tx x=f ty y.

Theorem f_JMequal_dependent_g_Prop: forall (A:Type) (g:A->Type)
(P:forall t:A, g t->Prop) (tx ty:A) (E:tx=ty) (x:g tx) (y:g ty),
x==y->P tx x->P ty y.


Theorem f2_JMequal_s: forall (A B C:Type)
(f:A->C) (g:B->C) (x:A) (y:B),
f==g -> x==y -> (f x)=(g y).

Theorem f_JMequal_dependent_gs: forall (A B:Type) (g:A->Type)
(f:forall t:A, g t->B) (tx ty:A)
(Ef:f tx==f ty) (Eg:g tx=g ty)
(x:g tx) (y:g ty),
x==y->f tx x=f ty y.


Section Examples.
Variable t:nat->Type.
Variable app:forall (m n:nat), t m->t n->t (m+n).
Implicit Arguments app [m n].
Infix "++" := app (right associativity, at level 60).
Variable m n p q:nat.
Variable x:t m.
Variable y:t n.
Variable u:t p.
Variable v:t q.
Hypothesis Emn:m=n.
Hypothesis Exy:x==y.

Let ej1: x++u==v -> y++u==v.

End Examples.

Opaque maptype.