Library maptypeconstruct

Require Import Classical.
Require Import ClassicalChoice.
Require Import ClassicalEpsilon.

Definition makevar_tactic (U:Type) (A:U):=
 exist (fun x:U=>x=A) A (refl_equal A).
Ltac makevar x:=let U:=type of x in
 destruct(makevar_tactic U x).

Tactic Notation "makevar" constr(x):=let U:=type of x in
 destruct(makevar_tactic U x).

Tactic Notation "makevar" constr(x) "as" ident(y) ident(H):=
let U:=type of x in
 destruct(makevar_tactic U x) as [y H].

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

Definition compose (A B C:Type) (f:B->C) (g:A->B):=
(fun x:A, f (g x)).
Implicit Arguments compose [A B C].
Infix "o" := compose (right associativity, at level 60) : type_scope.

Section maptypehypothesis.
Variable maptype: forall (A:Type) (B:Type) (EQ:A=B) (x:A), B.
Implicit Arguments maptype [A B].
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_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_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.
Definition prop_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.
Definition prop_maptype_hypothesis:=
prop_maptype_application /\
prop_maptype_application_t /\
prop_maptype_trans /\
prop_maptype_dependent_g /\
prop_maptype_fun.
Section maptypetheorems.
Hypothesis maptype_hypothesis: prop_maptype_hypothesis.
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.
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.
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.
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_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_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_selfany: forall (A:Type) (E:A=A) (x:A), maptype E x=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_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_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) 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 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.
End maptypetheorems.
End maptypehypothesis.

Theorem maptype_unique: forall (A B:Type) (E:A=B) (x:A)
(f g:forall (A B:Type) (E:A=B) (x:A), B),
prop_maptype_hypothesis f -> prop_maptype_hypothesis g ->
f A B E x=g A B E x.
Check(f (B -> B) (B -> A) E (f (A -> A) (B -> B) F id) fx).




Definition maptype2:forall (A B : Type) (E:A = B) (x:A),
{y:B|forall (P:forall X:Type, X->Prop), P A x<->P B y}.
Defined.
Eval compute in maptype2.

Definition maptype3: forall (A B : Type) (E:A = B) (x:A), B.
Defined.

Lemma maptype3_prop: forall (A B : Type) (E:A = B) (x:A)
(P:forall X:Type, X->Prop), P A x<->P B (maptype3 A B E x).

Implicit Arguments maptype3 [A B].


Print sig.

Definition constructor_aux: forall (A B:Type) (P:A->B->Prop)
(faux:forall a:A, sig (P a)), A->B.
Defined.

Lemma constructor_aux2: forall (A B:Type) (P:A->B->Prop)
(faux:forall a:A, sig (P a)),
forall a:A, P a (constructor_aux A B P faux a).

Definition constructor: forall (A B:Type) (P:A->B->Prop)
(faux:forall a:A, sig (P a)),
{f:A->B| forall a:A, P a (f a)}.
Defined.

Theorem constructor_choice: forall (A B : Type) (R : A->B->Prop),
    (forall x : A, exists y : B, R x y) ->
    (exists f : A->B, forall x : A, R x (f x)).

Definition dependentconstructor_aux: forall (A B:Type)
(g:A->Type) (P:forall a, g a->Prop)
(faux:forall a:A, sig (P a)),
(forall a:A, g a).
Defined.

Lemma dependentconstructor_aux2: forall (A B:Type)
(g:A->Type) (P:forall a, g a->Prop)
(faux:forall a:A, sig (P a)),
forall a:A, P a (dependentconstructor_aux A B g P faux a).

Definition dependentconstructor: forall (A B:Type)
(g:A->Type) (P:forall a, g a->Prop)
(faux:forall a:A, sig (P a)),
{f:forall a:A, g a| forall a:A, P a (f a)}.
Defined.

Theorem typedependentchoice:
forall (A B:Type) (g:A->Type) (R:forall a, g a -> Prop),
(forall x:A, exists y:g x, R x y)->
(exists f: (forall a:A, g a), forall x:A, R x (f x)).

Definition aa:
{f:forall (U:Type) (u:U), (forall X:Type, X->Prop)|
forall (U:Type) (u:U) (X:Type) (x:X),
(f U u) X x<->(X=U/\ x=u)}.

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

Definition maptype_std_dependent_g (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_std Eg (f x)=f y:=
match Eg in _=w return w with
|refl_equal => (f x)
end.

Definition maptype_std_application
(A B C:Type) (E:A=B)
(F:(A->C)=(B->C)) (f:A->C) (x:A):
maptype_std F f (maptype_std E x) = f x:=
match (E,F) in (prod y z) return z with
|(refl_equal,refl_equal) => refl_equal (A)
end.

Theorem exists_application:
exists maptype:forall A B : Type, A = B -> A -> B,
forall (A B C:Type) (E:A=B)
(F:(A->C)=(B->C)) (f:A->C) (x:A),
maptype (A->C) (B->C) F f (maptype A B E x) = f x.
Print ex_intro.


Inductive ex (A : Type) (P : A -> Prop) : Prop :=
    ex_intro : forall x : A, P x -> ex P
For ex: Argument A is implicit
For ex_intro: Argument A is implicit

choice =
fun (A B : Type) (R : A -> B -> Prop) (H : forall x : A, exists y : B, R x y) =>
ex_intro (fun f : A -> B => forall x : A, R x (f x))
  (fun x : A => proj1_sig (constructive_indefinite_description (R x) (H x)))
  (fun x : A => proj2_sig (constructive_indefinite_description (R x) (H x)))
     : forall (A B : Type) (R : A -> B -> Prop),
       (forall x : A, exists y : B, R x y) ->
       exists f : A -> B, forall x : A, R x (f x)



Theorem choice :
  forall (A B : Type) (R : A->B->Prop),
    (forall x : A, exists y : B, R x y) ->
    (exists f : A->B, forall x : A, R x (f x)).

Definition maptypeaux:
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:(forall A B : Type, A = B -> A -> B) |
maptype (g x) (g y) Eg (f x)=f y}.


Inductive mappedof (A B:Type) (E:A=B) (x:A) (y:B): Prop:=
|mappedof_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.

Theorem identitytype_existence:
exists f:(forall (A B:Type), A->B), identitytype f.
Definition identitytypeE_ind
 (f:forall (A B:Type) (E:A=B), A->B):=
forall (A B:Type) (E:A=B) (F:(A->Prop)=(B->Prop))
(x:A) (P:A->Prop),
(P x<->(f (A->Prop) (B->Prop) F P)(f A B E x)).

Lemma identitytype_identity: forall (A:Type)
(f:forall (A B:Type), A->B) (x:A),
identitytype f -> f A A x=x.

Definition maptypeaux
(A:Type) (B:Type) (EQ:A=B) (x:A):
{y:B |
forall (f:forall (A B:Type), A->B),
identitytype f -> f A B x=y
}.
Defined.
Print maptypeaux.

Definition maptype (A:Type) (B:Type) (EQ:A=B) (x:A):B.
Defined.
Eval compute in maptype.
Print maptype.

Theorem maptype_id: forall (A B:Type) (EQ:A=B) (x:A) (y:B),
maptype A B EQ x=y ->
forall (f:forall (A B:Type), A->B),
identitytype f -> f A B x=y.

Theorem maptype_identity: identitytypeE_ind maptype.