Require Export Relations.

Set Implicit Arguments.
Unset Strict Implicit.



Structure > Setoid'' : Type :=
  {Carrier'' :> Type;
   Equal'' : Relation Carrier'';
   Prf_equiv'' :> Equivalence Equal''}.

Infix "=_S''" := Equal'' (at level 70).


Lemma Refl'' : ∀ (S : Setoid'') (x : S), x =_S'' x.
Proof.
intro S; exact (Prf_refl S).
Qed.

Lemma Sym'' : ∀ (S : Setoid'') (x y : S), x =_S'' y → y =_S'' x.
Proof.
intro S; exact (Prf_sym S).
Qed.

Lemma Trans'' :
 ∀ (S : Setoid'') (x y z : S), x =_S'' y → y =_S'' z → x =_S'' z.
Proof.
intro S; exact (Prf_trans S).
Qed.



Section maps''.

Variable A B : Setoid''.

Definition Map_law'' (f : A → B) :=
  ∀ x y : A, x =_S'' y → f x =_S'' f y.

Structure > Map'' : Type := {Ap'' :> A → B; Pres'' :> Map_law'' Ap''}.


Lemma Pres1'' : ∀ (m : Map'') (x y : A), x =_S'' y → m x =_S'' m y.
Proof.
exact Pres''.
Qed.


Definition Ext'' (f g : Map'') := ∀ x : A, f x =_S'' g x.

Lemma Ext_equiv'' : Equivalence Ext''.
Proof.
intros; apply Build_Equivalence.
unfold Reflexive in |- *; unfold Ext'' in |- *; intros f x.
apply Refl''.
apply Build_Partial_equivalence.
unfold Transitive in |- *; unfold Ext'' in |- *; intros f g h e1 e2 x.
apply Trans'' with (g x).
apply (e1 x).
apply (e2 x).
unfold Symmetric in |- *; unfold Ext'' in |- *; intros f g e x.
apply Sym''; trivial.
Qed.

Canonical Structure Map_setoid'' : Setoid'' := Ext_equiv''.

End maps''.


Section fun2_to_map2''.

Variable A B C : Setoid''.

Definition Map2'' := Map'' A (Map_setoid'' B C).

Variable f : A → B → C.

Definition Map2_congl_law'' :=
  ∀ (b1 b2 : B) (a : A), b1 =_S'' b2 → f a b1 =_S'' f a b2.

Definition Map2_congr_law'' :=
  ∀ (a1 a2 : A) (b : B), a1 =_S'' a2 → f a1 b =_S'' f a2 b.

Definition Map2_cong_law'' :=
  ∀ (a1 a2 : A) (b1 b2 : B),
  a1 =_S'' a2 → b1 =_S'' b2 → f a1 b1 =_S'' f a2 b2.

Hypothesis pgcl : Map2_congl_law''.
Hypothesis pgcr : Map2_congr_law''.

Lemma Map2_map_law1'' : ∀ a : A, Map_law'' (f a).
Proof.
intro a; unfold Map_law'' in |- ×.
intros b1 b2 H; apply (pgcl a H).
Qed.

Canonical Structure Map2_map1'' (a : A) := Build_Map'' (Map2_map_law1'' a).

Lemma Map2_map_law2'' : Map_law'' Map2_map1''.
Proof.
unfold Map_law'', Map2_map1'' in |- ×.
intros a1 a2 H; simpl in |- *; unfold Ext'' in |- *; intro b; simpl in |- ×.
apply pgcr; trivial.
Qed.

Definition Build_Map2'' : Map2'' := Build_Map'' Map2_map_law2''.

End fun2_to_map2''.

Section prop_map2''.

Variables (A B C : Setoid'') (f : Map2'' A B C).

Definition Ap2'' (a : A) (b : B) := f a b.

Lemma Prf_map2_congl'' : Map2_congl_law'' Ap2''.
Proof.
unfold Map2_congl_law'' in |- *; intros b1 b2 a H.
unfold Ap2'' in |- *; apply (Pres1'' (f a)); trivial.
Qed.

Lemma Prf_map2_congr'' : Map2_congr_law'' Ap2''.
Proof.
unfold Map2_congr_law'' in |- *; intros a1 a2 b H.
apply (Pres1'' f H b).
Qed.

Lemma Prf_map2_cong'' : Map2_cong_law'' Ap2''.
Proof.
unfold Map2_cong_law'' in |- *; intros a1 a2 b1 b2 H1 H2.
apply Trans'' with (Ap2'' a2 b1).
apply (Prf_map2_congr'' b1 H1).
apply (Prf_map2_congl'' a2 H2).
Qed.

End prop_map2''.

Coercion Ap2'' : Map2'' >-> Funclass.

Identity Coercion Map2''_Map'' : Map2'' >-> Map''.