+(*Section Part_Function_Const.*)
+
+(*
+In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
+
+%\begin{convention}% Let [c:S].
+%\end{convention}%
+*)
+
+(*Variable c : S.*)
+
+definition Fconst: \forall S:CSetoid. \forall c: S. ? \def
+ \lambda S:CSetoid. \lambda c: S.
+ total_eq_part ? (Const_CSetoid_fun ? ? c).
+
+(* End Part_Function_Const. *)
+
+(* Section Part_Function_Id. *)
+
+definition Fid : \forall S:CSetoid. ? \def
+ \lambda S:CSetoid.total_eq_part ? (id_un_op S).
+
+(* End Part_Function_Id. *)
+
+(*
+(These happen to be always total functions, but that is more or less obvious,
+as we have no information on the setoid; however, we will be able to define
+partial functions just applying other operators to these ones.)
+
+If we have two setoid functions [F] and [G] we can always compose them.
+The domain of our new function will be the set of points [s] in the domain of [F]
+for which [F(s)] is in the domain of [G]#.
+
+#%\footnote{%Notice that the use of extension here is essential.%}.%
+The inversion in the order of the variables is done to maintain uniformity
+with the usual mathematical notation.
+
+%\begin{convention}%
+Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing
+their domains.
+%\end{convention}%
+*)
+
+(* Section Part_Function_Composition. *)
+
+(* Variables G F : PartFunct S. *)
+
+(* begin hide *)
+
+definition UP : \forall S:CSetoid. \forall F: PartFunct S. ? \def
+ \lambda S:CSetoid. \lambda F: PartFunct S.
+ pfdom ? F.
+(* Let P := Dom F. *)
+definition UQ : \forall S:CSetoid. \forall G : PartFunct S. ? \def
+ \lambda S:CSetoid. \lambda G: PartFunct S.
+ pfdom ? G.
+(* Let Q := Dom G. *)
+definition UR : \forall S:CSetoid. \forall F,G: PartFunct S. \forall x: S. ? \def
+ \lambda S:CSetoid. \lambda F,G: PartFunct S. \lambda x: S.
+ (sigT ? (\lambda Hx : UP S F x. UQ S G (pfpfun S F x Hx))).
+(*Let R x := {Hx : P x | Q (F x Hx)}.*)
+
+(* end hide *)
+
+(* TODO ProjT1 *)
+lemma part_function_comp_strext : \forall S:CSetoid. \forall F,G: PartFunct S.
+\forall x,y:S. \forall Hx : UR S F G x. \forall Hy : (UR S F G y).
+ (pfpfun ? G (pfpfun ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx))
+ \neq (pfpfun ? G (pfpfun ? F y (proj1_sigT ? ? Hy)) (proj2_sigTm ? ? Hy)) \to x \neq y.
+intros (S F G x y Hx Hy H).
+exact (pfstrx ? ? ? ? ? ? (pfstrx ? ? ? ? ? ? H)).
+qed.
+(*
+definition TempR : \forall S:CSetoid. \forall F,G: PartFunct S. \forall x: S. ? \def
+ \lambda S:CSetoid. \lambda F,G: PartFunct S. \lambda x: S.
+ (ex ? (\lambda Hx : UP S F x. UQ S G (pfpfun S F x Hx))). *)
+
+lemma part_function_comp_dom_wd :\forall S:CSetoid. \forall F,G: PartFunct S.
+ pred_wd S (UR S F G).
+ intros.unfold.
+ intros (x y H H0).
+ unfold UR.
+ elim H.
+ unfold in a.
+ unfold UP.unfold UQ.
+ apply (existT).
+ apply (dom_wd S F x y a H0).
+apply (dom_wd S G (pfpfun S F x a)).
+assumption.
+apply pfwdef; assumption.
+qed.
+
+definition Fcomp : \forall S:CSetoid. \forall F,G : PartFunct S. ? \def
+\lambda S:CSetoid. \lambda F,G : PartFunct S.
+mk_PartFunct ? (UR S F G) (part_function_comp_dom_wd S F G)
+(\lambda x. \lambda Hx : UR S F G x. (pfpfun S G (pfpfun S F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)))
+(part_function_comp_strext S F G).
+
+(*End Part_Function_Composition.*)
+
+(*End CSetoid_Ops.*)
+
+(*
+%\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
+%\end{convention}%
+*)
+
+(* Section BinPart_Function_Composition.*)
+
+(*Variables S1 S2 S3 : CSetoid.
+
+Variable G : BinPartFunct S2 S3.
+Variable F : BinPartFunct S1 S2.
+*)
+(* begin hide *)
+(* Let P := BDom F.
+Let Q := BDom G.*)
+(* end hide *)
+(*Let R x := {Hx : P x | Q (F x Hx)}.*)
+
+definition BP : \forall S1,S2:CSetoid. \forall F: BinPartFunct S1 S2. ? \def
+ \lambda S1,S2:CSetoid. \lambda F: BinPartFunct S1 S2.
+ bpfdom ? ? F.
+(* Let P := Dom F. *)
+definition BQ : \forall S2,S3:CSetoid. \forall G: BinPartFunct S2 S3. ? \def
+ \lambda S2,S3:CSetoid. \lambda G: BinPartFunct S2 S3.
+ bpfdom ? ? G.
+(* Let Q := BDom G.*)
+definition BR : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2.
+\forall G: BinPartFunct S2 S3.
+ \forall x: ?. ? \def
+ \lambda S1,S2,S3:CSetoid. \lambda F: BinPartFunct S1 S2.
+ \lambda G: BinPartFunct S2 S3. \lambda x: ?.
+ (sigT ? (\lambda Hx : BP S1 S2 F x. BQ S2 S3 G (bpfpfun S1 S2 F x Hx))).
+(*Let R x := {Hx : P x | Q (F x Hx)}.*)
+
+lemma bin_part_function_comp_strext : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2.
+\forall G: BinPartFunct S2 S3. \forall x,y. \forall Hx : BR S1 S2 S3 F G x.
+\forall Hy : (BR S1 S2 S3 F G y).
+(bpfpfun ? ? G (bpfpfun ? ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)) \neq
+(bpfpfun ? ? G (bpfpfun ? ? F y (proj1_sigT ? ? Hy)) (proj2_sigTm ? ? Hy)) \to x \neq y.
+intros (S1 S2 S3 x y Hx Hy H).
+exact (bpfstrx ? ? ? ? ? ? ? (bpfstrx ? ? ? ? ? ? ? H1)).
+qed.
+
+lemma bin_part_function_comp_dom_wd : \forall S1,S2,S3:CSetoid.
+ \forall F: BinPartFunct S1 S2. \forall G: BinPartFunct S2 S3.
+ pred_wd ? (BR S1 S2 S3 F G).
+intros.
+unfold.intros (x y H H0).
+unfold BR; elim H 0.intros (x0).
+apply (existT ? ? (bdom_wd ? ? F x y x0 H0)).
+apply (bdom_wd ? ? G (bpfpfun ? ? F x x0)).
+assumption.
+apply bpfwdef; assumption.
+qed.
+
+definition BinFcomp : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2.
+ \forall G: BinPartFunct S2 S3. ?
+\def
+\lambda S1,S2,S3:CSetoid. \lambda F: BinPartFunct S1 S2. \lambda G: BinPartFunct S2 S3.
+mk_BinPartFunct ? ? (BR S1 S2 S3 F G) (bin_part_function_comp_dom_wd S1 S2 S3 F G)
+ (\lambda x. \lambda Hx : BR S1 S2 S3 F G x.(bpfpfun ? ? G (bpfpfun ? ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)))
+ (bin_part_function_comp_strext S1 S2 S3 F G).
+(*End BinPart_Function_Composition.*)
+(* Different tokens for compatibility with coqdoc *)
+
+(*
+Implicit Arguments Fconst [S].
+Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
+
+Notation FId := (Fid _).
+
+Implicit Arguments Fcomp [S].
+Infix "[o]" := Fcomp (at level 65, no associativity).
+
+Hint Resolve pfwdef bpfwdef: algebra.
+*)
+(*Section bijections.*)
+(*Bijections *)
+
+
+definition injective : \forall A, B :CSetoid. \forall f : CSetoid_fun A B.
+ ? \def
+ \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B.
+ (\forall a0: A.\forall a1 : A. a0 \neq a1 \to
+ (csf_fun A B f a0) \neq (csf_fun A B f a1)).
+
+definition injective_weak: \forall A, B :CSetoid. \forall f : CSetoid_fun A B.
+ ? \def
+ \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B.
+ (\forall a0, a1 : A.
+ (csf_fun ? ? f a0) = (csf_fun ? ? f a1) -> a0 = a1).
+
+definition surjective : \forall A, B :CSetoid. \forall f : CSetoid_fun A B.
+ ? \def
+ \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B.
+ (\forall b : B. (\exists a : A. (csf_fun ? ? f a) = b)).
+
+(* Implicit Arguments injective [A B].
+ Implicit Arguments injective_weak [A B].
+ Implicit Arguments surjective [A B]. *)
+
+lemma injective_imp_injective_weak: \forall A, B :CSetoid. \forall f : CSetoid_fun A B.
+ injective A B f \to injective_weak A B f.
+intros 3 (A B f).
+unfold injective.
+intro H.
+unfold injective_weak.
+intros 3 (a0 a1 H0).
+apply not_ap_imp_eq.
+unfold.
+intro H1.
+letin H2 \def (H a0 a1 H1).
+letin H3 \def (ap_imp_neq B (csf_fun ? ? f a0) (csf_fun ? ? f a1) H2).
+letin H4 \def (eq_imp_not_neq B (csf_fun ? ? f a0) (csf_fun ? ? f a1) H0).
+apply H4.
+exact H3.
+qed.
+
+definition bijective : \forall A, B :CSetoid. \forall f : CSetoid_fun A B.
+? \def \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B.
+injective A B f \and surjective A B f.
+
+
+(* Implicit Arguments bijective [A B]. *)
+
+lemma id_is_bij : \forall A:CSetoid. bijective ? ? (id_un_op A).
+intro A.
+split [unfold. simplify; intros. exact H|
+unfold.intro. apply (ex_intro ).exact b. apply eq_reflexive]
+qed.
+
+lemma comp_resp_bij :\forall A,B,C,f,g.
+ bijective ? ? f \to bijective ? ? g \to bijective ? ? (compose_CSetoid_fun A B C f g).
+intros 5 (A B C f g).
+intros 2 (H0 H1).
+elim H0 0; clear H0;intros 2 (H00 H01).
+elim H1 0; clear H1; intros 2 (H10 H11).
+split[unfold. intros 2 (a0 a1); simplify; intro.
+unfold compose_CSetoid_fun.simplify.
+ apply H10; apply H00;exact H|unfold.
+ intro c; unfold compose_CSetoid_fun.simplify.
+elim (H11 c) 0;intros (b H20).
+elim (H01 b) 0.intros (a H30).
+apply ex_intro.apply a.
+apply (eq_transitive_unfolded ? ? (csf_fun B C g b)).
+apply csf_wd_unfolded.assumption.assumption]
+qed.
+
+(* Implicit Arguments invfun [A B]. *)
+
+record CSetoid_bijective_fun (A,B:CSetoid): Type \def
+{ direct :2> CSetoid_fun A B;
+ inverse: CSetoid_fun B A;
+ inv1: \forall x:A.(csf_fun ? ? inverse (csf_fun ? ? direct x)) = x;
+ inv2: \forall x:B.(csf_fun ? ? direct (csf_fun ? ? inverse x)) = x
+ }.
+
+lemma invfun : \forall A,B:CSetoid. \forall f:CSetoid_bijective_fun A B.
+ B \to A.
+ intros (A B f ).
+ elim (inverse A B f).apply f1.apply c.
+qed.
+
+lemma inv_strext : \forall A,B. \forall f : CSetoid_bijective_fun A B.
+ fun_strext B A (invfun A B f).
+intros.unfold invfun.
+elim (inverse A B f).simplify.intros.
+unfold in H.apply H.assumption.
+qed.
+
+
+
+definition Inv: \forall A, B:CSetoid.
+\forall f:CSetoid_bijective_fun A B. \forall H : (bijective ? ? (direct ? ? f)). ? \def
+\lambda A, B:CSetoid. \lambda f:CSetoid_bijective_fun A B. \lambda H : (bijective ? ? (direct ? ? f)).
+ mk_CSetoid_fun B A (invfun ? ? f) (inv_strext ? ? f).
+
+lemma eq_to_ap_to_ap: \forall A:CSetoid.\forall a,b,c:A.
+a = b \to b \neq c \to a \neq c.
+intros.
+generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
+intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).
+auto.assumption.
+qed.
+
+lemma Dir_bij : \forall A, B:CSetoid.
+ \forall f : CSetoid_bijective_fun A B.
+ bijective ? ? (direct ? ? f).
+ intros.unfold bijective.split
+ [unfold injective.intros.
+ apply (csf_strext_unfolded ? ? (inverse ? ? f)).
+ elim f.
+ apply (eq_to_ap_to_ap ? ? ? ? (H1 ?)).
+ apply ap_symmetric_unfolded.
+ apply (eq_to_ap_to_ap ? ? ? ? (H1 ?)).
+ apply ap_symmetric_unfolded.assumption
+ |unfold surjective.intros.
+ elim f.auto.
+ ]
+qed.
+
+lemma Inv_bij : \forall A, B:CSetoid.
+ \forall f : CSetoid_bijective_fun A B.
+ bijective ? ? (inverse A B f).
+ intros;
+ elim f 2;
+ elim c2 0;
+ elim c3 0;
+ simplify;
+ intros;
+ split;
+ [ intros;
+ apply H1;
+ apply (eq_to_ap_to_ap ? ? ? ? (H3 ?)).
+ apply ap_symmetric_unfolded.
+ apply (eq_to_ap_to_ap ? ? ? ? (H3 ?)).
+ apply ap_symmetric_unfolded.assumption|
+ intros.auto]
+qed.
+
+(* End bijections.*)
+
+(* Implicit Arguments bijective [A B].
+Implicit Arguments injective [A B].
+Implicit Arguments injective_weak [A B].
+Implicit Arguments surjective [A B].
+Implicit Arguments inv [A B].
+Implicit Arguments invfun [A B].
+Implicit Arguments Inv [A B].
+
+Implicit Arguments conj_wd [S P Q].
+*)