include "algebra/CSetoids.ma".
(* UNEXPORTED
-Section unary_function_composition.
+Section unary_function_composition
*)
(*#* ** Composition of Setoid functions
setoid function from [S1] to [S2], and [g] from [S2]
to [S3] in the following definition of composition. *)
-inline "cic:/CoRN/algebra/CSetoidFun/S1.var".
+alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S1.var".
-inline "cic:/CoRN/algebra/CSetoidFun/S2.var".
+alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S2.var".
-inline "cic:/CoRN/algebra/CSetoidFun/S3.var".
+alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S3.var".
-inline "cic:/CoRN/algebra/CSetoidFun/f.var".
+alias id "f" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/f.var".
-inline "cic:/CoRN/algebra/CSetoidFun/g.var".
+alias id "g" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/g.var".
inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con".
(* UNEXPORTED
-End unary_function_composition.
+End unary_function_composition
*)
(* UNEXPORTED
-Section unary_and_binary_function_composition.
+Section unary_and_binary_function_composition
*)
inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con".
inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con".
(* UNEXPORTED
-End unary_and_binary_function_composition.
+End unary_and_binary_function_composition
*)
(*#* ***Projections
*)
(* UNEXPORTED
-Section function_projection.
+Section function_projection
*)
inline "cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con".
inline "cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con".
(* UNEXPORTED
-End function_projection.
+End function_projection
*)
(* UNEXPORTED
-Section BinProj.
+Section BinProj
*)
-inline "cic:/CoRN/algebra/CSetoidFun/S.var".
+alias id "S" = "cic:/CoRN/algebra/CSetoidFun/BinProj/S.var".
inline "cic:/CoRN/algebra/CSetoidFun/binproj1.con".
inline "cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con".
(* UNEXPORTED
-End BinProj.
+End BinProj
*)
(*#* **Combining operations
*)
(* UNEXPORTED
-Section CombiningOperations.
+Section CombiningOperations
*)
-inline "cic:/CoRN/algebra/CSetoidFun/S1.var".
+alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S1.var".
-inline "cic:/CoRN/algebra/CSetoidFun/S2.var".
+alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S2.var".
-inline "cic:/CoRN/algebra/CSetoidFun/S3.var".
+alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S3.var".
(*#*
In the following definition, we assume [f] is a setoid function from
*)
(* UNEXPORTED
-Section CombiningUnaryOperations.
+Section CombiningUnaryOperations
*)
-inline "cic:/CoRN/algebra/CSetoidFun/f.var".
+alias id "f" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/f.var".
-inline "cic:/CoRN/algebra/CSetoidFun/op.var".
+alias id "op" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/op.var".
inline "cic:/CoRN/algebra/CSetoidFun/opOnFun.con".
(* UNEXPORTED
-End CombiningUnaryOperations.
+End CombiningUnaryOperations
*)
(* UNEXPORTED
-End CombiningOperations.
+End CombiningOperations
*)
(*#* **Partial Functions
*)
(* UNEXPORTED
-Section SubSets_of_G.
+Section SubSets_of_G
*)
(*#* ***Subsets of Setoids
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CSetoidFun/S.var".
+alias id "S" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/S.var".
(* UNEXPORTED
-Section Conjunction.
+Section Conjunction
*)
-inline "cic:/CoRN/algebra/CSetoidFun/P.var".
+alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/P.var".
-inline "cic:/CoRN/algebra/CSetoidFun/Q.var".
+alias id "Q" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/Q.var".
inline "cic:/CoRN/algebra/CSetoidFun/conjP.con".
inline "cic:/CoRN/algebra/CSetoidFun/conj_wd.con".
(* UNEXPORTED
-End Conjunction.
+End Conjunction
*)
(* UNEXPORTED
-Section Disjunction.
+Section Disjunction
*)
-inline "cic:/CoRN/algebra/CSetoidFun/P.var".
+alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/P.var".
-inline "cic:/CoRN/algebra/CSetoidFun/Q.var".
+alias id "Q" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/Q.var".
(*#*
Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
inline "cic:/CoRN/algebra/CSetoidFun/disj_wd.con".
(* UNEXPORTED
-End Disjunction.
+End Disjunction
*)
(* UNEXPORTED
-Section Extension.
+Section Extension
*)
(*#*
The next definition is a bit tricky, and is useful for choosing among the elements that satisfy a predicate [P] those that also satisfy [R] in the case where [R] is only defined for elements satisfying [P]---consider [R] to be a condition on the image of an object via a function with domain [P]. We chose to call this operation [extension].
*)
-inline "cic:/CoRN/algebra/CSetoidFun/P.var".
+alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/P.var".
-inline "cic:/CoRN/algebra/CSetoidFun/R.var".
+alias id "R" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/R.var".
inline "cic:/CoRN/algebra/CSetoidFun/extend.con".
inline "cic:/CoRN/algebra/CSetoidFun/extension_wd.con".
(* UNEXPORTED
-End Extension.
+End Extension
*)
(* UNEXPORTED
-End SubSets_of_G.
+End SubSets_of_G
*)
(* NOTATION
*)
(* UNEXPORTED
-Section CSetoid_Ops.
+Section CSetoid_Ops
*)
-inline "cic:/CoRN/algebra/CSetoidFun/S.var".
+alias id "S" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/S.var".
(*#*
To begin with, we want to be able to ``see'' each total function as a partial function.
inline "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con".
(* UNEXPORTED
-Section Part_Function_Const.
+Section Part_Function_Const
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CSetoidFun/c.var".
+alias id "c" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Const/c.var".
inline "cic:/CoRN/algebra/CSetoidFun/Fconst.con".
(* UNEXPORTED
-End Part_Function_Const.
+End Part_Function_Const
*)
(* UNEXPORTED
-Section Part_Function_Id.
+Section Part_Function_Id
*)
inline "cic:/CoRN/algebra/CSetoidFun/Fid.con".
(* UNEXPORTED
-End Part_Function_Id.
+End Part_Function_Id
*)
(*#*
*)
(* UNEXPORTED
-Section Part_Function_Composition.
+Section Part_Function_Composition
*)
-inline "cic:/CoRN/algebra/CSetoidFun/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/G.var".
-inline "cic:/CoRN/algebra/CSetoidFun/F.var".
+alias id "F" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/F.var".
(* begin hide *)
-inline "cic:/CoRN/algebra/CSetoidFun/P.con".
+inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/P.con" "CSetoid_Ops__Part_Function_Composition__".
-inline "cic:/CoRN/algebra/CSetoidFun/Q.con".
+inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/Q.con" "CSetoid_Ops__Part_Function_Composition__".
(* end hide *)
-inline "cic:/CoRN/algebra/CSetoidFun/R.con".
+inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/R.con" "CSetoid_Ops__Part_Function_Composition__".
inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con".
inline "cic:/CoRN/algebra/CSetoidFun/Fcomp.con".
(* UNEXPORTED
-End Part_Function_Composition.
+End Part_Function_Composition
*)
(* UNEXPORTED
-End CSetoid_Ops.
+End CSetoid_Ops
*)
(*#*
*)
(* UNEXPORTED
-Section BinPart_Function_Composition.
+Section BinPart_Function_Composition
*)
-inline "cic:/CoRN/algebra/CSetoidFun/S1.var".
+alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S1.var".
-inline "cic:/CoRN/algebra/CSetoidFun/S2.var".
+alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S2.var".
-inline "cic:/CoRN/algebra/CSetoidFun/S3.var".
+alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S3.var".
-inline "cic:/CoRN/algebra/CSetoidFun/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/G.var".
-inline "cic:/CoRN/algebra/CSetoidFun/F.var".
+alias id "F" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/F.var".
(* begin hide *)
-inline "cic:/CoRN/algebra/CSetoidFun/P.con".
+inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/P.con" "BinPart_Function_Composition__".
-inline "cic:/CoRN/algebra/CSetoidFun/Q.con".
+inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/Q.con" "BinPart_Function_Composition__".
(* end hide *)
-inline "cic:/CoRN/algebra/CSetoidFun/R.con".
+inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/R.con" "BinPart_Function_Composition__".
inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con".
inline "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con".
(* UNEXPORTED
-End BinPart_Function_Composition.
+End BinPart_Function_Composition
*)
(* Different tokens for compatibility with coqdoc *)
*)
(* UNEXPORTED
-Section bijections.
+Section bijections
*)
(*#* **Bijections *)
inline "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con".
(* UNEXPORTED
-End bijections.
+End bijections
*)
(* UNEXPORTED