Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Major Update

  • Loading branch information...
commit 9029b1ba71c99ac8d226cee37576287f882d8a45 1 parent 2925999
@vladimirias authored
View
98 Coq_patches/README
@@ -1,10 +1,6 @@
-This directory contains two patches for Coq-8.3pl2 written by Hugo Hereblin which are needed for proper compilation of the "Foundations" library. They are intended only as a temporary solution for the universe management issues in Coq which arise in connection with the univalent approach.
+This directory contains patches for Coq-8.3pl2 written by Hugo Hereblin and Dan Grayson which are needed for proper compilation of the "Foundations" library.
-The patches are to be applied in the home directory of Coq (before "make world") with the commands
-
-patch -p1 < inductive-indice-levels-matter-8.3.patch
-
-patch -p3 < patch.type-in-type
+Hugo's patches "inductive-indice-levels-matter-8.3.patch" and "patch.type-in-type" are intended only as a temporary solution for the universe management issues in Coq which arise in connection with the univalent approach.
The first of these patches changes the way the universe level of inductive types is computed for those definitions which do not specify [ Set ] or [ Prop ] as the target of the inductive construction explicitely. The new computation rule for the universe level takes into account not only the u-levels of the types occuring in the constructors but also the u-levels of types occuring in "pseudo-parametrs" i.e. in the [ forall ] expressions in the type of the inductive definition. For example, in the definition:
@@ -12,4 +8,92 @@ The first of these patches changes the way the universe level of inductive types
The u-level of [ Ind ] will be the maximum of the u-level computed on the basis of types occuring in the constructors and the u-level of [ A2 ]. The u-level of [ A1 ] which the type of a parameter [ a1 ] ( as opposed to a pseudo-parameter [ a2 ] ) is not taken into account.
-The second patch switches off the universe consistency checking in Coq which is a temporary measure which allows us to formalize interesting constructions such as [ ishinh ] and [ setquot ] without having the resizing rules.
+The second patch switches off the universe consistency checking in Coq which is a temporary measure which allows us to formalize interesting constructions such as [ ishinh ] and [ setquot ] without having the resizing rules.
+
+Dan's patches have the following functions (see also comments in the individual patches):
+
+1. "grayson-closedir-after-opendir.patch" imporoves the management of file openings/closing and eliminates in most cases the complaint that there arev too many open files.
+
+2. "grayson-fix-infinite-loop.patch" this is a temporary fix for a bug in the current version of Coq's "call by need" normnalization algorithm. The patch uses a flag previously installed in the source code to switch off some optimization features of the algorthim. The need for this patch has arised because of several cases when Coq process would hang after "Admitted". In practice the patch prevents hangings but makes compilation of some of the code slower. In particular, with this patch installed the current standard library file Cycllic31.v does not compile in a reasonable amount of time (see the suggestion of how to compile Coq without much of the standard library below). It also affect the time of compilation for some of the "computation tests" in the Foundations library increasing the compilation time by a factor of >5. Hopefully, the actuall buf will be located and removed in the next update.
+
+3. "grayson-improved-abstraction-version2-8.3pl2.patch" this patch dramatically improves the behavior of the [destruct] tactic making it applicable in many the cases when dependencies are present. It is not creating any complicated proof terms but simply uses the eliminator for inductive definitions in a more intelligent way than the standard [ destruct ] .
+
+
+4. "grayson-fix-infinite-loop.patch" fixes another hanging situation.
+
+The following is a copy of the terminal session on my mac with the application of the patches which shows in particular the "-p" levels which have to be used in each case. It also shows how one can compile all of the Coq which is needed for the Foundations library without compiling most of the Standard Library (it takes about 5 min instead of 20 min on my computer to do it the way suggested here):
+
+
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ ./configure --prefix /opt/local
+You have GNU Make >= 3.81. Good!
+You have Objective-Caml 3.11.2. Good!
+LablGtk2 not found: CoqIde will not be available.
+pngtopnm was not found; documentation will not be available
+
+ Coq top directory : /Applications/coq-8.3pl2_two_patches_and_Dan_3
+ Architecture : i386
+ Coq VM bytecode link flags : -custom
+ Coq tools bytecode link flags : -custom
+ OS dependent libraries : -cclib -lunix
+ Objective-Caml/Camlp4 version : 3.11.2
+ Objective-Caml/Camlp4 binaries in : /opt/local/bin
+ Objective-Caml library in : /opt/local/lib/ocaml
+ Camlp4 library in : +camlp5
+ Native dynamic link support : true
+ Documentation : None
+ CoqIde : no
+ Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
+ Coq web site : http://coq.inria.fr/
+
+ Paths for true installation:
+ binaries will be copied in /opt/local/bin
+ library will be copied in /opt/local/lib/coq
+ man pages will be copied in /opt/local/man
+ documentation will be copied in /opt/local/share/doc/coq
+ emacs mode will be copied in /opt/local/share/emacs/site-lisp
+
+If anything in the above is wrong, please restart './configure'.
+
+*Warning* To compile the system for a new architecture
+ don't forget to do a 'make archclean' before './configure'.
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p1 < inductive-indice-levels-matter-8.3.patch
+patching file kernel/indtypes.ml
+patching file kernel/inductive.ml
+patching file kernel/inductive.mli
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p3 < patch.type-in-type
+patching file kernel/reduction.ml
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p0 < fix-hanging-at-end-of-proof.patch
+patching file kernel/closure.ml
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p0 < grayson-fix-infinite-loop.patch
+patching file ./tactics/tactics.ml
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p0 < grayson-improved-abstraction-version2-8.3pl2.patch
+patching file ./configure
+patching file ./pretyping/evd.ml
+patching file ./pretyping/evd.mli
+patching file ./pretyping/pretype_errors.ml
+patching file ./pretyping/pretype_errors.mli
+patching file ./pretyping/unification.ml
+patching file ./pretyping/unification.mli
+patching file ./proofs/logic.ml
+patching file ./tactics/tactics.ml
+patching file ./test-suite/success/unification.v
+patching file ./test-suite/success/unification2.v
+patching file ./toplevel/himsg.ml
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ patch -p0 < grayson-closedir-after-opendir.patch
+patching file ./lib/system.ml
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ sudo make GOTO_STAGE=2 coqbinaries states
+....
+fuld-220:coq-8.3pl2_two_patches_and_Dan_3 vladimir$ sudo make install .
+
+
+(Note : install may give error messages because some of the files it wants to move are not created by this version of the compilation process. Just ignore it. )
+
+
+
+
+
+
+
+
+
View
12 Coq_patches/fix-hanging-at-end-of-proof.patch
@@ -0,0 +1,12 @@
+diff -ub coq-8.3pl2-clean/kernel/closure.ml coq-8.3pl2-no-universe-constraints--index-levels-matter/kernel/closure.ml
+--- kernel/closure.ml 2010-07-28 07:22:04.000000000 -0500
++++ kernel/closure.ml 2011-10-03 14:48:17.000000000 -0500
+@@ -17,7 +17,7 @@
+ open Esubst
+
+ let stats = ref false
+-let share = ref true
++let share = ref false
+
+ (* Profiling *)
+ let beta = ref 0
View
16 Coq_patches/grayson-closedir-after-opendir.patch
@@ -0,0 +1,16 @@
+This patch will leave many few file descriptors unclosed.
+
+ Dan Grayson
+
+diff -ur ../coq-8.3pl2-clean/lib/system.ml ./lib/system.ml
+--- ../coq-8.3pl2-clean/lib/system.ml 2010-12-24 03:55:54.000000000 -0600
++++ ./lib/system.ml 2011-10-14 12:49:30.000000000 -0500
+@@ -103,7 +103,7 @@
+ (* All subdirectories, recursively *)
+
+ let exists_dir dir =
+- try let _ = opendir dir in true with Unix_error _ -> false
++ try let _ = closedir (opendir dir) in true with Unix_error _ -> false
+
+ let skipped_dirnames = ref ["CVS"; "_darcs"]
+
View
19 Coq_patches/grayson-fix-infinite-loop.patch
@@ -0,0 +1,19 @@
+This "fixes" a seemingly infinite loop by abandoning the routine after ten repetitions.
+A better fix would involve understanding what the code was supposed to do.
+
+ Dan Grayson
+
+diff -ubr ../coq-8.3pl2-clean/tactics/tactics.ml ./tactics/tactics.ml
+--- ../coq-8.3pl2-clean/tactics/tactics.ml 2011-04-08 11:59:26.000000000 -0500
++++ ./tactics/tactics.ml 2011-10-07 09:55:24.000000000 -0500
+@@ -522,7 +522,10 @@
+
+ let pf_lookup_hypothesis_as_renamed_gen red h gl =
+ let env = pf_env gl in
++ let infinite_loop_detector = ref 0 in
+ let rec aux ccl =
++ incr infinite_loop_detector;
++ if !infinite_loop_detector > 10 then raise Redelimination;
+ match pf_lookup_hypothesis_as_renamed env ccl h with
+ | None when red ->
+ aux
View
350 Coq_patches/grayson-improved-abstraction-version2-8.3pl2.patch
@@ -0,0 +1,350 @@
+diff -ur ../coq-8.3pl2-patched/configure ./configure
+--- ../coq-8.3pl2-patched/configure 2011-04-19 02:19:00.000000000 -0500
++++ ./configure 2011-09-12 18:25:27.000000000 -0500
+@@ -6,7 +6,7 @@
+ #
+ ##################################
+
+-VERSION=8.3pl2
++VERSION=8.3pl2+improved-abstraction
+ VOMAGIC=08300
+ STATEMAGIC=58300
+ DATE=`LANG=C date +"%B %Y"`
+@@ -323,8 +323,8 @@
+ if [ "$MAKE" != "" ]; then
+ MAKEVERSION=`$MAKE -v | head -1`
+ case $MAKEVERSION in
+- "GNU Make 3.8"[12])
+- echo "You have GNU Make >= 3.81. Good!";;
++ "GNU Make 3.8"[1-9] | "GNU Make 3.8"[1-9].* | "GNU Make 3."[0-9] | "GNU Make 3."[0-9].* | "GNU Make "[4-9].* )
++ echo "You have GNU Make $MAKEVERSION >= 3.81. Good!";;
+ *)
+ OK="no"
+ if [ -x ./make ]; then
+diff -ur ../coq-8.3pl2-patched/pretyping/evd.ml ./pretyping/evd.ml
+--- ../coq-8.3pl2-patched/pretyping/evd.ml 2011-03-10 09:50:24.000000000 -0600
++++ ./pretyping/evd.ml 2011-09-11 06:30:25.000000000 -0500
+@@ -675,6 +675,11 @@
+ metas = Metamap.add mv (Clval(na,(mk_freelisted v,pb),ty)) evd.metas }
+ | _ -> anomaly "meta_reassign: not yet defined"
+
++let meta_unassign mv evd =
++ match Metamap.find mv evd.metas with
++ | Clval(na,_,ty) -> { evd with metas = Metamap.add mv (Cltyp(na,ty)) evd.metas }
++ | _ -> anomaly "meta_unassign: not yet defined"
++
+ (* If the meta is defined then forget its name *)
+ let meta_name evd mv =
+ try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
+diff -ur ../coq-8.3pl2-patched/pretyping/evd.mli ./pretyping/evd.mli
+--- ../coq-8.3pl2-patched/pretyping/evd.mli 2011-03-10 09:50:24.000000000 -0600
++++ ./pretyping/evd.mli 2011-09-11 06:30:39.000000000 -0500
+@@ -224,6 +224,7 @@
+ metavariable -> types -> ?name:name -> evar_map -> evar_map
+ val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map
+ val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map
++val meta_unassign : metavariable -> evar_map -> evar_map
+
+ (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
+ val meta_merge : evar_map -> evar_map -> evar_map
+diff -ur ../coq-8.3pl2-patched/pretyping/pretype_errors.ml ./pretyping/pretype_errors.ml
+--- ../coq-8.3pl2-patched/pretyping/pretype_errors.ml 2010-07-24 10:57:30.000000000 -0500
++++ ./pretyping/pretype_errors.ml 2011-09-13 16:23:06.000000000 -0500
+@@ -34,6 +34,7 @@
+ | CannotGeneralize of constr
+ | NoOccurrenceFound of constr * identifier option
+ | CannotFindWellTypedAbstraction of constr * constr list
++ | CannotFindAbstraction of Evd.evar_map * constr * constr list * string
+ | AbstractionOverMeta of name * name
+ | NonLinearUnification of name * constr
+ (* Pretyping *)
+@@ -178,6 +179,9 @@
+ let error_cannot_find_well_typed_abstraction env sigma p l =
+ raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l)))
+
++let error_cannot_find_abstraction env sigma c l msg =
++ raise (PretypeError (env_ise sigma env,CannotFindAbstraction (sigma,c,l,msg)))
++
+ let error_abstraction_over_meta env sigma hdmeta metaarg =
+ let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in
+ raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n)))
+diff -ur ../coq-8.3pl2-patched/pretyping/pretype_errors.mli ./pretyping/pretype_errors.mli
+--- ../coq-8.3pl2-patched/pretyping/pretype_errors.mli 2010-07-24 10:57:30.000000000 -0500
++++ ./pretyping/pretype_errors.mli 2011-09-13 16:22:42.000000000 -0500
+@@ -35,6 +35,7 @@
+ | CannotGeneralize of constr
+ | NoOccurrenceFound of constr * identifier option
+ | CannotFindWellTypedAbstraction of constr * constr list
++ | CannotFindAbstraction of Evd.evar_map * constr * constr list * string
+ | AbstractionOverMeta of name * name
+ | NonLinearUnification of name * constr
+ (* Pretyping *)
+@@ -107,6 +108,9 @@
+ val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
+ constr -> constr list -> 'b
+
++val error_cannot_find_abstraction : env -> Evd.evar_map ->
++ constr -> constr list -> string -> 'b
++
+ val error_abstraction_over_meta : env -> Evd.evar_map ->
+ metavariable -> metavariable -> 'b
+
+diff -ur ../coq-8.3pl2-patched/pretyping/unification.ml ./pretyping/unification.ml
+--- ../coq-8.3pl2-patched/pretyping/unification.ml 2010-07-26 17:12:43.000000000 -0500
++++ ./pretyping/unification.ml 2011-09-13 17:03:34.000000000 -0500
+@@ -28,6 +28,109 @@
+ open Coercion.Default
+ open Recordops
+
++let rec take n x =
++ if n = 0 then [] else
++ match x with
++ [] -> raise Not_found
++ | e::x -> e::(take (n-1) x)
++
++let rec last x = match x with
++ | [] -> error "internal error: empty list"
++ | [e] -> e
++ | _::x -> last x
++
++let all_but_last x = List.rev (List.tl (List.rev x))
++
++let is_well_typed env evd t = try ignore(Typing.type_of env evd t); true with Type_errors.TypeError _ -> false
++
++let meta_name evd mv =
++ match find_meta evd mv with
++ | Cltyp(na,_) -> na
++ | Clval(na,_,_) -> na
++
++let abstract_metas evd mvs t = List.fold_right
++ (fun mv t ->
++ mkLambda( meta_name evd mv, Typing.meta_type evd mv, replace_term (mkMeta mv) (mkRel 1) t))
++ mvs t
++
++let occurrence_count term subterm =
++ let n = ref 0 in
++ let rec f c = if eq_constr subterm c then incr n else iter_constr f c in
++ iter_constr f term;
++ !n
++
++let subsets n =
++ assert (n >= 0);
++ let rec subsets n =
++ if n = 0 then [[]]
++ else
++ let m = n-1 in
++ let s = subsets m in
++ List.append s (List.map (fun t -> m :: t) s) in
++ List.map List.rev (subsets n)
++let cartprod2 x y = List.flatten (List.map (fun t -> List.map (fun u -> t::u) y) x)
++let cartprod z = List.fold_right cartprod2 z [[]]
++let subsetsn l = cartprod (List.map subsets l)
++
++let replace_term_occ occs c by_c in_t =
++ let ctr = ref 0 in
++ let rec f x = (
++ if eq_constr c x
++ then (
++ let x' = if List.mem !ctr occs then by_c else x in
++ incr ctr;
++ x'
++ )
++ else map_constr f x
++ ) in
++ f in_t
++
++let select f x =
++ let rec select f = function
++ | [] -> []
++ | a::x -> if f a then a :: select f x else select f x in
++ select f x
++
++let abstract_list_search_warning = ref (function (env:env) -> function (evd:evar_map) -> function (survivors:constr list) -> assert false)
++
++let always_search = true (* true for development, false for production *)
++
++let abstract_list_search env evd2 typ c l =
++ let c_orig = c in
++ let l_orig = l in
++ let elimA = List.rev (take (List.length l) (List.map fst (meta_list evd2))) in
++ let k = last l in
++ let l = all_but_last l in
++ let psvar = all_but_last elimA in
++ let evd = List.fold_right meta_unassign psvar evd2 in
++ let psvalpairs = List.map (fun mv -> (mv,meta_value evd2 mv)) psvar in
++ let ispsval t =
++ let rec f = function [] -> None | (mv,v)::rest -> if eq_constr t v then Some mv else f rest in
++ f psvalpairs in
++ let c = replace_term k (mkMeta (last elimA)) c in
++ let c =
++ let rec f t = match ispsval t with Some mv -> mkMeta mv | None -> map_constr f t in
++ map_constr f c in
++ let psvargoalcount = List.map (occurrence_count c) (List.map mkMeta psvar) in
++ let totcount = List.fold_right (+) psvargoalcount 0 in
++ if totcount > 16 then error_cannot_find_abstraction env evd2 c_orig l_orig "attempted, more than 16 replacement spots";
++ let psvaroccs = subsetsn psvargoalcount in
++ let possibilities = List.map
++ (fun occlist -> List.fold_right2 (fun occ (mv,vl) goal -> replace_term_occ occ (mkMeta mv) vl goal) occlist psvalpairs c)
++ psvaroccs in
++ let survivors = select (is_well_typed env evd) possibilities in
++ let survivors = List.map (abstract_metas evd elimA) survivors in
++ begin
++ match List.length survivors with
++ 0 -> error_cannot_find_abstraction env evd2 c_orig l_orig "possible"
++ | 1 -> ()
++ | _ -> !abstract_list_search_warning env evd2 survivors
++ end;
++ let p = List.hd survivors in
++ if is_conv_leq env evd2 (Typing.type_of env evd2 p) typ
++ then p
++ else error "internal error: abstraction not convertible?"
++
+ let occur_meta_or_undefined_evar evd c =
+ let rec occrec c = match kind_of_term c with
+ | Meta _ -> raise Occur
+@@ -930,7 +1033,8 @@
+ let (evd',cllist) =
+ w_unify_to_subterm_list env flags allow_K p oplist typ evd in
+ let typp = Typing.meta_type evd' p in
+- let pred = abstract_list_all env evd' typp typ cllist in
++ let pred = try abstract_list_all env evd' typp typ cllist
++ with PretypeError _ -> abstract_list_search env evd' typp typ cllist in
+ w_merge env false flags (evd',[p,pred,(ConvUpToEta 0,TypeProcessed)],[])
+
+ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
+diff -ur ../coq-8.3pl2-patched/pretyping/unification.mli ./pretyping/unification.mli
+--- ../coq-8.3pl2-patched/pretyping/unification.mli 2010-07-24 10:57:30.000000000 -0500
++++ ./pretyping/unification.mli 2011-09-12 12:27:16.000000000 -0500
+@@ -52,3 +52,6 @@
+ (* (exported for inv.ml) *)
+ val abstract_list_all :
+ env -> evar_map -> constr -> constr -> constr list -> constr
++
++
++val abstract_list_search_warning : (env -> evar_map -> Term.constr list -> unit) ref
+diff -ur ../coq-8.3pl2-patched/proofs/logic.ml ./proofs/logic.ml
+--- ../coq-8.3pl2-patched/proofs/logic.ml 2010-07-26 17:12:43.000000000 -0500
++++ ./proofs/logic.ml 2011-09-12 11:47:14.000000000 -0500
+@@ -58,7 +58,7 @@
+ (* unification errors *)
+ | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
+- |CannotFindWellTypedAbstraction _|OccurCheck _
++ |CannotFindAbstraction _|CannotFindWellTypedAbstraction _|OccurCheck _
+ |UnsolvableImplicit _)) -> true
+ | Typeclasses_errors.TypeClassError
+ (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
+diff -ur ../coq-8.3pl2-patched/tactics/tactics.ml ./tactics/tactics.ml
+--- ../coq-8.3pl2-patched/tactics/tactics.ml 2011-10-11 07:28:57.000000000 -0500
++++ ./tactics/tactics.ml 2011-10-10 16:38:28.000000000 -0500
+@@ -134,7 +134,9 @@
+ errorlabstrm "" (pr_id id ++ str " is used in conclusion.")
+ | Evarutil.OccurHypInSimpleClause (Some id') ->
+ errorlabstrm ""
+- (pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str".")
++ (pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str"." ++ fnl() ++ fnl()
++ ++ str "The context:" ++ fnl() ++ str " " ++ Printer.pr_context_of env
++ )
+ | Evarutil.EvarTypingBreak ev ->
+ errorlabstrm ""
+ (str "Cannot remove " ++ pr_id id ++
+@@ -1912,13 +1914,8 @@
+ let argl = snd (decompose_app indtyp) in
+ let c = List.nth argl (i-1) in
+ match kind_of_term c with
+- | Var id when not (List.exists (occur_var (pf_env gl) id) avoid) ->
+- atomize_one (i-1) ((mkVar id)::avoid) gl
+ | Var id ->
+- let x = fresh_id [] id gl in
+- tclTHEN
+- (letin_tac None (Name x) (mkVar id) None allHypsAndConcl)
+- (atomize_one (i-1) ((mkVar x)::avoid)) gl
++ atomize_one (i-1) ((mkVar id)::avoid) gl
+ | _ ->
+ let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
+ Anonymous in
+diff -ur ../coq-8.3pl2-patched/test-suite/success/unification.v ./test-suite/success/unification.v
+--- ../coq-8.3pl2-patched/test-suite/success/unification.v 2010-04-07 17:01:23.000000000 -0500
++++ ./test-suite/success/unification.v 2011-09-12 17:55:41.000000000 -0500
+@@ -136,3 +136,4 @@
+ Proof.
+ intros.
+ rewrite H.
++Abort.
+diff -ur ../coq-8.3pl2-patched/test-suite/success/unification2.v ./test-suite/success/unification2.v
+--- ../coq-8.3pl2-patched/test-suite/success/unification2.v 2011-10-11 07:31:05.000000000 -0500
++++ ./test-suite/success/unification2.v 2011-09-12 18:11:59.000000000 -0500
+@@ -0,0 +1,35 @@
++(* tests to go with Grayson's patch to "destruct" for handling Univalent Foundations *)
++
++Unset Automatic Introduction.
++
++(* Voevodsky's original example: *)
++
++Definition test ( X : Type ) ( x : X ) ( fxe : forall x1 : X , identity x1 x1 ) : identity ( fxe x ) ( fxe x ).
++Proof. intros. destruct ( fxe x ). apply identity_refl. Defined.
++
++(* a harder example *)
++
++Definition UU := Type .
++Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t.
++Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X) , UU := newfoo : foo X0 x0 X0 x0.
++Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo X0 x0 X1 x1 -> foo X0 x0 X1 x1.
++Proof. intros * t. exact t. Defined.
++
++Lemma hA (T:UU) (t:T) (k : foo T t T t) : paths k (idonfoo k).
++Proof. intros.
++ destruct k.
++ unfold idonfoo.
++ apply idpath.
++Defined.
++
++(* an example with two constructors *)
++
++Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X) , UU := newfoo1 : foo' X0 x0 X0 x0 | newfoo2 : foo' X0 x0 X0 x0 .
++Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo' X0 x0 X1 x1 -> foo' X0 x0 X1 x1.
++Proof. intros * t. exact t. Defined.
++Lemma tryb2 (T:UU) (t:T) (k : foo' T t T t) : paths k (idonfoo' k).
++Proof. intros.
++ destruct k.
++ unfold idonfoo'. apply idpath.
++ unfold idonfoo'. apply idpath.
++Defined.
+diff -ur ../coq-8.3pl2-patched/toplevel/himsg.ml ./toplevel/himsg.ml
+--- ../coq-8.3pl2-patched/toplevel/himsg.ml 2010-09-24 17:23:07.000000000 -0500
++++ ./toplevel/himsg.ml 2011-09-13 17:07:40.000000000 -0500
+@@ -439,6 +439,16 @@
+ str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
+ str "which is ill-typed."
+
++let explain_cannot_find_abstraction env evd c l msg =
++ str "Abstraction over the " ++
++ str (plural (List.length l) "term") ++ spc () ++
++ hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++
++ str "not" ++ spc() ++ str msg ++ str "." ++
++ fnl() ++ fnl() ++ str "The context:" ++ fnl() ++
++ str " " ++ pr_context_of env ++
++ fnl() ++ fnl() ++ str "The term to be abstracted: " ++ fnl() ++ fnl() ++
++ str " " ++ pr_constr c
++
+ let explain_abstraction_over_meta _ m n =
+ strbrk "Too complex unification problem: cannot find a solution for both " ++
+ pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
+@@ -502,6 +512,8 @@
+ | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
+ | CannotFindWellTypedAbstraction (p,l) ->
+ explain_cannot_find_well_typed_abstraction env p l
++ | CannotFindAbstraction (evd,c,l,msg) ->
++ explain_cannot_find_abstraction env evd c l msg
+ | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
+ | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
+
+@@ -850,3 +862,8 @@
+ pr_enum pr_call calls ++ strbrk kind_of_last_call)
+ else
+ mt ()
++
++let _ =
++ Unification.abstract_list_search_warning :=
++ function env -> function evd -> function l ->
++ msgnl(str "warning: multiple well-typed abstractions found:" ++ (fnl()) ++ prlist_with_sep fnl pr_constr l)
View
557 Generalities/uu0.v
291 additions, 266 deletions not shown
View
94 Generalities/uuu.v
@@ -1,38 +1,7 @@
-(** * Introduction ( by Vladimir Voevodsky , Feb. 2010 - Jun. 2011 )
+(** * Introduction. Vladimir Voevodsky . Feb. 2010 - Sep. 2011
-This is the first of the group of files which contain the (current state of) the mathematical library for the proof assistant Coq based on the Univalent Foundations.
-This particular files contains only definitions and results which do not depend on the concept of equality and dependent sums.
+This is the first in the group of files which contain the (current state of) the mathematical library for theproof assistant Coq based on the Univalent Foundations. It contains some new notations for constructions defined in Coq.Init library as well as the definition of dependent sum as a record.
-Univalent Foundations are inspired by the univalent model of type theory which interprets types as homotopy types, Martin-Lof equality as paths spaces and universes as bases of universal ("univalent") fibrations. For a detailed overview of the content see the table of content in toc.html . In has been modified from the eralier version in a several places but most importantly the part of the earlier file concerning the h-version of the inhabited construction and constructions related to finite sets have been moved to separate files.
-
-I tried to keep the notations such that the names of types which are (expected to be) a property in the sense of being of h-level 1 start with "is" but I have not been very consistent about it.
-
-There is an increasing number of theorems which have very short proofs based on the univalence axiom which are given much longer proofs here. One hopes that eventually a mechnaical procedure for the replacement of proofs using the univalence axiom by proofs which only use it in some computationally uninformative ways will be found but until then I am not using the univalence axiom in any of the constructions.
-
-
-IMPORTANT: for those who may want to add to these files. There are some rules which have to be followed in creating new definitions and theorems which at the moment are not tracked by the proof checker.
-
-1. The current system of Coq is not completely compatible with the univalent semantics. The problem (the only one as far as I know) lies in the way the universe levels (u-levels) are assigned to the objects defined by the inductive definitions of the form
-
-Inductive Ind (...)...(...): A -> Type := ...
-
-
-The current u-level assignemet takes into account the u-levels of the constructors but not the u-level of A. To ensure compatibility with the univalent model the u-level of Ind should be no less than the u-level of A. The u-levels of the parameters (the types appearing in (...)...(...) ) do not matter.
-
-A particular case of this problem is the "singleton elimination" rule which provides a good example of this incompatibility. The inductive definition of the identity types which uses one of the points as a parametr has A=:T (the underlying type) but since no mention of T appears in the constructor the system considers that there are no u-level restrictions on the resulting object and in particular that it can be placed in Prop while still having the full Ind_rect elimninator (see elimination, singleton elimination in the Index to the Refernce Manual).
-
-Since in the present approach the universe management is made explicit one has:
-
-RULE 1 Do not use inductive definitions of the form
-
-Inductive Ind (...)...(...): A -> UU := ...
-
-unless all the "arguments" of A can be typed to UU.
-
-
-2. While it does not lead directly to any contradictions the shape of the foundations suggests very strongly that at the moment it is best to completely avoid the use of the universes Prop and Set. Instead we should use the the conditions isaprop and isaset which are applicable to the types of any of the type universes.
-
-Note on implicit arguments : In the latest version of my univalent library I started to systematically use implicit arguments. The rules which I am using for assessing which arguments should be made implicit are somewhat different from the rules which the automatic Coq system for detection of implicit arguments is using. For example given arguments ( X : Type ) ( x : X ) , the Coq command Implicit Arguments would assign implicit ( although *not* strict implicit ) status to X . I do not consider X to be an implicit argument in this case due to the existence of subtyping for universes . On the other hand I do make the type argument of [ paths ] to be implicit because [ paths X X' ] is in fact independent from the universe in which X and X' are considered.
*)
@@ -43,43 +12,49 @@ Note on implicit arguments : In the latest version of my univalent library I sta
Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *)
+(** Universe structure *)
-(** The empty type is introduced in Coq.Init.Datatypes by the line :
+Notation UUU := Set .
-Inductive Empty_set : Set := .
+(** Empty type. The empty type is introduced in Coq.Init.Datatypes by the line:
-*)
+[ Inductive Empty_set : Set := . ]
+*)
-Notation UUU := Set .
Notation empty := Empty_set.
-(** Idenity types are introduced in Coq.Init.Datatypes by the lines :
+(** Identity Types. Idenity types are introduced in Coq.Init.Datatypes by the lines :
-Inductive identity ( A:Type ) (a:A) : A -> Type := identity_refl : identity _ a a.
-Hint Resolve identity_refl : core.
+[ Inductive identity ( A : Type ) ( a : A ) : A -> Type := identity_refl : identity _ a a .
+Hint Resolve identity_refl : core . ]
*)
Notation paths := identity .
Notation idpath := identity_refl .
-(** *** Dependent sums (fibrations) *)
+(** Dpendent sums.
-Record total2 { T: Type } ( P: T -> Type ) := tpair { pr21_c : T ; pr22_c : P pr21_c }.
+One can not use a new record each time one needs it because the general theorems about this construction would not apply to new instances of "Record" due to the "generativity" of inductive definitions in Coq. One could use "Inductive" instead of "Record" here but using "Record" which is equivalent to "Structure" allows us later to use the mechanism of canonical structures with total2. *)
-Definition pr21 { T: Type } { P : T -> Type } ( tp : total2 P ) := match tp with tpair t p => t end .
-Definition pr22 { T: Type } { P : T -> Type } ( tp : total2 P ) := match tp as a return P ( pr21 a ) with tpair t p => p end .
+Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T ; pr2 : P pr1 }.
-Implicit Arguments tpair [ T ] .
-(* Implicit Arguments pr21 [ T P ] .
-Implicit Arguments pr22 [ T P ] . *)
+(* Definition pr1 { T: Type } { P : T -> Type } ( tp : total2 P ) := match tp with tpair t p => t end .
+Definition pr2 { T: Type } { P : T -> Type } ( tp : total2 P ) := match tp as a return P ( pr1 a ) with tpair t p => p end . *)
+Implicit Arguments tpair [ T ] .
+Implicit Arguments pr1 [ T P ] .
+Implicit Arguments pr2 [ T P ] .
-(** One can not use a new record each time one needs it because the general theorems about this construction would not apply to new instances of "Record" due to the "generativity" of inductive definitions in Coq. One could use "Inductive" instead of "Record" here but using "Record" which is equivalent to "Structure" allows us later to use the mechanism of canonical structures with total2. *)
+(** Coproducts .
+The coproduct of two types is introduced in Coq.Init.Datatypes by the lines:
-(** [ sum A B ], written [ A + B ], is the disjoint sum of [A] and [B] . The lest and right inclusions are denoted by [ inl ] and [ inr ] in Coq.Init.Datatypes *)
+[ Inductive sum (A B:Type) : Type :=
+ | inl : A -> sum A B
+ | inr : B -> sum A B. ]
+*)
Notation coprod := sum .
@@ -92,28 +67,15 @@ Implicit Arguments ii1 [ A B ] .
Implicit Arguments ii2 [ A B ] .
-Check (paths O O) .
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+(** The phantom type family ( following George Gonthier ) *)
+Inductive Phant ( T : Type ) := phant : Phant T .
+(** The following command checks wheather the patch which modifies the universe level assignement for inductive types have been installed. With the patch it returns [ paths 0 0 : UUU ] . Without the patch it returns [ paths 0 0 : Prop ]. *)
+Check (paths O O) .
View
14 Proof_of_Extensionality/funextfun.v
@@ -39,10 +39,10 @@ Axiom weqpathsweq0 : forall ( T1 T2 : UU ) ( w : weq T1 T2 ) , paths ( eqweqmap
Theorem univfromtwoaxioms ( T1 T2 : UU ) : isweq ( @eqweqmap T1 T2 ).
Proof. intros. set ( P1 := fun XY : dirprod UU UU => ( match XY with tpair X Y => paths X Y end ) ) . set ( P2 := fun XY : dirprod UU UU => match XY with tpair X Y => weq X Y end ) . set ( Z1 := total2 P1 ). set ( Z2 := total2 P2 ). set ( f := totalfun _ _ ( fun XY : dirprod UU UU => match XY with tpair X Y => @eqweqmap X Y end ) : Z1 -> Z2 ) . set ( g := totalfun _ _ ( fun XY : dirprod UU UU => match XY with tpair X Y => weqtopaths0 X Y end ) : Z2 -> Z1 ) . set ( s1 := fun X Y : UU => fun w : weq X Y => tpair P2 ( dirprodpair X Y ) w ) . set ( efg := fun a => match a as a' return ( paths ( f ( g a' ) ) a' ) with tpair ( tpair X Y ) w => ( maponpaths ( s1 X Y ) ( weqpathsweq0 X Y w ) ) end ) .
-set ( h := fun a1 : Z1 => pr21 ( pr21 a1 ) ) .
-assert ( egf0 : forall a1 : Z1 , paths ( pr21 ( g ( f a1 ) ) ) ( pr21 a1 ) ). intro. apply idpath.
-assert ( egf1 : forall a1 a1' : Z1 , paths ( pr21 a1' ) ( pr21 a1 ) -> paths a1' a1 ). intros. set ( X' := maponpaths ( @pr21 _ _ ) X ).
-assert ( is : isweq h ). apply isweqpr21pr21 . apply ( invmaponpathsweq ( weqpair h is ) _ _ X' ).
+set ( h := fun a1 : Z1 => pr1 ( pr1 a1 ) ) .
+assert ( egf0 : forall a1 : Z1 , paths ( pr1 ( g ( f a1 ) ) ) ( pr1 a1 ) ). intro. apply idpath.
+assert ( egf1 : forall a1 a1' : Z1 , paths ( pr1 a1' ) ( pr1 a1 ) -> paths a1' a1 ). intros. set ( X' := maponpaths ( @pr1 _ _ ) X ).
+assert ( is : isweq h ). apply isweqpr1pr1 . apply ( invmaponpathsweq ( weqpair h is ) _ _ X' ).
set ( egf := fun a1 => ( egf1 _ _ ( egf0 a1 ) ) ).
set ( is2 := gradth _ _ egf efg ).
apply ( isweqtotaltofib P1 P2 ( fun XY : dirprod UU UU => match XY with tpair X Y => @eqweqmap X Y end ) is2 ( dirprodpair T1 T2 ) ). Defined.
@@ -114,12 +114,12 @@ Lemma eqcor0 { X X' : UU } ( w : weq X X' ) ( Y : UU ) ( f1 f2 : X' -> Y ) : pa
Proof. intros. apply ( invmaponpathsweq ( weqpair _ ( isweqcompwithweq w Y ) ) f1 f2 ). assumption. Defined.
-Lemma apathpr1topr2 ( T : UU ) : paths ( fun z : pathsspace T => pr21 z ) ( fun z : pathsspace T => pr21 ( pr22 z ) ).
-Proof. intro. apply ( eqcor0 ( weqpair _ ( isweqdeltap T ) ) _ ( fun z : pathsspace T => pr21 z ) ( fun z : pathsspace T => pr21 ( pr22 z ) ) ( idpath ( idfun T ) ) ) . Defined.
+Lemma apathpr1topr ( T : UU ) : paths ( fun z : pathsspace T => pr1 z ) ( fun z : pathsspace T => pr1 ( pr2 z ) ).
+Proof. intro. apply ( eqcor0 ( weqpair _ ( isweqdeltap T ) ) _ ( fun z : pathsspace T => pr1 z ) ( fun z : pathsspace T => pr1 ( pr2 z ) ) ( idpath ( idfun T ) ) ) . Defined.
Theorem funextfun { X Y : UU } ( f1 f2 : X -> Y ) ( e : forall x : X , paths ( f1 x ) ( f2 x ) ) : paths f1 f2.
-Proof. intros. set ( f := fun x : X => pathsspacetriple Y ( e x ) ) . set ( g1 := fun z : pathsspace Y => pr21 z ) . set ( g2 := fun z : pathsspace Y => pr21 ( pr22 z ) ). assert ( e' : paths g1 g2 ). apply ( apathpr1topr2 Y ). assert ( ee : paths ( fun x : X => f1 x ) ( fun x : X => f2 x ) ). change ( paths (fun x : X => g1 ( f x ) ) (fun x : X => g2 ( f x ) ) ) . destruct e' . apply idpath . apply etacoronpaths. apply ee . Defined.
+Proof. intros. set ( f := fun x : X => pathsspacetriple Y ( e x ) ) . set ( g1 := fun z : pathsspace Y => pr1 z ) . set ( g2 := fun z : pathsspace Y => pr1 ( pr2 z ) ). assert ( e' : paths g1 g2 ). apply ( apathpr1topr Y ). assert ( ee : paths ( fun x : X => f1 x ) ( fun x : X => f2 x ) ). change ( paths (fun x : X => g1 ( f x ) ) (fun x : X => g2 ( f x ) ) ) . destruct e' . apply idpath . apply etacoronpaths. apply ee . Defined.
(* End of the file funextfun.v *)
View
23 README
@@ -1,8 +1,8 @@
-By Vladimir Voevodsky Feb. 2010 - Sep. 2011 .
+By Vladimir Voevodsky Feb. 2010 - Nov. 2011 .
-This is the current version (as of Sep. 2 , 2011) of the mathematical library for the proof assistant Coq based on the univalent semantics for the calculus of inductive constructions. The best way to see in detail what the files in these subdirectories are about is to generate the corresponding tables of content with coqdoc . Here we give a brief outline of the library structure .
+This is the current version (as of Nov. 6 , 2011) of the mathematical library for the proof assistant Coq based on the univalent semantics for the calculus of inductive constructions. The best way to see in detail what the files in these subdirectories are about is to generate the corresponding tables of content with coqdoc . Here we give a brief outline of the library structure .
-Important : files in the library starting with hProp.v will not compile without a type_in_type patch which turns off the universe consistency checking . This is hopefully a temporary situation which will be corrected when better universe management is implememnted in Coq . One is also advised to use a patch which modifies the rule by which the universe level of inductive definitions is computed . If the later patch is applied correctly then the compilation of the first file uuu.v should produce a message of the form [ paths 0 0 : UUU ] . Without a patch the message will be [ paths 0 0 : Prop ] .
+Important : files in the library starting with hProp.v will not compile without a type_in_type patch which turns off the universe consistency checking . This is a temporary situation which will be corrected when better universe management is implememnted in Coq . We also use a patch which modifies the rule by which the universe level of inductive definitions is computed . If the later patch is applied correctly then the compilation of the first file uuu.v should produce a message of the form [ paths 0 0 : UUU ] . Without a patch the message will be [ paths 0 0 : Prop ] .
The library contains subdirectories Generalities/ hlevel1/ hlevel2/ and /Proof_of_Extensionality .
@@ -10,8 +10,21 @@ Directory Generalities/ contains files uuu.v and uu0.v . The file uuu.v contain
Directory hlevel1/ contains one file hProp.v with results and constructions related to types of h-level 1 i.e. to types which correspond to "propositions" in our formalization. Some of the results here use " resizing rules " and therefore it will currently not compile without a type_in_type patch . Note that we continue to keep track of universe levels in these files "by hand" and use only those "universe re-assigment" or "resizing" rules which are semantically justified. Some of the results in this file also use the univalence axiom for hProp called [ uahp ] which is equivalent to the axiom asserting that if two propositions are logically equivalent then they are equal .
-Directory hlevel2/ contains files with constructions and results related to types of hlevel 2 i.e. to types corresponding to sets in our formalization . The main file is hSet.v . It contains most general definitions related to sets including the constructions related to set-quotinets of types . The next file in the hierarchy is algebra1.v it contains many definitions and constructions of general abstract algebra culminating at the moment in the construction of localizations for commutative rings . The next file is hnat.v which contains many simple lemmas about arithmetic and inequalities on natural numbers . Then the hierarchy branches into the files stnfsets.v and finitesets.v which introduce constructions related to standard and general finite sets respectively and file hz.v which introduces the first few cosntructions related to the integer arithmetic . The abelian group of integers is defined as the abelian group associated with the abelian monoid [ nat ] using then general constructions in algebra1.v
-At the end of files finitesets.v and hz.v there are some sample computations which show that we use the axioms carefully enough so that the relevant terms of types [ bool ] and [ nat ] evaluate properly.
+Directory hlevel2/ contains files with constructions and results related to types of hlevel 2 i.e. to types corresponding to sets in our formalization .
+
+The first file is hSet.v . It contains most general definitions related to sets including the constructions related to set-quotients of types .
+
+The next group of files in the hierarchy are algebra1(a b c d).v which contains many definitions and constructions of general abstract algebra culminating at the moment in the construction of the field of fractions of an integral domain. The files also contain definitions and results about the relations on algebraic structures .
+
+The next file is hnat.v which contains many simple lemmas about arithmetic and comparisons on natural numbers .
+
+Then the hierarchy branches.
+
+On one branch there are files stnfsets.v and finitesets.v which introduce constructions related to standard and general finite sets respectively.
+
+On another branch there are files hz.v and hq.v which introduce the basic cosntructions related to the integer and rational arithmetic as particular cases of the general theorems of the algebra1 group of files.
+
+At the end of files finitesets.v, hz.v and hq.v there are sample computations which show that despite our use of stnadard extensionality axioms the relevant terms of types [ bool ] and [ nat ] fully normalize. The last computation example in hq.v which evaluates the integral part of 10/-3 takes relatively long time ( about 30 sec. on my computer, it should work much faster with the stnadard optimized version of the "call by need" normalization algorithm which is switched off by one of the patches which I use, see the explanation in the README file of the patches directory) and it might make sense to comment it out.
Directory Proof_of_Extensionality/ contains the formulation of general Univalence Axiom and a proof that it implies functional extensionality .
View
14 forcoqdoc
@@ -0,0 +1,14 @@
+Generalities/uuu.v
+Generalities/uu0.v
+hlevel1/hProp.v
+hlevel2/hSet.v
+hlevel2/algebra1a.v
+hlevel2/algebra1b.v
+hlevel2/algebra1c.v
+hlevel2/algebra1d.v
+hlevel2/hnat.v
+hlevel2/stnfsets.v
+hlevel2/finitesets.v
+hlevel2/hz.v
+hlevel2/hq.v
+
View
147 hlevel1/hProp.v
@@ -2,11 +2,11 @@
In this file we introduce the hProp - an analog of Prop defined based on the univalent semantics. We further introduce the hProp version of the "inhabited" construction - i.e. for any [ T ] in [ UU0 ] we construct an object [ ishinh T ] and a function [ hinhpr : T -> ishinh T ] which plays the role of [ inhabits ] from the Coq standard library. The semantic meaning of [ hinhpr ] is that it is universal among functions from [ T ] to objects of hProp. Proving that [ ishinh T ] is in [ hProp ] requires a resizing rule which can be written in the putative notation for such rules as follows :
-RR1 ( U1 U2 : Univ ) ( X : U1 ) ( is : isaprop X ) |- X : U2 .
+Resizing Rule RR1 ( U1 U2 : Univ ) ( X : U1 ) ( is : isaprop X ) |- X : U2 .
Further in the file we introduce the univalence axiom for hProp and a proof of the fact that it is equivalent to a simplier and better known axiom [ uahp ]. We prove that this axiom implies that [ hProp ] satisfies [ isaset ] i.e. it is a type of h-level 2 . This requires another resizing rule :
-RR2 ( U1 U2 : Univ ) |- @hProp U1 : U2 .
+Resizing Rule RR2 ( U1 U2 : Univ ) |- @hProp U1 : U2 .
Since resizing rules are not currently implemented in Coq the file does not compile without a patch provided by Hugo Herbelin which turns off the universe consistency verification. We do however keep track of universes in our development "by hand" to ensure that when the resizing rules will become available the current proofs will verify correctly. To point out which results require resizing rules in a substantial way we mark the first few of such reults by (** RR1 *) or (** RR2 *) comment .
@@ -37,8 +37,7 @@ Definition UU0 := UU .
(* end of " Preambule " . *)
-
-
+(** ** To upstream files *)
@@ -46,10 +45,14 @@ Definition UU0 := UU .
Definition hProp := total2 ( fun X : UU0 => isaprop X ) .
-Definition hProppair:= tpair (fun X : UU0 => isaprop X ) .
-Definition hProppr21 := @pr21 _ _ : hProp -> Type .
-Coercion hProppr21: hProp >-> Sortclass.
+Definition hProppair ( X : UU0 ) ( is : isaprop X ) : hProp := tpair (fun X : UU0 => isaprop X ) X is .
+Definition hProppr1 := @pr1 _ _ : hProp -> Type .
+Coercion hProppr1: hProp >-> Sortclass.
+
+(** ** The type [ tildehProp ] of pairs ( P , p : P ) where [ P : hProp ] *)
+Definition tildehProp := total2 ( fun P : hProp => P ) .
+Definition tildehProppair { P : hProp } ( p : P ) : tildehProp := tpair _ P p .
(** The following re-definitions should make proofs easier in the future when the unification algorithms in Coq are improved . At the moment they create more complications than they eliminate ( e.g. try to prove [ isapropishinh ] with [ isaprop ] in [ hProp ] ) so for the time being they are commented out .
@@ -84,36 +87,47 @@ Definition isdeceq ( X : UU0 ) : hProp := hProppair _ ( isapropisdeceq X ) .
Definition ishinh_UU ( X : UU0 ) := forall P: hProp, ( ( X -> P ) -> P ).
-Lemma isapropishinh ( X : UU0 ) : isaprop ( ishinh_UU X ). (** RR1 *)
-Proof. intro. apply impred . intro P . apply impred. intro. apply ( pr22 P ) . Defined .
+Lemma isapropishinh ( X : UU0 ) : isaprop ( ishinh_UU X ).
+Proof. intro. apply impred . intro P . apply impred. intro. apply ( pr2 P ) . Defined .
-Definition ishinh ( X : UU0 ) : hProp := hProppair ( ishinh_UU X ) ( isapropishinh X ) .
+Definition ishinh ( X : UU0 ) : hProp := hProppair ( ishinh_UU X ) ( isapropishinh X ) .
+Canonical Structure ishinh . (** RR1 *)
Definition hinhpr ( X : UU0 ) : X -> ishinh X := fun x : X => fun P : hProp => fun f : X -> P => f x .
Definition hinhfun { X Y : UU0 } ( f : X -> Y ) : ishinh_UU X -> ishinh_UU Y := fun isx : ishinh X => fun P : _ => fun yp : Y -> P => isx P ( fun x : X => yp ( f x ) ) .
-Definition hinhuniv { X : UU0 } { P: hProp } ( f : X -> P ) ( wit : ishinh_UU X ) : P := wit P f .
+Definition hinhuniv { X : UU0 } { P : hProp } ( f : X -> P ) ( wit : ishinh_UU X ) : P := wit P f .
+
(** Note that the previous definitions do not require RR1 in an essential way ( except for the placing of [ ishinh ] in [ hProp UU0 ] - without RR1 it would be placed in [ hProp UU1 ] ) . The first place where RR1 is essentially required is in application of [ hinhuniv ] to a function [ X -> ishinh Y ] *)
Definition hinhand { X Y : UU0 } ( inx1 : ishinh_UU X ) ( iny1 : ishinh_UU Y) : ishinh ( dirprod X Y ) := fun P:_ => ddualand (inx1 P) (iny1 P).
-Definition hinhuniv2 { X Y : UU0 } { P : hProp } ( f : X -> Y -> P ) ( isx : ishinh_UU X ) ( isy : ishinh_UU Y ) : P := hinhuniv ( fun xy : dirprod X Y => f ( pr21 xy ) ( pr22 xy ) ) ( hinhand isx isy ) .
+Definition hinhuniv2 { X Y : UU0 } { P : hProp } ( f : X -> Y -> P ) ( isx : ishinh_UU X ) ( isy : ishinh_UU Y ) : P := hinhuniv ( fun xy : dirprod X Y => f ( pr1 xy ) ( pr2 xy ) ) ( hinhand isx isy ) .
-Definition hinhfun2 { X Y Z : UU0 } ( f : X -> Y -> Z ) ( isx : ishinh_UU X ) ( isy : ishinh_UU Y ) : ishinh Z := hinhfun ( fun xy: dirprod X Y => f ( pr21 xy ) ( pr22 xy ) ) ( hinhand isx isy ) .
+Definition hinhfun2 { X Y Z : UU0 } ( f : X -> Y -> Z ) ( isx : ishinh_UU X ) ( isy : ishinh_UU Y ) : ishinh Z := hinhfun ( fun xy: dirprod X Y => f ( pr1 xy ) ( pr2 xy ) ) ( hinhand isx isy ) .
Definition hinhunivcor1 ( P : hProp ) : ishinh_UU P -> P := hinhuniv ( idfun P ).
Notation hinhprinv := hinhunivcor1 .
+(** *** [ ishinh ] and negation [ neg ] *)
+
+
+Lemma weqishinhnegtoneg ( X : UU0 ) : weq ( ishinh ( neg X ) ) ( neg X ) .
+Proof . intro . assert ( lg : logeq ( ishinh ( neg X ) ) ( neg X ) ) . split . simpl . apply ( @hinhuniv _ ( hProppair _ ( isapropneg X ) ) ) . simpl . intro nx . apply nx . apply hinhpr . apply ( weqimplimpl ( pr1 lg ) ( pr2 lg ) ( pr2 ( ishinh _ ) ) ( isapropneg X ) ) . Defined .
+
+Lemma weqnegtonegishinh ( X : UU0 ) : weq ( neg X ) ( neg ( ishinh X ) ) .
+Proof . intro . assert ( lg : logeq ( neg ( ishinh X ) ) ( neg X ) ) . split . apply ( negf ( hinhpr X ) ) . intro nx . unfold neg . simpl . apply ( @hinhuniv _ ( hProppair _ isapropempty ) ) . apply nx . apply ( weqimplimpl ( pr2 lg ) ( pr1 lg ) ( isapropneg _ ) ( isapropneg _ ) ) . Defined .
+
(** *** [ ishinh ] and [ coprod ] *)
-Lemma hinhcoprod ( X Y : UU0 ) ( is : ishinh_UU ( coprod ( ishinh X ) ( ishinh Y ) ) ) : ishinh ( coprod X Y ) .
+Lemma hinhcoprod ( X Y : UU0 ) ( is : ishinh ( coprod ( ishinh X ) ( ishinh Y ) ) ) : ishinh ( coprod X Y ) .
Proof. intros . unfold ishinh. intro P . intro CP. set (CPX := fun x : X => CP ( ii1 x ) ) . set (CPY := fun y : Y => CP (ii2 y) ). set (is1P := is P).
assert ( f : coprod ( ishinh X ) ( ishinh Y ) -> P ) . apply ( sumofmaps ( hinhuniv CPX ) ( hinhuniv CPY ) ). apply (is1P f ) . Defined.
@@ -126,34 +140,93 @@ Definition htrue : hProp := hProppair unit isapropunit.
Definition hfalse : hProp := hProppair empty isapropempty.
-Definition hconj ( P Q : hProp ) : hProp := hProppair ( dirprod P Q ) (isofhleveldirprod ( S O ) _ _ ( pr22 P ) ( pr22 Q ) ).
+Definition hconj ( P Q : hProp ) : hProp := hProppair ( dirprod P Q ) ( isapropdirprod _ _ ( pr2 P ) ( pr2 Q ) ).
+
+Definition hdisj ( P Q : UU0 ) : hProp := ishinh ( coprod P Q ) .
+
+Definition hneg ( P : UU0 ) : hProp := hProppair ( neg P ) ( isapropneg P ) .
-Definition hdisj ( P Q : hProp ) : hProp := ishinh ( coprod P Q ) .
+Definition himpl ( P : UU0 ) ( Q : hProp ) : hProp.
+Proof. intros. split with ( P -> Q ) . apply impred. intro. apply (pr2 Q). Defined.
-Definition hneg (P: hProp) : hProp.
-Proof. intro. split with (P -> empty). apply impred. intro. apply isapropempty. Defined.
+Definition hexists { X : UU0 } ( P : X -> UU0 ) := ishinh ( total2 P ) .
-Definition himpl (P Q : hProp) : hProp.
-Proof. intros. split with (P -> Q). apply impred. intro. apply (pr22 Q). Defined.
+Definition wittohexists { X : UU0 } ( P : X -> UU0 ) ( x : X ) ( is : P x ) : hexists P := hinhpr ( total2 P ) (tpair _ x is ) .
-Definition hforall { X : UU0 } ( P : X -> hProp ) : hProp.
-Proof. intros. split with (forall x:X, P x). apply impred. intro. apply (pr22 (P t)). Defined.
+Definition total2tohexists { X : UU0 } ( P : X -> UU0 ) : total2 P -> hexists P := hinhpr _ .
-Definition hexists { X:UU0 } (P: X -> hProp) : hProp := ishinh (total2 P).
+Definition weqneghexistsnegtotal2 { X : UU0 } ( P : X -> UU0 ) : weq ( neg ( hexists P ) ) ( neg ( total2 P ) ) .
+Proof . intros . assert ( lg : ( neg ( hexists P ) ) <-> ( neg ( total2 P ) ) ) . split . apply ( negf ( total2tohexists P ) ) . intro nt2 . unfold neg . change ( ishinh_UU ( total2 P ) -> hfalse ) . apply ( hinhuniv ) . apply nt2 . apply ( weqimplimpl ( pr1 lg ) ( pr2 lg ) ( isapropneg _ ) ( isapropneg _ ) ) . Defined .
-Definition wittohexists { X : UU0 } (P: X -> hProp)(x:X)(is: P x): hexists P := hinhpr (total2 P) (tpair _ x is).
+
+(** *** Associativity and commutativity of [ hdisj ] and [ hconj ] up to logical equivalence *)
+
+Lemma islogeqcommhdisj { P Q : hProp } : hdisj P Q <-> hdisj Q P .
+Proof . intros . split . simpl . apply hinhfun . apply coprodcomm . simpl . apply hinhfun . apply coprodcomm . Defined .
+
(** *** Proof of the only non-trivial axiom of intuitionistic logic for our constructions. For the full list of axioms see e.g. http://plato.stanford.edu/entries/logic-intuitionistic/ *)
-Lemma hconjtohdisj (P Q R : hProp) : hconj ( himpl P R ) ( himpl Q R ) -> himpl ( hdisj P Q ) R .
+Lemma hconjtohdisj ( P Q : UU0 ) ( R : hProp ) : hconj ( himpl P R ) ( himpl Q R ) -> himpl ( hdisj P Q ) R .
Proof. intros P Q R X0.
assert (s1: hdisj P Q -> R) . intro X1.
-assert (s2: coprod P Q -> R ) . intro X2. destruct X2 as [ XP | XQ ]. apply X0. assumption. apply ( pr22 X0 ). assumption.
-apply ( hinhuniv s2 ). assumption. unfold himpl. assumption. Defined.
+assert (s2: coprod P Q -> R ) . intro X2. destruct X2 as [ XP | XQ ]. apply X0. apply XP . apply ( pr2 X0 ). apply XQ .
+apply ( hinhuniv s2 ). apply X1 . unfold himpl. simpl . apply s1 . Defined.
+
+
+
+
+(** *** Negation and quantification.
+
+There are four standard implications in classical logic which can be summarized as ( neg ( forall P ) ) <-> ( exists ( neg P ) ) and ( neg ( exists P ) ) <-> ( forall ( neg P ) ) . Of these four implications three are provable in the intuitionistic logic. The remaining implication ( neg ( forall P ) ) -> ( exists ( neg P ) ) is not provable in general . For a proof in the case of bounded quantification of decidable predicates on natural numbers see hnat.v . For some other cases when these implications hold see ??? . *)
+
+Lemma hexistsnegtonegforall { X : UU0 } ( F : X -> UU0 ) : hexists ( fun x : X => neg ( F x ) ) -> neg ( forall x : X , F x ) .
+Proof . intros X F . simpl . apply ( @hinhuniv _ ( hProppair _ ( isapropneg (forall x : X , F x ) ) ) ) . simpl . intros t2 f2 . destruct t2 as [ x d2 ] . apply ( d2 ( f2 x ) ) . Defined .
+
+Lemma forallnegtoneghexists { X : UU0 } ( F : X -> UU0 ) : ( forall x : X , neg ( F x ) ) -> neg ( hexists F ) .
+Proof. intros X F nf . change ( ( ishinh_UU ( total2 F ) ) -> hfalse ) . apply hinhuniv . intro t2 . destruct t2 as [ x f ] . apply ( nf x f ) . Defined .
+Lemma neghexisttoforallneg { X : UU0 } ( F : X -> UU0 ) : neg ( hexists F ) -> forall x : X , neg ( F x ) .
+Proof . intros X F nhe x . intro fx . apply ( nhe ( hinhpr _ ( tpair F x fx ) ) ) . Defined .
+Definition weqforallnegtonegexists { X : UU0 } ( F : X -> UU0 ) : weq ( forall x : X , neg ( F x ) ) ( neg ( hexists F ) ) .
+Proof . intros . apply ( weqimplimpl ( forallnegtoneghexists F ) ( neghexisttoforallneg F ) ) . apply impred . intro x . apply isapropneg . apply isapropneg . Defined .
+
+
+
+(** *** Negation and conjunction ( "and" ) and disjunction ( "or" ) .
+
+There are four implications in classical logic ( ( neg X ) and ( neg Y ) ) <-> ( neg ( X or Y ) ) and ( ( neg X ) or ( neg Y ) ) <-> ( neg ( X and Y ) ) . Of these four, three are provable unconditionally in the intuitionistic logic and the remaining one ( neg ( X and Y ) ) -> ( ( neg X ) or ( neg Y ) ) is provable only if one of the propositions is deidable. These two cases are proved in uu0.v under the names [ fromneganddecx ] and [ fromneganddecy ] . *)
+
+Lemma tonegdirprod { X Y : UU0 } ( is : hdisj ( neg X ) ( neg Y ) ) : neg ( dirprod X Y ) .
+Proof. intros X Y . simpl . apply ( @hinhuniv _ ( hProppair _ ( isapropneg ( dirprod X Y ) ) ) ) . intro c . destruct c as [ nx | ny ] . simpl . intro xy . apply ( nx ( pr1 xy ) ) . simpl . intro xy . apply ( ny ( pr2 xy ) ) . Defined .
+
+Lemma tonegcoprod { X Y : UU } ( is : dirprod ( neg X ) ( neg Y ) ) : neg ( coprod X Y ) .
+Proof . intros. intro c . destruct c as [ x | y ] . apply ( pr1 is x ) . apply ( pr2 is y ) . Defined .
+
+Lemma toneghdisj { X Y : UU } ( is : dirprod ( neg X ) ( neg Y ) ) : neg ( hdisj X Y ) .
+Proof . intros . unfold hdisj. apply ( weqnegtonegishinh ) . apply tonegcoprod . apply is . Defined .
+
+Lemma fromnegcoprod { X Y : UU0 } ( is : neg ( coprod X Y ) ) : dirprod ( neg X ) ( neg Y ) .
+Proof . intros . split . exact ( fun x => is ( ii1 x ) ) . exact ( fun y => is ( ii2 y ) ) . Defined .
+
+Lemma hdisjtoimpl { P : UU0 } { Q : hProp } : hdisj P Q -> ( neg P -> Q ) .
+Proof . intros P Q . assert ( int : isaprop ( neg P -> Q ) ) . apply impred . intro . apply ( pr2 Q ) . simpl . apply ( @hinhuniv _ ( hProppair _ int ) ) . simpl . intro pq . destruct pq as [ p | q ] . intro np . destruct ( np p ) . intro np . apply q . Defined .
+
+
+
+(** *** Property of being deidable and [ hdisj ] ( "or" ) .
+
+For being deidable [ hconj ] see [ isdecpropdirprod ] in uu0.v *)
+
+Lemma isdecprophdisj { X Y : UU0 } ( isx : isdecprop X ) ( isy : isdecprop Y ) : isdecprop ( hdisj X Y ) .
+Proof . intros . apply isdecpropif . apply ( pr2 ( hdisj X Y ) ) . destruct ( pr1 isx ) as [ x | nx ] . apply ( ii1 ( hinhpr _ ( ii1 x ) ) ) . destruct ( pr1 isy ) as [ y | ny ] . apply ( ii1 ( hinhpr _ ( ii2 y ) ) ) . apply ( ii2 ( toneghdisj ( dirprodpair nx ny ) ) ) . Defined .
+
+
+
+
(** *** The double negation version of [ hinhabited ] ( does not require RR1 ) . *)
@@ -189,7 +262,7 @@ Proof. intros . destruct e . apply idweq. Defined.
Definition weqtopathshProp { P P' : hProp } (w: weq P P' ): @paths hProp P P' := uahp P P' w ( invweq w ) .
Definition weqpathsweqhProp { P P' : hProp } (w : weq P P'): paths (eqweqmaphProp (weqtopathshProp w)) w.
-Proof. intros. apply proofirrelevance . apply (isapropweqtoprop P P' (pr22 P')). Defined.
+Proof. intros. apply proofirrelevance . apply (isapropweqtoprop P P' (pr2 P')). Defined.
Theorem univfromtwoaxiomshProp (P P':hProp): isweq (@eqweqmaphProp P P').
@@ -197,10 +270,10 @@ Proof. intros.
set (P1:= fun XY: dirprod hProp hProp => (match XY with tpair X Y => paths X Y end)). set (P2:= fun XY: dirprod hProp hProp => match XY with tpair X Y => weq X Y end). set (Z1:= total2 P1). set (Z2:= total2 P2). set (f:= ( totalfun _ _ (fun XY: dirprod hProp hProp => (match XY with tpair X Y => @eqweqmaphProp X Y end))): Z1 -> Z2). set (g:= ( totalfun _ _ (fun XY: dirprod hProp hProp => (match XY with tpair X Y => @weqtopathshProp X Y end))): Z2 -> Z1). set (s1:= (fun X Y :hProp => fun w: weq X Y => tpair P2 ( dirprodpair X Y) w)). set (efg:= (fun a:_ => match a as a' return (paths (f (g a')) a') with tpair ( tpair X Y) w => ( maponpaths (s1 X Y) (@weqpathsweqhProp X Y w)) end)).
-set (h:= fun a1:Z1 => (pr21 ( pr21 a1))).
-assert (egf0: forall a1:Z1, paths ( pr21 (g (f a1))) ( pr21 a1)). intro. apply idpath.
-assert (egf1: forall a1 a1':Z1, paths ( pr21 a1') ( pr21 a1) -> paths a1' a1). intros ? ? X . set (X':= maponpaths ( @pr21 _ _ ) X).
-assert (is: isweq h). apply ( isweqpr21pr21). apply ( invmaponpathsweq ( weqpair h is ) _ _ X').
+set (h:= fun a1:Z1 => (pr1 ( pr1 a1))).
+assert (egf0: forall a1:Z1, paths ( pr1 (g (f a1))) ( pr1 a1)). intro. apply idpath.
+assert (egf1: forall a1 a1':Z1, paths ( pr1 a1') ( pr1 a1) -> paths a1' a1). intros ? ? X . set (X':= maponpaths ( @pr1 _ _ ) X).
+assert (is: isweq h). apply ( isweqpr1pr1 hProp ). apply ( invmaponpathsweq ( weqpair h is ) _ _ X').
set (egf:= fun a1:_ => (egf1 _ _ (egf0 a1))).
set (is2:= gradth _ _ egf efg).
apply ( isweqtotaltofib P1 P2 (fun XY: dirprod hProp hProp => (match XY with tpair X Y => @eqweqmaphProp X Y end)) is2 ( dirprodpair P P')). Defined.
@@ -208,9 +281,17 @@ apply ( isweqtotaltofib P1 P2 (fun XY: dirprod hProp hProp => (match XY with t
Definition weqeqweqhProp ( P P' : hProp ) := weqpair _ ( univfromtwoaxiomshProp P P' ) .
Corollary isasethProp : isaset hProp.
-Proof. unfold isaset. simpl. intros x x'. apply (isofhlevelweqb (S O) ( weqeqweqhProp x x' ) (isapropweqtoprop x x' (pr22 x'))). Defined.
+Proof. unfold isaset. simpl. intros x x'. apply (isofhlevelweqb (S O) ( weqeqweqhProp x x' ) (isapropweqtoprop x x' (pr2 x'))). Defined.
+
+
+Lemma iscontrtildehProp : iscontr tildehProp .
+Proof . split with ( tpair _ htrue tt ) . intro tP . destruct tP as [ P p ] . apply ( invmaponpathsincl _ ( isinclpr1 ( fun P : hProp => P ) ( fun P => pr2 P ) ) ) . simpl . apply uahp . apply ( fun x => tt ) . intro t. apply p . Defined .
+Lemma isaproptildehProp : isaprop tildehProp .
+Proof . apply ( isapropifcontr iscontrtildehProp ) . Defined .
+Lemma isasettildehProp : isaset tildehProp .
+Proof . apply ( isasetifcontr iscontrtildehProp ) . Defined .
View
1,878 hlevel2/algebra1.v
0 additions, 1,878 deletions not shown
View
1,007 hlevel2/algebra1a.v
@@ -0,0 +1,1007 @@
+(** * Algebra 1 . Part A . Generalities. Vladimir Voevodsky. Aug. 2011 - .
+
+*)
+
+
+
+(** ** Preambule *)
+
+(** Settings *)
+
+Add Rec LoadPath "../Generalities".
+Add Rec LoadPath "../hlevel1".
+Add Rec LoadPath "../hlevel2".
+
+Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *)
+
+
+(** Imports *)
+
+Require Export hSet .
+
+
+(** To upstream files *)
+
+
+
+(** ** Sets with one and two binary operations *)
+
+(** *** Binary operations *)
+
+(** **** General definitions *)
+
+Definition binop ( X : UU0 ) := X -> X -> X .
+
+Definition islcancelable { X : UU0 } ( opp : binop X ) ( x : X ) := isincl ( fun x0 : X => opp x x0 ) .
+
+Definition isrcancelable { X : UU0 } ( opp : binop X ) ( x : X ) := isincl ( fun x0 : X => opp x0 x ) .
+
+Definition iscancelable { X : UU0 } ( opp : binop X ) ( x : X ) := dirprod ( islcancelable opp x ) ( isrcancelable opp x ) .
+
+Definition islinvertible { X : UU0 } ( opp : binop X ) ( x : X ) := isweq ( fun x0 : X => opp x x0 ) .
+
+Definition isrinvertible { X : UU0 } ( opp : binop X ) ( x : X ) := isweq ( fun x0 : X => opp x0 x ) .
+
+Definition isinvertible { X : UU0 } ( opp : binop X ) ( x : X ) := dirprod ( islinvertible opp x ) ( isrinvertible opp x ) .
+
+
+
+(** **** Standard conditions on one binary operation on a set *)
+
+(** *)
+
+Definition isassoc { X : hSet} ( opp : binop X ) := forall x x' x'' , paths ( opp ( opp x x' ) x'' ) ( opp x ( opp x' x'' ) ) .
+
+Lemma isapropisassoc { X : hSet } ( opp : binop X ) : isaprop ( isassoc opp ) .
+Proof . intros . apply impred . intro x . apply impred . intro x' . apply impred . intro x'' . simpl . apply ( setproperty X ) . Defined .
+
+(** *)
+
+Definition islunit { X : hSet} ( opp : binop X ) ( un0 : X ) := forall x : X , paths ( opp un0 x ) x .
+
+Lemma isapropislunit { X : hSet} ( opp : binop X ) ( un0 : X ) : isaprop ( islunit opp un0 ) .
+Proof . intros . apply impred . intro x . simpl . apply ( setproperty X ) . Defined .
+
+Definition isrunit { X : hSet} ( opp : binop X ) ( un0 : X ) := forall x : X , paths ( opp x un0 ) x .
+
+Lemma isapropisrunit { X : hSet} ( opp : binop X ) ( un0 : X ) : isaprop ( isrunit opp un0 ) .
+Proof . intros . apply impred . intro x . simpl . apply ( setproperty X ) . Defined .
+
+Definition isunit { X : hSet} ( opp : binop X ) ( un0 : X ) := dirprod ( islunit opp un0 ) ( isrunit opp un0 ) .
+
+Definition isunital { X : hSet} ( opp : binop X ) := total2 ( fun un0 : X => isunit opp un0 ) .
+Definition isunitalpair { X : hSet } { opp : binop X } ( un0 : X ) ( is : isunit opp un0 ) : isunital opp := tpair _ un0 is .
+
+Lemma isapropisunital { X : hSet} ( opp : binop X ) : isaprop ( isunital opp ) .
+Proof . intros . apply ( @isapropsubtype X ( fun un0 : _ => hconj ( hProppair _ ( isapropislunit opp un0 ) ) ( hProppair _ ( isapropisrunit opp un0 ) ) ) ) . intros u1 u2 . intros ua1 ua2 . apply ( pathscomp0 ( pathsinv0 ( pr2 ua2 u1 ) ) ( pr1 ua1 u2 ) ) . Defined .
+
+
+(** *)
+
+Definition ismonoidop { X : hSet } ( opp : binop X ) := dirprod ( isassoc opp ) ( isunital opp ) .
+Definition assocax_is { X : hSet } { opp : binop X } : ismonoidop opp -> isassoc opp := @pr1 _ _ .
+Definition unel_is { X : hSet } { opp : binop X } ( is : ismonoidop opp ) : X := pr1 ( pr2 is ) .
+Definition lunax_is { X : hSet } { opp : binop X } ( is : ismonoidop opp ) := pr1 ( pr2 ( pr2 is ) ) .
+Definition runax_is { X : hSet } { opp : binop X } ( is : ismonoidop opp ) := pr2 ( pr2 ( pr2 is ) ) .
+
+
+Lemma isapropismonoidop { X : hSet } ( opp : binop X ) : isaprop ( ismonoidop opp ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply ( isapropisassoc ) . apply ( isapropisunital ) . Defined .
+
+
+
+(** *)
+
+Definition islinv { X : hSet } ( opp : binop X ) ( un0 : X ) ( inv0 : X -> X ) := forall x : X , paths ( opp ( inv0 x ) x ) un0 .
+
+Lemma isapropislinv { X : hSet } ( opp : binop X ) ( un0 : X ) ( inv0 : X -> X ) : isaprop ( islinv opp un0 inv0 ) .
+Proof . intros . apply impred . intro x . apply ( setproperty X (opp (inv0 x) x) un0 ) . Defined .
+
+Definition isrinv { X : hSet } ( opp : binop X ) ( un0 : X ) ( inv0 : X -> X ) := forall x : X , paths ( opp x ( inv0 x ) ) un0 .
+
+Lemma isapropisrinv { X : hSet } ( opp : binop X ) ( un0 : X ) ( inv0 : X -> X ) : isaprop ( isrinv opp un0 inv0 ) .
+Proof . intros . apply impred . intro x . apply ( setproperty X ) . Defined .
+
+Definition isinv { X : hSet } ( opp : binop X ) ( un0 : X ) ( inv0 : X -> X ) := dirprod ( islinv opp un0 inv0 ) ( isrinv opp un0 inv0 ) .
+
+Lemma isapropisinv { X : hSet } ( opp : binop X ) ( un0 : X ) ( inv0 : X -> X ) : isaprop ( isinv opp un0 inv0 ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply isapropislinv . apply isapropisrinv . Defined .
+
+Definition invstruct { X : hSet } ( opp : binop X ) ( is : ismonoidop opp ) := total2 ( fun inv0 : X -> X => isinv opp ( unel_is is ) inv0 ) .
+
+Definition isgrop { X : hSet } ( opp : binop X ) := total2 ( fun is : ismonoidop opp => invstruct opp is ) .
+Definition isgroppair { X : hSet } { opp : binop X } ( is1 : ismonoidop opp ) ( is2 : invstruct opp is1 ) : isgrop opp := tpair ( fun is : ismonoidop opp => invstruct opp is ) is1 is2 .
+Definition pr1isgrop ( X : hSet ) ( opp : binop X ) : isgrop opp -> ismonoidop opp := @pr1 _ _ .
+Coercion pr1isgrop : isgrop >-> ismonoidop .
+
+Definition grinv_is { X : hSet } { opp : binop X } ( is : isgrop opp ) : X -> X := pr1 ( pr2 is ) .
+
+Definition grlinvax_is { X : hSet } { opp : binop X } ( is : isgrop opp ) := pr1 ( pr2 ( pr2 is ) ) .
+
+Definition grrinvax_is { X : hSet } { opp : binop X } ( is : isgrop opp ) := pr2 ( pr2 ( pr2 is ) ) .
+
+
+Lemma isweqrmultingr_is { X : hSet } { opp : binop X } ( is : isgrop opp ) ( x0 : X ) : isrinvertible opp x0 .
+Proof . intros . destruct is as [ is istr ] . set ( f := fun x : X => opp x x0 ) . set ( g := fun x : X , opp x ( ( pr1 istr ) x0 ) ) . destruct is as [ assoc isun0 ] . destruct istr as [ inv0 axs ] . destruct isun0 as [ un0 unaxs ] . simpl in * |- .
+assert ( egf : forall x : _ , paths ( g ( f x ) ) x ) . intro x . unfold f . unfold g . destruct ( pathsinv0 ( assoc x x0 ( inv0 x0 ) ) ) . assert ( e := pr2 axs x0 ) . simpl in e . rewrite e . apply ( pr2 unaxs x ) .
+assert ( efg : forall x : _ , paths ( f ( g x ) ) x ) . intro x . unfold f . unfold g . destruct ( pathsinv0 ( assoc x ( inv0 x0 ) x0 ) ) . assert ( e := pr1 axs x0 ) . simpl in e . rewrite e . apply ( pr2 unaxs x ) .
+apply ( gradth _ _ egf efg ) . Defined .
+
+Lemma isweqlmultingr_is { X : hSet } { opp : binop X } ( is : isgrop opp ) ( x0 : X ) : islinvertible opp x0 .
+Proof . intros . destruct is as [ is istr ] . set ( f := fun x : X => opp x0 x ) . set ( g := fun x : X , opp ( ( pr1 istr ) x0 ) x ) . destruct is as [ assoc isun0 ] . destruct istr as [ inv0 axs ] . destruct isun0 as [ un0 unaxs ] . simpl in * |- .
+assert ( egf : forall x : _ , paths ( g ( f x ) ) x ) . intro x . unfold f . unfold g . destruct ( assoc ( inv0 x0 ) x0 x ) . assert ( e := pr1 axs x0 ) . simpl in e . rewrite e . apply ( pr1 unaxs x ) .
+assert ( efg : forall x : _ , paths ( f ( g x ) ) x ) . intro x . unfold f . unfold g . destruct ( assoc x0 ( inv0 x0 ) x ) . assert ( e := pr2 axs x0 ) . simpl in e . rewrite e . apply ( pr1 unaxs x ) .
+apply ( gradth _ _ egf efg ) . Defined .
+
+
+Lemma isapropinvstruct { X : hSet } { opp : binop X } ( is : ismonoidop opp ) : isaprop ( invstruct opp is ) .
+Proof . intros . apply isofhlevelsn . intro is0 . set ( un0 := pr1 ( pr2 is ) ) . assert ( int : forall i : X -> X , isaprop ( dirprod ( forall x : X , paths ( opp ( i x ) x ) un0 ) ( forall x : X , paths ( opp x ( i x ) ) un0 ) ) ) . intro i . apply ( isofhleveldirprod 1 ) . apply impred . intro x . simpl . apply ( setproperty X ) . apply impred . intro x . simpl . apply ( setproperty X ) . apply ( isapropsubtype ( fun i : _ => hProppair _ ( int i ) ) ) . intros inv1 inv2 . simpl . intro ax1 . intro ax2 . apply funextfun . intro x0 . apply ( invmaponpathsweq ( weqpair _ ( isweqrmultingr_is ( tpair _ is is0 ) x0 ) ) ) . simpl . rewrite ( pr1 ax1 x0 ) . rewrite ( pr1 ax2 x0 ) . apply idpath . Defined .
+
+Lemma isapropisgrop { X : hSet } ( opp : binop X ) : isaprop ( isgrop opp ) .
+Proof . intros . apply ( isofhleveltotal2 1 ) . apply isapropismonoidop . apply isapropinvstruct . Defined .
+
+(* (** Unitary monoid where all elements are invertible is a group *)
+
+Definition allinvvertibleinv { X : hSet } { opp : binop X } ( is : ismonoidop opp ) ( allinv : forall x : X , islinvertible opp x ) : X -> X := fun x : X => invmap ( weqpair _ ( allinv x ) ) ( unel_is is ) .
+
+*)
+
+
+(** The following lemma is an analog of [ Bourbaki , Alg. 1 , ex. 2 , p. 132 ] *)
+
+Lemma isgropif { X : hSet } { opp : binop X } ( is0 : ismonoidop opp ) ( is : forall x : X, hexists ( fun x0 : X => eqset ( opp x x0 ) ( unel_is is0 ) ) ) : isgrop opp .
+Proof . intros . split with is0 . destruct is0 as [ assoc isun0 ] . destruct isun0 as [ un0 unaxs0 ] . simpl in is . simpl in unaxs0 . simpl in un0 . simpl in assoc . simpl in unaxs0 .
+
+assert ( l1 : forall x' : X , isincl ( fun x0 : X => opp x0 x' ) ) . intro x' . apply ( @hinhuniv ( total2 ( fun x0 : X => paths ( opp x' x0 ) un0 ) ) ( hProppair _ ( isapropisincl ( fun x0 : X => opp x0 x' ) ) ) ) . intro int1 . simpl . apply isinclbetweensets . apply ( pr2 X ) . apply ( pr2 X ) . intros a b . intro e . rewrite ( pathsinv0 ( pr2 unaxs0 a ) ) . rewrite ( pathsinv0 ( pr2 unaxs0 b ) ) . destruct int1 as [ invx' eq ] . rewrite ( pathsinv0 eq ) . destruct ( assoc a x' invx' ) . destruct ( assoc b x' invx' ) . rewrite e . apply idpath . apply ( is x' ) .
+
+assert ( is' : forall x : X, hexists ( fun x0 : X => eqset ( opp x0 x ) un0 ) ) . intro x . apply ( fun f : _ => hinhuniv f ( is x ) ) . intro s1 . destruct s1 as [ x' eq ] . apply hinhpr . split with x' . simpl . apply ( invmaponpathsincl _ ( l1 x' ) ) . rewrite ( assoc x' x x' ) . rewrite eq . rewrite ( pr1 unaxs0 x' ) . unfold unel_is. simpl . rewrite ( pr2 unaxs0 x' ) . apply idpath .
+
+assert ( l1' : forall x' : X , isincl ( fun x0 : X => opp x' x0 ) ) . intro x' . apply ( @hinhuniv ( total2 ( fun x0 : X => paths ( opp x0 x' ) un0 ) ) ( hProppair _ ( isapropisincl ( fun x0 : X => opp x' x0 ) ) ) ) . intro int1 . simpl . apply isinclbetweensets . apply ( pr2 X ) . apply ( pr2 X ) . intros a b . intro e . rewrite ( pathsinv0 ( pr1 unaxs0 a ) ) . rewrite ( pathsinv0 ( pr1 unaxs0 b ) ) . destruct int1 as [ invx' eq ] . rewrite ( pathsinv0 eq ) . destruct ( pathsinv0 ( assoc invx' x' a ) ) . destruct ( pathsinv0 ( assoc invx' x' b ) ) . rewrite e . apply idpath . apply ( is' x' ) .
+
+assert ( int : forall x : X , isaprop ( total2 ( fun x0 : X => eqset ( opp x0 x ) un0 ) ) ) . intro x . apply isapropsubtype . intros x1 x2 . intros eq1 eq2 . apply ( invmaponpathsincl _ ( l1 x ) ) . rewrite eq1 . rewrite eq2 . apply idpath .
+
+simpl . set ( linv0 := fun x : X => hinhunivcor1 ( hProppair _ ( int x ) ) ( is' x ) ) . simpl in linv0 . set ( inv0 := fun x : X => pr1 ( linv0 x ) ) . split with inv0 . simpl . split with ( fun x : _ => pr2 ( linv0 x ) ) . intro x . apply ( invmaponpathsincl _ ( l1 x ) ) . rewrite ( assoc x ( inv0 x ) x ) . change ( inv0 x ) with ( pr1 ( linv0 x ) ) . rewrite ( pr2 ( linv0 x ) ) . unfold unel_is . simpl . rewrite ( pr1 unaxs0 x ) . rewrite ( pr2 unaxs0 x ) . apply idpath . Defined .
+
+
+
+(** *)
+
+Definition iscomm { X : hSet} ( opp : binop X ) := forall x x' : X , paths ( opp x x' ) ( opp x' x ) .
+
+Lemma isapropiscomm { X : hSet } ( opp : binop X ) : isaprop ( iscomm opp ) .
+Proof . intros . apply impred . intros x . apply impred . intro x' . simpl . apply ( setproperty X ) . Defined .
+
+Definition isabmonoidop { X : hSet } ( opp : binop X ) := dirprod ( ismonoidop opp ) ( iscomm opp ) .
+Definition pr1isabmonoidop ( X : hSet ) ( opp : binop X ) : isabmonoidop opp -> ismonoidop opp := @pr1 _ _ .
+Coercion pr1isabmonoidop : isabmonoidop >-> ismonoidop .
+
+Definition commax_is { X : hSet} { opp : binop X } ( is : isabmonoidop opp ) : iscomm opp := pr2 is .
+
+Lemma isapropisabmonoidop { X : hSet } ( opp : binop X ) : isaprop ( isabmonoidop opp ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply isapropismonoidop . apply isapropiscomm . Defined .
+
+Lemma abmonoidoprer { X : hSet } { opp : binop X } ( is : isabmonoidop opp ) ( a b c d : X ) : paths ( opp ( opp a b ) ( opp c d ) ) ( opp ( opp a c ) ( opp b d ) ) .
+Proof . intros . destruct is as [ is comm ] . destruct is as [ assoc unital0 ] . simpl in * . destruct ( assoc ( opp a b ) c d ) . destruct ( assoc ( opp a c ) b d ) . destruct ( pathsinv0 ( assoc a b c ) ) . destruct ( pathsinv0 ( assoc a c b ) ) . destruct ( comm b c ) . apply idpath . Defined .
+
+
+
+
+(** *)
+
+
+Lemma weqlcancelablercancelable { X : hSet } ( opp : binop X ) ( is : iscomm opp ) ( x : X ) : weq ( islcancelable opp x ) ( isrcancelable opp x ) .
+Proof . intros .
+
+assert ( f : ( islcancelable opp x ) -> ( isrcancelable opp x ) ) . unfold islcancelable . unfold isrcancelable . intro isl . apply ( fun h : _ => isinclhomot _ _ h isl ) . intro x0 . apply is .
+assert ( g : ( isrcancelable opp x ) -> ( islcancelable opp x ) ) . unfold islcancelable . unfold isrcancelable . intro isr . apply ( fun h : _ => isinclhomot _ _ h isr ) . intro x0 . apply is .
+
+split with f . apply ( isweqimplimpl f g ( isapropisincl ( fun x0 : X => opp x x0 ) ) ( isapropisincl ( fun x0 : X => opp x0 x ) ) ) . Defined .
+
+
+
+Lemma weqlinvertiblerinvertible { X : hSet } ( opp : binop X ) ( is : iscomm opp ) ( x : X ) : weq ( islinvertible opp x ) ( isrinvertible opp x ) .
+Proof . intros .
+
+assert ( f : ( islinvertible opp x ) -> ( isrinvertible opp x ) ) . unfold islinvertible . unfold isrinvertible . intro isl . apply ( fun h : _ => isweqhomot _ _ h isl ) . apply is .
+assert ( g : ( isrinvertible opp x ) -> ( islinvertible opp x ) ) . unfold islinvertible . unfold isrinvertible . intro isr . apply ( fun h : _ => isweqhomot _ _ h isr ) . intro x0 . apply is .
+
+split with f . apply ( isweqimplimpl f g ( isapropisweq ( fun x0 : X => opp x x0 ) ) ( isapropisweq ( fun x0 : X => opp x0 x ) ) ) . Defined .
+
+
+Lemma weqlunitrunit { X : hSet } ( opp : binop X ) ( is : iscomm opp ) ( un0 : X ) : weq ( islunit opp un0 ) ( isrunit opp un0 ) .
+Proof . intros .
+
+assert ( f : ( islunit opp un0 ) -> ( isrunit opp un0 ) ) . unfold islunit . unfold isrunit . intro isl . intro x . destruct ( is un0 x ) . apply ( isl x ) .
+assert ( g : ( isrunit opp un0 ) -> ( islunit opp un0 ) ) . unfold islunit . unfold isrunit . intro isr . intro x . destruct ( is x un0 ) . apply ( isr x ) .
+
+split with f . apply ( isweqimplimpl f g ( isapropislunit opp un0 ) ( isapropisrunit opp un0 ) ) . Defined .
+
+
+Lemma weqlinvrinv { X : hSet } ( opp : binop X ) ( is : iscomm opp ) ( un0 : X ) ( inv0 : X -> X ) : weq ( islinv opp un0 inv0 ) ( isrinv opp un0 inv0 ) .
+Proof . intros .
+
+assert ( f : ( islinv opp un0 inv0 ) -> ( isrinv opp un0 inv0 ) ) . unfold islinv . unfold isrinv . intro isl . intro x . destruct ( is ( inv0 x ) x ) . apply ( isl x ) .
+assert ( g : ( isrinv opp un0 inv0 ) -> ( islinv opp un0 inv0 ) ) . unfold islinv . unfold isrinv . intro isr . intro x . destruct ( is x ( inv0 x ) ) . apply ( isr x ) .
+
+split with f . apply ( isweqimplimpl f g ( isapropislinv opp un0 inv0 ) ( isapropisrinv opp un0 inv0 ) ) . Defined .
+
+
+Opaque abmonoidoprer .
+
+
+(** *)
+
+Definition isabgrop { X : hSet } ( opp : binop X ) := dirprod ( isgrop opp ) ( iscomm opp ) .
+Definition pr1isabgrop ( X : hSet ) ( opp : binop X ) : isabgrop opp -> isgrop opp := @pr1 _ _ .
+Coercion pr1isabgrop : isabgrop >-> isgrop .
+
+Definition isabgroptoisabmonoidop ( X : hSet ) ( opp : binop X ) : isabgrop opp -> isabmonoidop opp := fun is : _ => dirprodpair ( pr1 ( pr1 is ) ) ( pr2 is ) .
+Coercion isabgroptoisabmonoidop : isabgrop >-> isabmonoidop .
+
+Lemma isapropisabgrop { X : hSet } ( opp : binop X ) : isaprop ( isabgrop opp ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply isapropisgrop . apply isapropiscomm . Defined .
+
+
+
+
+
+
+
+
+(** **** Standard conditions on a pair of binary operations on a set *)
+
+(** *)
+
+Definition isldistr { X : hSet} ( opp1 opp2 : binop X ) := forall x x' x'' : X , paths ( opp2 x'' ( opp1 x x' ) ) ( opp1 ( opp2 x'' x ) ( opp2 x'' x' ) ) .
+
+Lemma isapropisldistr { X : hSet} ( opp1 opp2 : binop X ) : isaprop ( isldistr opp1 opp2 ) .
+Proof . intros . apply impred . intro x . apply impred . intro x' . apply impred . intro x'' . simpl . apply ( setproperty X ) . Defined .
+
+Definition isrdistr { X : hSet} ( opp1 opp2 : binop X ) := forall x x' x'' : X , paths ( opp2 ( opp1 x x' ) x'' ) ( opp1 ( opp2 x x'' ) ( opp2 x' x'' ) ) .
+
+Lemma isapropisrdistr { X : hSet} ( opp1 opp2 : binop X ) : isaprop ( isrdistr opp1 opp2 ) .
+Proof . intros . apply impred . intro x . apply impred . intro x' . apply impred . intro x'' . simpl . apply ( setproperty X ) . Defined .
+
+Definition isdistr { X : hSet } ( opp1 opp2 : binop X ) := dirprod ( isldistr opp1 opp2 ) ( isrdistr opp1 opp2 ) .
+
+Lemma isapropisdistr { X : hSet } ( opp1 opp2 : binop X ) : isaprop ( isdistr opp1 opp2 ) .
+Proof . intros . apply ( isofhleveldirprod 1 _ _ ( isapropisldistr _ _ ) ( isapropisrdistr _ _ ) ) . Defined .
+
+(** *)
+
+Lemma weqldistrrdistr { X : hSet} ( opp1 opp2 : binop X ) ( is : iscomm opp2 ) : weq ( isldistr opp1 opp2 ) ( isrdistr opp1 opp2 ) .
+Proof . intros .
+
+assert ( f : ( isldistr opp1 opp2 ) -> ( isrdistr opp1 opp2 ) ) . unfold isldistr . unfold isrdistr . intro isl . intros x x' x'' . destruct ( is x'' ( opp1 x x' ) ) . destruct ( is x'' x ) . destruct ( is x'' x' ) . apply ( isl x x' x'' ) .
+assert ( g : ( isrdistr opp1 opp2 ) -> ( isldistr opp1 opp2 ) ) . unfold isldistr . unfold isrdistr . intro isr . intros x x' x'' . destruct ( is ( opp1 x x' ) x'' ) . destruct ( is x x'' ) . destruct ( is x' x'' ) . apply ( isr x x' x'' ) .
+
+split with f . apply ( isweqimplimpl f g ( isapropisldistr opp1 opp2 ) ( isapropisrdistr opp1 opp2 ) ) . Defined .
+
+
+(** *)
+
+
+Definition isrigops { X : hSet } ( opp1 opp2 : binop X ) := dirprod ( total2 ( fun axs : dirprod ( isabmonoidop opp1 ) ( ismonoidop opp2 ) => ( dirprod ( forall x : X , paths ( opp2 ( unel_is ( pr1 axs ) ) x ) ( unel_is ( pr1 axs ) ) ) ) ( forall x : X , paths ( opp2 x ( unel_is ( pr1 axs ) ) ) ( unel_is ( pr1 axs ) ) ) ) ) ( isdistr opp1 opp2 ) .
+
+Definition rigop1axs_is { X : hSet } { opp1 opp2 : binop X } : isrigops opp1 opp2 -> isabmonoidop opp1 := fun is : _ => pr1 ( pr1 ( pr1 is ) ) .
+Definition rigop2axs_is { X : hSet } { opp1 opp2 : binop X } : isrigops opp1 opp2 -> ismonoidop opp2 := fun is : _ => pr2 ( pr1 ( pr1 is ) ) .
+Definition rigdistraxs_is { X : hSet } { opp1 opp2 : binop X } : isrigops opp1 opp2 -> isdistr opp1 opp2 := fun is : _ => pr2 is .
+Definition rigldistrax_is { X : hSet } { opp1 opp2 : binop X } : isrigops opp1 opp2 -> isldistr opp1 opp2 := fun is : _ => pr1 ( pr2 is ) .
+Definition rigrdistrax_is { X : hSet } { opp1 opp2 : binop X } : isrigops opp1 opp2 -> isrdistr opp1 opp2 := fun is : _ => pr2 ( pr2 is ) .
+Definition rigunel1_is { X : hSet } { opp1 opp2 : binop X } ( is : isrigops opp1 opp2 ) : X := pr1 (pr2 (pr1 (rigop1axs_is is))) .
+Definition rigunel2_is { X : hSet } { opp1 opp2 : binop X } ( is : isrigops opp1 opp2 ) : X := (pr1 (pr2 (rigop2axs_is is))) .
+Definition rigmult0x_is { X : hSet } { opp1 opp2 : binop X } ( is : isrigops opp1 opp2 ) ( x : X ) : paths ( opp2 ( rigunel1_is is ) x ) ( rigunel1_is is ) := pr1 ( pr2 ( pr1 is ) ) x .
+Definition rigmultx0_is { X : hSet } { opp1 opp2 : binop X } ( is : isrigops opp1 opp2 ) ( x : X ) : paths ( opp2 x ( rigunel1_is is ) ) ( rigunel1_is is ) := pr2 ( pr2 ( pr1 is ) ) x .
+
+
+Lemma isapropisrigops { X : hSet } ( opp1 opp2 : binop X ) : isaprop ( isrigops opp1 opp2 ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply ( isofhleveltotal2 1 ) . apply ( isofhleveldirprod 1 ) . apply isapropisabmonoidop . apply isapropismonoidop. intro x . apply ( isofhleveldirprod 1 ) . apply impred. intro x' . apply ( setproperty X ) . apply impred . intro x' . apply ( setproperty X ) . apply isapropisdistr . Defined .
+
+
+
+
+(** *)
+
+
+Definition isrngops { X : hSet } ( opp1 opp2 : binop X ) := dirprod ( dirprod ( isabgrop opp1 ) ( ismonoidop opp2 ) ) ( isdistr opp1 opp2 ) .
+
+Definition rngop1axs_is { X : hSet } { opp1 opp2 : binop X } : isrngops opp1 opp2 -> isabgrop opp1 := fun is : _ => pr1 ( pr1 is ) .
+Definition rngop2axs_is { X : hSet } { opp1 opp2 : binop X } : isrngops opp1 opp2 -> ismonoidop opp2 := fun is : _ => pr2 ( pr1 is ) .
+Definition rngdistraxs_is { X : hSet } { opp1 opp2 : binop X } : isrngops opp1 opp2 -> isdistr opp1 opp2 := fun is : _ => pr2 is .
+Definition rngldistrax_is { X : hSet } { opp1 opp2 : binop X } : isrngops opp1 opp2 -> isldistr opp1 opp2 := fun is : _ => pr1 ( pr2 is ) .
+Definition rngrdistrax_is { X : hSet } { opp1 opp2 : binop X } : isrngops opp1 opp2 -> isrdistr opp1 opp2 := fun is : _ => pr2 ( pr2 is ) .
+Definition rngunel1_is { X : hSet } { opp1 opp2 : binop X } ( is : isrngops opp1 opp2 ) : X := unel_is ( pr1 ( pr1 is ) ) .
+Definition rngunel2_is { X : hSet } { opp1 opp2 : binop X } ( is : isrngops opp1 opp2 ) : X := unel_is ( pr2 ( pr1 is ) ) .
+
+
+Lemma isapropisrngops { X : hSet } ( opp1 opp2 : binop X ) : isaprop ( isrngops opp1 opp2 ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply ( isofhleveldirprod 1 ) . apply isapropisabgrop . apply isapropismonoidop. apply isapropisdistr . Defined .
+
+Lemma multx0_is_l { X : hSet } { opp1 opp2 : binop X } ( is1 : isgrop opp1 ) ( is2 : ismonoidop opp2 ) ( is12 : isdistr opp1 opp2 ) : forall x : X , paths ( opp2 x ( unel_is ( pr1 is1 ) ) ) ( unel_is ( pr1 is1 ) ) .
+Proof . intros . destruct is12 as [ ldistr0 rdistr0 ] . destruct is2 as [ assoc2 [ un2 [ lun2 run2 ] ] ] . simpl in * . apply ( invmaponpathsweq ( weqpair _ ( isweqrmultingr_is is1 ( opp2 x un2 ) ) ) ) . simpl . destruct is1 as [ [ assoc1 [ un1 [ lun1 run1 ] ] ] [ inv0 [ linv0 rinv0 ] ] ] . unfold unel_is . simpl in * . rewrite ( lun1 ( opp2 x un2 ) ) . destruct ( ldistr0 un1 un2 x ) . rewrite ( run2 x ) . rewrite ( lun1 un2 ) . rewrite ( run2 x ) . apply idpath . Defined .
+
+Opaque multx0_is_l .
+
+Lemma mult0x_is_l { X : hSet } { opp1 opp2 : binop X } ( is1 : isgrop opp1 ) ( is2 : ismonoidop opp2 ) ( is12 : isdistr opp1 opp2 ) : forall x : X , paths ( opp2 ( unel_is ( pr1 is1 ) ) x ) ( unel_is ( pr1 is1 ) ) .
+Proof . intros . destruct is12 as [ ldistr0 rdistr0 ] . destruct is2 as [ assoc2 [ un2 [ lun2 run2 ] ] ] . simpl in * . apply ( invmaponpathsweq ( weqpair _ ( isweqrmultingr_is is1 ( opp2 un2 x ) ) ) ) . simpl . destruct is1 as [ [ assoc1 [ un1 [ lun1 run1 ] ] ] [ inv0 [ linv0 rinv0 ] ] ] . unfold unel_is . simpl in * . rewrite ( lun1 ( opp2 un2 x ) ) . destruct ( rdistr0 un1 un2 x ) . rewrite ( lun2 x ) . rewrite ( lun1 un2 ) . rewrite ( lun2 x ) . apply idpath . Defined .
+
+Opaque mult0x_is_l .
+
+
+
+Definition minus1_is_l { X : hSet } { opp1 opp2 : binop X } ( is1 : isgrop opp1 ) ( is2 : ismonoidop opp2 ) := ( grinv_is is1 ) ( unel_is is2 ) .
+
+Lemma islinvmultwithminus1_is_l { X : hSet } { opp1 opp2 : binop X } ( is1 : isgrop opp1 ) ( is2 : ismonoidop opp2 ) ( is12 : isdistr opp1 opp2 ) ( x : X ) : paths ( opp1 ( opp2 ( minus1_is_l is1 is2 ) x ) x ) ( unel_is ( pr1 is1 ) ) .
+Proof . intros . set ( xinv := opp2 (minus1_is_l is1 is2) x ) . rewrite ( pathsinv0 ( lunax_is is2 x ) ) . unfold xinv . rewrite ( pathsinv0 ( pr2 is12 _ _ x ) ) . unfold minus1_is_l . unfold grinv_is . rewrite ( grlinvax_is is1 _ ) . apply mult0x_is_l . apply is2 . apply is12 . Defined .
+
+Opaque islinvmultwithminus1_is_l .
+
+Lemma isrinvmultwithminus1_is_l { X : hSet } { opp1 opp2 : binop X } ( is1 : isgrop opp1 ) ( is2 : ismonoidop opp2 ) ( is12 : isdistr opp1 opp2 ) ( x : X ) : paths ( opp1 x ( opp2 ( minus1_is_l is1 is2 ) x ) ) ( unel_is ( pr1 is1 ) ) .
+Proof . intros . set ( xinv := opp2 (minus1_is_l is1 is2) x ) . rewrite ( pathsinv0 ( lunax_is is2 x ) ) . unfold xinv . rewrite ( pathsinv0 ( pr2 is12 _ _ x ) ) . unfold minus1_is_l . unfold grinv_is . rewrite ( grrinvax_is is1 _ ) . apply mult0x_is_l . apply is2 . apply is12 . Defined .
+
+Opaque isrinvmultwithminus1_is_l .
+
+
+Lemma isminusmultwithminus1_is_l { X : hSet } { opp1 opp2 : binop X } ( is1 : isgrop opp1 ) ( is2 : ismonoidop opp2 ) ( is12 : isdistr opp1 opp2 ) ( x : X ) : paths ( opp2 ( minus1_is_l is1 is2 ) x ) ( grinv_is is1 x ) .
+Proof . intros . apply ( invmaponpathsweq ( weqpair _ ( isweqrmultingr_is is1 x ) ) ) . simpl . rewrite ( islinvmultwithminus1_is_l is1 is2 is12 x ) . unfold grinv_is . rewrite ( grlinvax_is is1 x ) . apply idpath . Defined .
+
+Opaque isminusmultwithminus1_is_l .
+
+Lemma isrngopsif { X : hSet } { opp1 opp2 : binop X } ( is1 : isgrop opp1 ) ( is2 : ismonoidop opp2 ) ( is12 : isdistr opp1 opp2 ) : isrngops opp1 opp2 .
+Proof . intros . set ( assoc1 := pr1 ( pr1 is1 ) ) . split . split . split with is1 .
+intros x y . apply ( invmaponpathsweq ( weqpair _ ( isweqrmultingr_is is1 ( opp2 ( minus1_is_l is1 is2 ) ( opp1 x y ) ) ) ) ) . simpl . rewrite ( isrinvmultwithminus1_is_l is1 is2 is12 ( opp1 x y ) ) . rewrite ( pr1 is12 x y _ ) . destruct ( assoc1 ( opp1 y x ) (opp2 (minus1_is_l is1 is2) x) (opp2 (minus1_is_l is1 is2) y)) . rewrite ( assoc1 y x _ ) . destruct ( pathsinv0 ( isrinvmultwithminus1_is_l is1 is2 is12 x ) ) . unfold unel_is . rewrite ( runax_is ( pr1 is1 ) y ) . rewrite ( isrinvmultwithminus1_is_l is1 is2 is12 y ) . apply idpath . apply is2 . apply is12 . Defined .
+
+Definition rngmultx0_is { X : hSet } { opp1 opp2 : binop X } ( is : isrngops opp1 opp2 ) := multx0_is_l ( rngop1axs_is is ) ( rngop2axs_is is ) ( rngdistraxs_is is ) .
+
+Definition rngmult0x_is { X : hSet } { opp1 opp2 : binop X } ( is : isrngops opp1 opp2 ) := mult0x_is_l ( rngop1axs_is is ) ( rngop2axs_is is ) ( rngdistraxs_is is ) .
+
+Definition rngminus1_is { X : hSet } { opp1 opp2 : binop X } ( is : isrngops opp1 opp2 ) := minus1_is_l ( rngop1axs_is is ) ( rngop2axs_is is ) .
+
+Definition rngmultwithminus1_is { X : hSet } { opp1 opp2 : binop X } ( is : isrngops opp1 opp2 ) := isminusmultwithminus1_is_l ( rngop1axs_is is ) ( rngop2axs_is is ) ( rngdistraxs_is is ) .
+
+Definition isrngopstoisrigops ( X : hSet ) ( opp1 opp2 : binop X ) ( is : isrngops opp1 opp2 ) : isrigops opp1 opp2 .
+Proof. intros . split . split with ( dirprodpair ( isabgroptoisabmonoidop _ _ ( rngop1axs_is is ) ) ( rngop2axs_is is ) ) . split . simpl . apply ( rngmult0x_is ) . simpl . apply ( rngmultx0_is ) . apply ( rngdistraxs_is is ) . Defined .
+
+Coercion isrngopstoisrigops : isrngops >-> isrigops .
+
+
+
+(** *)
+
+Definition iscommrigops { X : hSet } ( opp1 opp2 : binop X ) := dirprod ( isrigops opp1 opp2 ) ( iscomm opp2 ) .
+Definition pr1iscommrigops ( X : hSet ) ( opp1 opp2 : binop X ) : iscommrigops opp1 opp2 -> isrigops opp1 opp2 := @pr1 _ _ .
+Coercion pr1iscommrigops : iscommrigops >-> isrigops .
+
+Definition rigiscommop2_is { X : hSet } { opp1 opp2 : binop X } ( is : iscommrigops opp1 opp2 ) : iscomm opp2 := pr2 is .
+
+Lemma isapropiscommrig { X : hSet } ( opp1 opp2 : binop X ) : isaprop ( iscommrigops opp1 opp2 ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply isapropisrigops . apply isapropiscomm . Defined .
+
+
+
+
+
+
+(** *)
+
+Definition iscommrngops { X : hSet } ( opp1 opp2 : binop X ) := dirprod ( isrngops opp1 opp2 ) ( iscomm opp2 ) .
+Definition pr1iscommrngops ( X : hSet ) ( opp1 opp2 : binop X ) : iscommrngops opp1 opp2 -> isrngops opp1 opp2 := @pr1 _ _ .
+Coercion pr1iscommrngops : iscommrngops >-> isrngops .
+
+Definition rngiscommop2_is { X : hSet } { opp1 opp2 : binop X } ( is : iscommrngops opp1 opp2 ) : iscomm opp2 := pr2 is .
+
+Lemma isapropiscommrng { X : hSet } ( opp1 opp2 : binop X ) : isaprop ( iscommrngops opp1 opp2 ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply isapropisrngops . apply isapropiscomm . Defined .
+
+Definition iscommrngopstoiscommrigops ( X : hSet ) ( opp1 opp2 : binop X ) ( is : iscommrngops opp1 opp2 ) : iscommrigops opp1 opp2 := dirprodpair ( isrngopstoisrigops _ _ _ ( pr1 is ) ) ( pr2 is ) .
+Coercion iscommrngopstoiscommrigops : iscommrngops >-> iscommrigops .
+
+
+
+
+(** *** Sets with one binary operation *)
+
+(** **** General definitions *)
+
+
+Definition setwithbinop := total2 ( fun X : hSet => binop X ) .
+Definition setwithbinoppair ( X : hSet ) ( opp : binop X ) : setwithbinop := tpair ( fun X : hSet => binop X ) X opp .
+Definition pr1setwithbinop : setwithbinop -> hSet := @pr1 _ ( fun X : hSet => binop X ) .
+Coercion pr1setwithbinop : setwithbinop >-> hSet .
+
+
+Definition op { X : setwithbinop } : binop X := pr2 X .
+
+Notation "x + y" := ( op x y ) : addoperation_scope .
+Notation "x * y" := ( op x y ) : multoperation_scope .
+
+
+
+(** **** Functions compatible with a binary operation ( homomorphisms ) and their properties *)
+
+Definition isbinopfun { X Y : setwithbinop } ( f : X -> Y ) := forall x x' : X , paths ( f ( op x x' ) ) ( op ( f x ) ( f x' ) ) .
+
+Lemma isapropisbinopfun { X Y : setwithbinop } ( f : X -> Y ) : isaprop ( isbinopfun f ) .
+Proof . intros . apply impred . intro x . apply impred . intro x' . apply ( setproperty Y ) . Defined .
+
+Definition binopfun ( X Y : setwithbinop ) : UU0 := total2 ( fun f : X -> Y => isbinopfun f ) .
+Definition binopfunpair { X Y : setwithbinop } ( f : X -> Y ) ( is : isbinopfun f ) : binopfun X Y := tpair _ f is .
+Definition pr1binopfun ( X Y : setwithbinop ) : binopfun X Y -> ( X -> Y ) := @pr1 _ _ .
+Coercion pr1binopfun : binopfun >-> Funclass .
+
+Lemma isasetbinopfun ( X Y : setwithbinop ) : isaset ( binopfun X Y ) .
+Proof . intros . apply ( isasetsubset ( pr1binopfun X Y ) ) . change ( isofhlevel 2 ( X -> Y ) ) . apply impred . intro . apply ( setproperty Y ) . apply isinclpr1 . intro . apply isapropisbinopfun . Defined .
+
+Lemma isbinopfuncomp { X Y Z : setwithbinop } ( f : binopfun X Y ) ( g : binopfun Y Z ) : isbinopfun ( funcomp ( pr1 f ) ( pr1 g ) ) .
+Proof . intros . set ( axf := pr2 f ) . set ( axg := pr2 g ) . intros a b . unfold funcomp . rewrite ( axf a b ) . rewrite ( axg ( pr1 f a ) ( pr1 f b ) ) . apply idpath . Defined .
+
+Opaque isbinopfuncomp .
+
+Definition binopfuncomp { X Y Z : setwithbinop } ( f : binopfun X Y ) ( g : binopfun Y Z ) : binopfun X Z := binopfunpair ( funcomp ( pr1 f ) ( pr1 g ) ) ( isbinopfuncomp f g ) .
+
+
+Definition binopmono ( X Y : setwithbinop ) : UU0 := total2 ( fun f : incl X Y => isbinopfun ( pr1 f ) ) .
+Definition binopmonopair { X Y : setwithbinop } ( f : incl X Y ) ( is : isbinopfun f ) : binopmono X Y := tpair _ f is .
+Definition pr1binopmono ( X Y : setwithbinop ) : binopmono X Y -> incl X Y := @pr1 _ _ .
+Coercion pr1binopmono : binopmono >-> incl .
+
+Definition binopincltobinopfun ( X Y : setwithbinop ) : binopmono X Y -> binopfun X Y := fun f => binopfunpair ( pr1 ( pr1 f ) ) ( pr2 f ) .
+Coercion binopincltobinopfun : binopmono >-> binopfun .
+
+
+Definition binopmonocomp { X Y Z : setwithbinop } ( f : binopmono X Y ) ( g : binopmono Y Z ) : binopmono X Z := binopmonopair ( inclcomp ( pr1 f ) ( pr1 g ) ) ( isbinopfuncomp f g ) .
+
+Definition binopiso ( X Y : setwithbinop ) : UU0 := total2 ( fun f : weq X Y => isbinopfun f ) .
+Definition binopisopair { X Y : setwithbinop } ( f : weq X Y ) ( is : isbinopfun f ) : binopiso X Y := tpair _ f is .
+Definition pr1binopiso ( X Y : setwithbinop ) : binopiso X Y -> weq X Y := @pr1 _ _ .
+Coercion pr1binopiso : binopiso >-> weq .
+
+Definition binopisotobinopmono ( X Y : setwithbinop ) : binopiso X Y -> binopmono X Y := fun f => binopmonopair ( pr1 f ) ( pr2 f ) .
+Coercion binopisotobinopmono : binopiso >-> binopmono .
+
+Definition binopisocomp { X Y Z : setwithbinop } ( f : binopiso X Y ) ( g : binopiso Y Z ) : binopiso X Z := binopisopair ( weqcomp ( pr1 f ) ( pr1 g ) ) ( isbinopfuncomp f g ) .
+
+Lemma isbinopfuninvmap { X Y : setwithbinop } ( f : binopiso X Y ) : isbinopfun ( invmap ( pr1 f ) ) .
+Proof . intros . set ( axf := pr2 f ) . intros a b . apply ( invmaponpathsweq ( pr1 f ) ) . rewrite ( homotweqinvweq ( pr1 f ) ( op a b ) ) . rewrite ( axf (invmap (pr1 f) a) (invmap (pr1 f) b) ) . rewrite ( homotweqinvweq ( pr1 f ) a ) . rewrite ( homotweqinvweq ( pr1 f ) b ) . apply idpath . Defined .
+
+Opaque isbinopfuninvmap .
+
+Definition invbinopiso { X Y : setwithbinop } ( f : binopiso X Y ) : binopiso Y X := binopisopair ( invweq ( pr1 f ) ) ( isbinopfuninvmap f ) .
+
+
+
+(** **** Transport of properties of a binary operation *)
+
+
+Lemma isincltwooutof3a { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( isg : isincl g ) ( isgf : isincl ( funcomp f g ) ) : isincl f .
+Proof . intros . apply ( isofhlevelff 1 f g isgf ) . apply ( isofhlevelfsnincl 1 g isg ) . Defined .
+
+
+Lemma islcancelablemonob { X Y : setwithbinop } ( f : binopmono X Y ) ( x : X ) ( is : islcancelable ( @op Y ) ( f x ) ) : islcancelable ( @op X ) x .
+Proof . intros . unfold islcancelable . apply ( isincltwooutof3a (fun x0 : X => op x x0) f ( pr2 ( pr1 f ) ) ) .
+
+assert ( h : homot ( funcomp f ( fun y0 : Y => op ( f x ) y0 ) ) (funcomp (fun x0 : X => op x x0) f) ) . intro x0 . unfold funcomp . apply ( pathsinv0 ( ( pr2 f ) x x0 ) ) .
+
+apply ( isinclhomot _ _ h ) . apply ( isinclcomp f ( inclpair _ is ) ) . Defined .
+
+
+Lemma isrcancelablemonob { X Y : setwithbinop } ( f : binopmono X Y ) ( x : X ) ( is : isrcancelable ( @op Y ) ( f x ) ) : isrcancelable ( @op X ) x .
+Proof . intros . unfold islcancelable . apply ( isincltwooutof3a (fun x0 : X => op x0 x) f ( pr2 ( pr1 f ) ) ) .
+
+assert ( h : homot ( funcomp f ( fun y0 : Y => op y0 ( f x ) ) ) (funcomp (fun x0 : X => op x0 x ) f) ) . intro x0 . unfold funcomp . apply ( pathsinv0 ( ( pr2 f ) x0 x ) ) .
+
+apply ( isinclhomot _ _ h ) . apply ( isinclcomp f ( inclpair _ is ) ) . Defined .
+
+
+Lemma iscancelablemonob { X Y : setwithbinop } ( f : binopmono X Y ) ( x : X ) ( is : iscancelable ( @op Y ) ( f x ) ) : iscancelable ( @op X ) x .
+Proof . intros . apply ( dirprodpair ( islcancelablemonob f x ( pr1 is ) ) ( isrcancelablemonob f x ( pr2 is ) ) ) . Defined .
+
+Notation islcancelableisob := islcancelablemonob .
+Notation isrcancelableisob := isrcancelablemonob .
+Notation iscancelableisob := iscancelablemonob .
+
+
+Lemma islinvertibleisob { X Y : setwithbinop } ( f : binopiso X Y ) ( x : X ) ( is : islinvertible ( @op Y ) ( f x ) ) : islinvertible ( @op X ) x .
+Proof . intros . unfold islinvertible . apply ( twooutof3a (fun x0 : X => op x x0) f ) .
+
+assert ( h : homot ( funcomp f ( fun y0 : Y => op ( f x ) y0 ) ) (funcomp (fun x0 : X => op x x0) f) ) . intro x0 . unfold funcomp . apply ( pathsinv0 ( ( pr2 f ) x x0 ) ) .
+
+apply ( isweqhomot _ _ h ) . apply ( pr2 ( weqcomp f ( weqpair _ is ) ) ) . apply ( pr2 ( pr1 f ) ) . Defined .
+
+Lemma isrinvertibleisob { X Y : setwithbinop } ( f : binopiso X Y ) ( x : X ) ( is : isrinvertible ( @op Y ) ( f x ) ) : isrinvertible ( @op X ) x .
+Proof . intros . unfold islinvertible . apply ( twooutof3a (fun x0 : X => op x0 x) f ) .
+
+assert ( h : homot ( funcomp f ( fun y0 : Y => op y0 ( f x ) ) ) (funcomp (fun x0 : X => op x0 x ) f) ) . intro x0 . unfold funcomp . apply ( pathsinv0 ( ( pr2 f ) x0 x ) ) .
+
+apply ( isweqhomot _ _ h ) . apply ( pr2 ( weqcomp f ( weqpair _ is ) ) ) . apply ( pr2 ( pr1 f ) ) . Defined .
+
+
+Lemma isinvertiblemonob { X Y : setwithbinop } ( f : binopiso X Y ) ( x : X ) ( is : isinvertible ( @op Y ) ( f x ) ) : isinvertible ( @op X ) x .
+Proof . intros . apply ( dirprodpair ( islinvertibleisob f x ( pr1 is ) ) ( isrinvertibleisob f x ( pr2 is ) ) ) . Defined .
+
+
+Definition islinvertibleisof { X Y : setwithbinop } ( f : binopiso X Y ) ( x : X ) ( is : islinvertible ( @op X ) x ) : islinvertible ( @op Y ) ( f x ) .
+Proof . intros . unfold islinvertible . apply ( twooutof3b f ) . apply ( pr2 ( pr1 f ) ) .
+
+assert ( h : homot ( funcomp ( fun x0 : X => op x x0 ) f ) (fun x0 : X => op (f x) (f x0)) ) . intro x0 . unfold funcomp . apply ( pr2 f x x0 ) .
+
+apply ( isweqhomot _ _ h ) . apply ( pr2 ( weqcomp ( weqpair _ is ) f ) ) . Defined .
+
+Definition isrinvertibleisof { X Y : setwithbinop } ( f : binopiso X Y ) ( x : X ) ( is : isrinvertible ( @op X ) x ) : isrinvertible ( @op Y ) ( f x ) .
+Proof . intros . unfold isrinvertible . apply ( twooutof3b f ) . apply ( pr2 ( pr1 f ) ) .
+
+assert ( h : homot ( funcomp ( fun x0 : X => op x0 x ) f ) (fun x0 : X => op (f x0) (f x) ) ) . intro x0 . unfold funcomp . apply ( pr2 f x0 x ) .
+
+apply ( isweqhomot _ _ h ) . apply ( pr2 ( weqcomp ( weqpair _ is ) f ) ) . Defined .
+
+Lemma isinvertiblemonof { X Y : setwithbinop } ( f : binopiso X Y ) ( x : X ) ( is : isinvertible ( @op X ) x ) : isinvertible ( @op Y ) ( f x ) .
+Proof . intros . apply ( dirprodpair ( islinvertibleisof f x ( pr1 is ) ) ( isrinvertibleisof f x ( pr2 is ) ) ) . Defined .
+
+
+Lemma isassocmonob { X Y : setwithbinop } ( f : binopmono X Y ) ( is : isassoc ( @op Y ) ) : isassoc ( @op X ) .
+Proof . intros . set ( axf := pr2 f ) . simpl in axf . intros a b c . apply ( invmaponpathsincl _ ( pr2 ( pr1 f ) ) ) . rewrite ( axf ( op a b ) c ) . rewrite ( axf a b ) . rewrite ( axf a ( op b c ) ) . rewrite ( axf b c ) . apply is . Defined .
+
+Opaque isassocmonob .
+
+Lemma iscommmonob { X Y : setwithbinop } ( f : binopmono X Y ) ( is : iscomm ( @op Y ) ) : iscomm ( @op X ) .
+Proof . intros . set ( axf := pr2 f ) . simpl in axf . intros a b . apply ( invmaponpathsincl _ ( pr2 ( pr1 f ) ) ) . rewrite ( axf a b ) . rewrite ( axf b a ) . apply is . Defined .
+
+Opaque iscommmonob .
+
+Notation isassocisob := isassocmonob .
+Notation iscommisob := iscommmonob .
+
+Lemma isassocisof { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isassoc ( @op X ) ) : isassoc ( @op Y ) .
+Proof . intros . apply ( isassocmonob ( invbinopiso f ) is ) . Defined .
+
+Opaque isassocisof .
+
+Lemma iscommisof { X Y : setwithbinop } ( f : binopiso X Y ) ( is : iscomm ( @op X ) ) : iscomm ( @op Y ) .
+Proof . intros . apply ( iscommmonob ( invbinopiso f ) is ) . Defined .
+
+Opaque iscommisof .
+
+Lemma isunitisof { X Y : setwithbinop } ( f : binopiso X Y ) ( unx : X ) ( is : isunit ( @op X ) unx ) : isunit ( @op Y ) ( f unx ) .
+Proof . intros . set ( axf := pr2 f ) . split .
+
+intro a . change ( f unx ) with ( pr1 f unx ) . apply ( invmaponpathsweq ( pr1 ( invbinopiso f ) ) ) . rewrite ( pr2 ( invbinopiso f ) ( pr1 f unx ) a ) . simpl . rewrite ( homotinvweqweq ( pr1 f ) unx ) . apply ( pr1 is ) .
+
+intro a . change ( f unx ) with ( pr1 f unx ) . apply ( invmaponpathsweq ( pr1 ( invbinopiso f ) ) ) . rewrite ( pr2 ( invbinopiso f ) a ( pr1 f unx ) ) . simpl . rewrite ( homotinvweqweq ( pr1 f ) unx ) . apply ( pr2 is ) . Defined .
+
+Opaque isunitisof .
+
+Definition isunitalisof { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isunital ( @op X ) ) : isunital ( @op Y ) := isunitalpair ( f ( pr1 is ) ) ( isunitisof f ( pr1 is ) ( pr2 is ) ) .
+
+Lemma isunitisob { X Y : setwithbinop } ( f : binopiso X Y ) ( uny : Y ) ( is : isunit ( @op Y ) uny ) : isunit ( @op X ) ( ( invmap f ) uny ) .
+Proof . intros . set ( int := isunitisof ( invbinopiso f ) ) . simpl . simpl in int . apply int . apply is . Defined .
+
+Opaque isunitisob .
+
+Definition isunitalisob { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isunital ( @op Y ) ) : isunital ( @op X ) := isunitalpair ( ( invmap f ) ( pr1 is ) ) ( isunitisob f ( pr1 is ) ( pr2 is ) ) .
+
+
+Definition ismonoidopisof { X Y : setwithbinop } ( f : binopiso X Y ) ( is : ismonoidop ( @op X ) ) : ismonoidop ( @op Y ) := dirprodpair ( isassocisof f ( pr1 is ) ) ( isunitalisof f ( pr2 is ) ) .
+
+Definition ismonoidopisob { X Y : setwithbinop } ( f : binopiso X Y ) ( is : ismonoidop ( @op Y ) ) : ismonoidop ( @op X ) := dirprodpair ( isassocisob f ( pr1 is ) ) ( isunitalisob f ( pr2 is ) ) .
+
+Lemma isinvisof { X Y : setwithbinop } ( f : binopiso X Y ) ( unx : X ) ( invx : X -> X ) ( is : isinv ( @op X ) unx invx ) : isinv ( @op Y ) ( pr1 f unx ) ( funcomp ( invmap ( pr1 f ) ) ( funcomp invx ( pr1 f ) ) ) .
+Proof . intros . set ( axf := pr2 f ) . set ( axinvf := pr2 ( invbinopiso f ) ) . simpl in axf . simpl in axinvf . unfold funcomp . split .
+
+intro a . apply ( invmaponpathsweq ( pr1 ( invbinopiso f ) ) ) . simpl . rewrite ( axinvf ( ( pr1 f ) (invx (invmap ( pr1 f ) a))) a ) . rewrite ( homotinvweqweq ( pr1 f ) unx ) . rewrite ( homotinvweqweq ( pr1 f ) (invx (invmap ( pr1 f ) a)) ) . apply ( pr1 is ) .
+
+intro a . apply ( invmaponpathsweq ( pr1 ( invbinopiso f ) ) ) . simpl . rewrite ( axinvf a ( ( pr1 f ) (invx (invmap ( pr1 f ) a))) ) . rewrite ( homotinvweqweq ( pr1 f ) unx ) . rewrite ( homotinvweqweq ( pr1 f ) (invx (invmap ( pr1 f ) a)) ) . apply ( pr2 is ) . Defined .
+
+Opaque isinvisof .
+
+Definition isgropisof { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isgrop ( @op X ) ) : isgrop ( @op Y ) := tpair _ ( ismonoidopisof f is ) ( tpair _ ( funcomp ( invmap ( pr1 f ) ) ( funcomp ( grinv_is is ) ( pr1 f ) ) ) ( isinvisof f ( unel_is is ) ( grinv_is is ) ( pr2 ( pr2 is ) ) ) ) .
+
+Lemma isinvisob { X Y : setwithbinop } ( f : binopiso X Y ) ( uny : Y ) ( invy : Y -> Y ) ( is : isinv ( @op Y ) uny invy ) : isinv ( @op X ) ( invmap ( pr1 f ) uny ) ( funcomp ( pr1 f ) ( funcomp invy ( invmap ( pr1 f ) ) ) ) .
+Proof . intros . apply ( isinvisof ( invbinopiso f ) uny invy is ) . Defined .
+
+Opaque isinvisob .
+
+Definition isgropisob { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isgrop ( @op Y ) ) : isgrop ( @op X ) := tpair _ ( ismonoidopisob f is ) ( tpair _ ( funcomp ( pr1 f ) ( funcomp ( grinv_is is ) ( invmap ( pr1 f ) ) ) ) ( isinvisob f ( unel_is is ) ( grinv_is is ) ( pr2 ( pr2 is ) ) ) ) .
+
+Definition isabmonoidopisof { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isabmonoidop ( @op X ) ) : isabmonoidop ( @op Y ) := tpair _ ( ismonoidopisof f is ) ( iscommisof f ( commax_is is ) ) .
+
+Definition isabmonoidopisob { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isabmonoidop ( @op Y ) ) : isabmonoidop ( @op X ) := tpair _ ( ismonoidopisob f is ) ( iscommisob f ( commax_is is ) ) .
+
+
+Definition isabgropisof { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isabgrop ( @op X ) ) : isabgrop ( @op Y ) := tpair _ ( isgropisof f is ) ( iscommisof f ( commax_is is ) ) .
+
+Definition isabgropisob { X Y : setwithbinop } ( f : binopiso X Y ) ( is : isabgrop ( @op Y ) ) : isabgrop ( @op X ) := tpair _ ( isgropisob f is ) ( iscommisob f ( commax_is is ) ) .
+
+
+
+
+
+
+
+(** **** Subobjects *)
+
+Definition issubsetwithbinop { X : hSet } ( opp : binop X ) ( A : hsubtypes X ) := forall a a' : A , A ( opp ( pr1 a ) ( pr1 a' ) ) .
+
+Lemma isapropissubsetwithbinop { X : hSet } ( opp : binop X ) ( A : hsubtypes X ) : isaprop ( issubsetwithbinop opp A ) .
+Proof . intros . apply impred . intro a . apply impred . intros a' . apply ( pr2 ( A ( opp (pr1 a) (pr1 a')) ) ) . Defined .
+
+Definition subsetswithbinop { X : setwithbinop } := total2 ( fun A : hsubtypes X => issubsetwithbinop ( @op X ) A ) .
+Definition subsetswithbinoppair { X : setwithbinop } := tpair ( fun A : hsubtypes X => issubsetwithbinop ( @op X ) A ) .
+Definition subsetswithbinopconstr { X : setwithbinop } := @subsetswithbinoppair X .
+Definition pr1subsetswithbinop ( X : setwithbinop ) : @subsetswithbinop X -> hsubtypes X := @pr1 _ ( fun A : hsubtypes X => issubsetwithbinop ( @op X ) A ) .
+Coercion pr1subsetswithbinop : subsetswithbinop >-> hsubtypes .
+
+Definition totalsubsetwithbinop ( X : setwithbinop ) : @subsetswithbinop X .
+Proof . intros . split with ( fun x : X => htrue ) . intros x x' . apply tt . Defined .
+
+
+Definition carrierofasubsetwithbinop { X : setwithbinop } ( A : @subsetswithbinop X ) : setwithbinop .
+Proof . intros . set ( aset := ( hSetpair ( carrier A ) ( isasetsubset ( pr1carrier A ) ( setproperty X ) ( isinclpr1carrier A ) ) ) : hSet ) . split with aset .
+set ( subopp := ( fun a a' : A => carrierpair A ( op ( pr1carrier _ a ) ( pr1carrier _ a' ) ) ( pr2 A a a' ) ) : ( A -> A -> A ) ) . simpl . unfold binop . apply subopp . Defined .
+
+Coercion carrierofasubsetwithbinop : subsetswithbinop >-> setwithbinop .
+
+
+
+
+
+
+(** **** Relations compatible with a binary operation and quotient objects *)
+
+Definition isbinophrel { X : setwithbinop } ( R : hrel X ) := dirprod ( forall a b c : X , R a b -> R ( op c a ) ( op c b ) ) ( forall a b c : X , R a b -> R ( op a c ) ( op b c ) ) .
+
+Definition isbinophrellogeqf { X : setwithbinop } { L R : hrel X } ( lg : hrellogeq L R ) ( isl : isbinophrel L ) : isbinophrel R .
+Proof . intros . split . intros a b c rab . apply ( ( pr1 ( lg _ _ ) ( ( pr1 isl ) _ _ _ ( pr2 ( lg _ _ ) rab ) ) ) ) . intros a b c rab . apply ( ( pr1 ( lg _ _ ) ( ( pr2 isl ) _ _ _ ( pr2 ( lg _ _ ) rab ) ) ) ) . Defined .
+
+Lemma isapropisbinophrel { X : setwithbinop } ( R : hrel X ) : isaprop ( isbinophrel R ) .
+Proof . intros . apply isapropdirprod . apply impred . intro a . apply impred . intro b . apply impred . intro c . apply impred . intro r . apply ( pr2 ( R _ _ ) ) . apply impred . intro a . apply impred . intro b . apply impred . intro c . apply impred . intro r . apply ( pr2 ( R _ _ ) ) . Defined .
+
+Lemma isbinophrelif { X : setwithbinop } ( R : hrel X ) ( is : iscomm ( @op X ) ) ( isl : forall a b c : X , R a b -> R ( op c a ) ( op c b ) ) : isbinophrel R .
+Proof . intros . split with isl . intros a b c rab . destruct ( is c a ) . destruct ( is c b ) . apply ( isl _ _ _ rab ) . Defined .
+
+Lemma iscompbinoptransrel { X : setwithbinop } ( R : hrel X ) ( ist : istrans R ) ( isb : isbinophrel R ) : iscomprelrelfun2 R R ( @op X ) .
+Proof . intros . intros a b c d . intros rab rcd . set ( racbc := pr2 isb a b c rab ) . set ( rbcbd := pr1 isb c d b rcd ) . apply ( ist _ _ _ racbc rbcbd ) . Defined .
+
+Lemma isbinopreflrel { X : setwithbinop } ( R : hrel X ) ( isr : isrefl R ) ( isb : iscomprelrelfun2 R R ( @op X ) ) : isbinophrel R .
+Proof . intros . split . intros a b c rab . apply ( isb c c a b ( isr c ) rab ) . intros a b c rab . apply ( isb a b c c rab ( isr c ) ) . Defined .
+
+
+Definition binophrel { X : setwithbinop } := total2 ( fun R : hrel X => isbinophrel R ) .
+Definition binophrelpair { X : setwithbinop } := tpair ( fun R : hrel X => isbinophrel R ) .
+Definition pr1binophrel ( X : setwithbinop ) : @binophrel X -> hrel X := @pr1 _ ( fun R : hrel X => isbinophrel R ) .
+Coercion pr1binophrel : binophrel >-> hrel .
+
+Definition binoppo { X : setwithbinop } := total2 ( fun R : po X => isbinophrel R ) .
+Definition binoppopair { X : setwithbinop } := tpair ( fun R : po X => isbinophrel R ) .
+Definition pr1binoppo ( X : setwithbinop ) : @binoppo X -> po X := @pr1 _ ( fun R : po X => isbinophrel R ) .
+Coercion pr1binoppo : binoppo >-> po .
+
+Definition binopeqrel { X : setwithbinop } := total2 ( fun R : eqrel X => isbinophrel R ) .
+Definition binopeqrelpair { X : setwithbinop } := tpair ( fun R : eqrel X => isbinophrel R ) .
+Definition pr1binopeqrel ( X : setwithbinop ) : @binopeqrel X -> eqrel X := @pr1 _ ( fun R : eqrel X => isbinophrel R ) .
+Coercion pr1binopeqrel : binopeqrel >-> eqrel .
+
+Definition setwithbinopquot { X : setwithbinop } ( R : @binopeqrel X ) : setwithbinop .
+Proof . intros . split with ( setquotinset R ) . set ( qt := setquot R ) . set ( qtset := setquotinset R ) .
+assert ( iscomp : iscomprelrelfun2 R R op ) . apply ( iscompbinoptransrel R ( eqreltrans R ) ( pr2 R ) ) .
+set ( qtmlt := setquotfun2 R R op iscomp ) . simpl . unfold binop . apply qtmlt . Defined .
+
+
+Definition ispartbinophrel { X : setwithbinop } ( S : hsubtypes X ) ( R : hrel X ) := dirprod ( forall a b c : X , S c -> R a b -> R ( op c a ) ( op c b ) ) ( forall a b c : X , S c -> R a b -> R ( op a c ) ( op b c ) ) .
+
+Definition isbinoptoispartbinop { X : setwithbinop } ( S : hsubtypes X ) ( L : hrel X ) ( is : isbinophrel L ) : ispartbinophrel S L .
+Proof . intros X S L . unfold isbinophrel . unfold ispartbinophrel . intro d2 . split . intros a b c is . apply ( pr1 d2 a b c ) . intros a b c is . apply ( pr2 d2 a b c ) . Defined .
+
+Definition ispartbinophrellogeqf { X : setwithbinop } ( S : hsubtypes X ) { L R : hrel X } ( lg : hrellogeq L R ) ( isl : ispartbinophrel S L ) : ispartbinophrel S R .
+Proof . intros . split . intros a b c is rab . apply ( ( pr1 ( lg _ _ ) ( ( pr1 isl ) _ _ _ is ( pr2 ( lg _ _ ) rab ) ) ) ) . intros a b c is rab . apply ( ( pr1 ( lg _ _ ) ( ( pr2 isl ) _ _ _ is ( pr2 ( lg _ _ ) rab ) ) ) ) . Defined .
+
+Lemma ispartbinophrelif { X : setwithbinop } ( S : hsubtypes X ) ( R : hrel X ) ( is : iscomm ( @op X ) ) ( isl : forall a b c : X , S c -> R a b -> R ( op c a ) ( op c b ) ) : ispartbinophrel S R .
+Proof . intros . split with isl . intros a b c s rab . destruct ( is c a ) . destruct ( is c b ) . apply ( isl _ _ _ s rab ) . Defined .
+
+
+
+(** **** Relations inversely compatible with a binary operation *)
+
+Definition isinvbinophrel { X : setwithbinop } ( R : hrel X ) := dirprod ( forall a b c : X , R ( op c a ) ( op c b ) -> R a b ) ( forall a b c : X , R ( op a c ) ( op b c ) -> R a b ) .
+
+Definition isinvbinophrellogeqf { X : setwithbinop } { L R : hrel X } ( lg : hrellogeq L R ) ( isl : isinvbinophrel L ) : isinvbinophrel R .
+Proof . intros . split . intros a b c rab . apply ( ( pr1 ( lg _ _ ) ( ( pr1 isl ) _ _ _ ( pr2 ( lg _ _ ) rab ) ) ) ) . intros a b c rab . apply ( ( pr1 ( lg _ _ ) ( ( pr2 isl ) _ _ _ ( pr2 ( lg _ _ ) rab ) ) ) ) . Defined .
+
+Lemma isapropisinvbinophrel { X : setwithbinop } ( R : hrel X ) : isaprop ( isinvbinophrel R ) .
+Proof . intros . apply isapropdirprod . apply impred . intro a . apply impred . intro b . apply impred . intro c . apply impred . intro r . apply ( pr2 ( R _ _ ) ) . apply impred . intro a . apply impred . intro b . apply impred . intro c . apply impred . intro r . apply ( pr2 ( R _ _ ) ) . Defined .
+
+Lemma isinvbinophrelif { X : setwithbinop } ( R : hrel X ) ( is : iscomm ( @op X ) ) ( isl : forall a b c : X , R ( op c a ) ( op c b ) -> R a b ) : isinvbinophrel R .
+Proof . intros . split with isl . intros a b c rab . destruct ( is c a ) . destruct ( is c b ) . apply ( isl _ _ _ rab ) . Defined .
+
+
+
+
+
+Definition ispartinvbinophrel { X : setwithbinop } ( S : hsubtypes X ) ( R : hrel X ) := dirprod ( forall a b c : X , S c -> R ( op c a ) ( op c b ) -> R a b ) ( forall a b c : X , S c -> R ( op a c ) ( op b c ) -> R a b ) .
+
+Definition isinvbinoptoispartinvbinop { X : setwithbinop } ( S : hsubtypes X ) ( L : hrel X ) ( is : isinvbinophrel L ) : ispartinvbinophrel S L .
+Proof . intros X S L . unfold isinvbinophrel . unfold ispartinvbinophrel . intro d2 . split . intros a b c s . apply ( pr1 d2 a b c ) . intros a b c s . apply ( pr2 d2 a b c ) . Defined .
+
+Definition ispartinvbinophrellogeqf { X : setwithbinop } ( S : hsubtypes X ) { L R : hrel X } ( lg : hrellogeq L R ) ( isl : ispartinvbinophrel S L ) : ispartinvbinophrel S R .
+Proof . intros . split . intros a b c s rab . apply ( ( pr1 ( lg _ _ ) ( ( pr1 isl ) _ _ _ s ( pr2 ( lg _ _ ) rab ) ) ) ) . intros a b c s rab . apply ( ( pr1 ( lg _ _ ) ( ( pr2 isl ) _ _ _ s ( pr2 ( lg _ _ ) rab ) ) ) ) . Defined .
+
+Lemma ispartinvbinophrelif { X : setwithbinop } ( S : hsubtypes X ) ( R : hrel X ) ( is : iscomm ( @op X ) ) ( isl : forall a b c : X , S c -> R ( op c a ) ( op c b ) -> R a b ) : ispartinvbinophrel S R .
+Proof . intros . split with isl . intros a b c s rab . destruct ( is c a ) . destruct ( is c b ) . apply ( isl _ _ _ s rab ) . Defined .
+
+
+(** **** Homomorphisms and relations *)
+
+Lemma binophrelandfun { X Y : setwithbinop } ( f : binopfun X Y ) ( R : hrel Y ) ( is : @isbinophrel Y R ) : @isbinophrel X ( fun x x' => R ( f x ) ( f x' ) ) .
+Proof . intros . set ( ish := ( pr2 f ) : forall a0 b0 , paths ( f ( op a0 b0 ) ) ( op ( f a0 ) ( f b0 ) ) ) . split .
+
+intros a b c r . rewrite ( ish _ _ ) . rewrite ( ish _ _ ) . apply ( pr1 is ) . apply r .
+
+intros a b c r . rewrite ( ish _ _ ) . rewrite ( ish _ _ ) . apply ( pr2 is ) . apply r . Defined .
+
+
+Lemma ispartbinophrelandfun { X Y : setwithbinop } ( f : binopfun X Y ) ( SX : hsubtypes X ) ( SY : hsubtypes Y ) ( iss : forall x : X , ( SX x ) -> ( SY ( f x ) ) ) ( R : hrel Y ) ( is : @ispartbinophrel Y SY R ) : @ispartbinophrel X SX ( fun x x' => R ( f x ) ( f x' ) ) .
+Proof . intros . set ( ish := ( pr2 f ) : forall a0 b0 , paths ( f ( op a0 b0 ) ) ( op ( f a0 ) ( f b0 ) ) ) . split .
+
+intros a b c s r . rewrite ( ish _ _ ) . rewrite ( ish _ _ ) . apply ( ( pr1 is ) _ _ _ ( iss _ s ) r ) .
+
+intros a b c s r . rewrite ( ish _ _ ) . rewrite ( ish _ _ ) . apply ( ( pr2 is ) _ _ _ ( iss _ s ) r ) . Defined .
+
+Lemma invbinophrelandfun { X Y : setwithbinop } ( f : binopfun X Y ) ( R : hrel Y ) ( is : @isinvbinophrel Y R ) : @isinvbinophrel X ( fun x x' => R ( f x ) ( f x' ) ) .
+Proof . intros . set ( ish := ( pr2 f ) : forall a0 b0 , paths ( f ( op a0 b0 ) ) ( op ( f a0 ) ( f b0 ) ) ) . split .
+
+intros a b c r . rewrite ( ish _ _ ) in r . rewrite ( ish _ _ ) in r . apply ( ( pr1 is ) _ _ _ r ) .
+
+intros a b c r . rewrite ( ish _ _ ) in r . rewrite ( ish _ _ ) in r . apply ( ( pr2 is ) _ _ _ r ) . Defined .
+
+
+Lemma ispartinvbinophrelandfun { X Y : setwithbinop } ( f : binopfun X Y ) ( SX : hsubtypes X ) ( SY : hsubtypes Y ) ( iss : forall x : X , ( SX x ) -> ( SY ( f x ) ) ) ( R : hrel Y ) ( is : @ispartinvbinophrel Y SY R ) : @ispartinvbinophrel X SX ( fun x x' => R ( f x ) ( f x' ) ) .
+Proof . intros . set ( ish := ( pr2 f ) : forall a0 b0 , paths ( f ( op a0 b0 ) ) ( op ( f a0 ) ( f b0 ) ) ) . split .
+
+intros a b c s r . rewrite ( ish _ _ ) in r . rewrite ( ish _ _ ) in r . apply ( ( pr1 is ) _ _ _ ( iss _ s ) r ) .
+
+intros a b c s r . rewrite ( ish _ _ ) in r . rewrite ( ish _ _ ) in r . apply ( ( pr2 is ) _ _ _ ( iss _ s ) r ) . Defined .
+
+
+(** **** Quotient relations *)
+
+Lemma isbinopquotrel { X : setwithbinop } ( R : @binopeqrel X ) { L : hrel X } ( is : iscomprelrel R L ) ( isl : isbinophrel L ) : @isbinophrel ( setwithbinopquot R ) ( quotrel is ) .
+Proof . intros . unfold isbinophrel . split . assert ( int : forall a b c : setwithbinopquot R , isaprop ( quotrel is a b -> quotrel is (op c a ) (op c b ) ) ) . intros a b c . apply impred . intro . apply ( pr2 ( quotrel is _ _ ) ) . apply ( setquotuniv3prop R ( fun a b c => hProppair _ ( int a b c ) ) ) . exact ( pr1 isl ) .
+ assert ( int : forall a b c : setwithbinopquot R , isaprop ( quotrel is a b -> quotrel is (op a c ) (op b c ) ) ) . intros a b c . apply impred . intro . apply ( pr2 ( quotrel is _ _ ) ) . apply ( setquotuniv3prop R ( fun a b c => hProppair _ ( int a b c ) ) ) . exact ( pr2 isl ) . Defined .
+
+
+
+(** **** Direct products *)
+
+Definition setwithbinopdirprod ( X Y : setwithbinop ) : setwithbinop .
+Proof . intros . split with ( setdirprod X Y ) . unfold binop . simpl . apply ( fun xy xy' : _ => dirprodpair ( op ( pr1 xy ) ( pr1 xy' ) ) ( op ( pr2 xy ) ( pr2 xy' ) ) ) . Defined .
+
+
+
+
+
+
+(** *** Sets with two binary operations *)
+
+(** **** General definitions *)
+
+
+Definition setwith2binop := total2 ( fun X : hSet => dirprod ( binop X ) ( binop X ) ) .
+Definition setwith2binoppair ( X : hSet ) ( opps : dirprod ( binop X ) ( binop X ) ) : setwith2binop := tpair ( fun X : hSet => dirprod ( binop X ) ( binop X ) ) X opps .
+Definition pr1setwith2binop : setwith2binop -> hSet := @pr1 _ ( fun X : hSet => dirprod ( binop X ) ( binop X ) ) .
+Coercion pr1setwith2binop : setwith2binop >-> hSet .
+
+Definition op1 { X : setwith2binop } : binop X := pr1 ( pr2 X ) .
+Definition op2 { X : setwith2binop } : binop X := pr2 ( pr2 X ) .
+
+Definition setwithbinop1 ( X : setwith2binop ) : setwithbinop := setwithbinoppair ( pr1 X ) ( @op1 X ) .
+Definition setwithbinop2 ( X : setwith2binop ) : setwithbinop := setwithbinoppair ( pr1 X ) ( @op2 X ) .
+
+Notation "x + y" := ( op1 x y ) : twobinops_scope .
+Notation "x * y" := ( op2 x y ) : twobinops_scope .
+
+
+(** **** Functions compatible with a pair of binary operation ( homomorphisms ) and their properties *)
+
+Definition istwobinopfun { X Y : setwith2binop } ( f : X -> Y ) := dirprod ( forall x x' : X , paths ( f ( op1 x x' ) ) ( op1 ( f x ) ( f x' ) ) ) ( forall x x' : X , paths ( f ( op2 x x' ) ) ( op2 ( f x ) ( f x' ) ) ) .
+
+Lemma isapropistwobinopfun { X Y : setwith2binop } ( f : X -> Y ) : isaprop ( istwobinopfun f ) .
+Proof . intros . apply isofhleveldirprod . apply impred . intro x . apply impred . intro x' . apply ( setproperty Y ) . apply impred . intro x . apply impred . intro x' . apply ( setproperty Y ) . Defined .
+
+Definition twobinopfun ( X Y : setwith2binop ) : UU0 := total2 ( fun f : X -> Y => istwobinopfun f ) .
+Definition twobinopfunpair { X Y : setwith2binop } ( f : X -> Y ) ( is : istwobinopfun f ) : twobinopfun X Y := tpair _ f is .
+Definition pr1twobinopfun ( X Y : setwith2binop ) : twobinopfun X Y -> ( X -> Y ) := @pr1 _ _ .
+Coercion pr1twobinopfun : twobinopfun >-> Funclass .
+
+Definition binop1fun { X Y : setwith2binop } ( f : twobinopfun X Y ) : binopfun ( setwithbinop1 X ) ( setwithbinop1 Y ) := @binopfunpair ( setwithbinop1 X ) ( setwithbinop1 Y ) ( pr1 f ) ( pr1 ( pr2 f ) ) .
+
+Definition binop2fun { X Y : setwith2binop } ( f : twobinopfun X Y ) : binopfun ( setwithbinop2 X ) ( setwithbinop2 Y ) := @binopfunpair ( setwithbinop2 X ) ( setwithbinop2 Y ) ( pr1 f ) ( pr2 ( pr2 f ) ) .
+Lemma isasettwobinopfun ( X Y : setwith2binop ) : isaset ( twobinopfun X Y ) .
+Proof . intros . apply ( isasetsubset ( pr1twobinopfun X Y ) ) . change ( isofhlevel 2 ( X -> Y ) ) . apply impred . intro . apply ( setproperty Y ) . apply isinclpr1 . intro . apply isapropistwobinopfun . Defined .
+
+
+Lemma istwobinopfuncomp { X Y Z : setwith2binop } ( f : twobinopfun X Y ) ( g : twobinopfun Y Z ) : istwobinopfun ( funcomp ( pr1 f ) ( pr1 g ) ) .
+Proof . intros . set ( ax1f := pr1 ( pr2 f ) ) . set ( ax2f := pr2 ( pr2 f ) ) . set ( ax1g := pr1 ( pr2 g ) ) . set ( ax2g := pr2 ( pr2 g ) ) . split.
+
+intros a b . unfold funcomp . rewrite ( ax1f a b ) . rewrite ( ax1g ( pr1 f a ) ( pr1 f b ) ) . apply idpath .
+intros a b . unfold funcomp . rewrite ( ax2f a b ) . rewrite ( ax2g ( pr1 f a ) ( pr1 f b ) ) . apply idpath . Defined .
+
+Opaque istwobinopfuncomp .
+
+Definition twobinopfuncomp { X Y Z : setwith2binop } ( f : twobinopfun X Y ) ( g : twobinopfun Y Z ) : twobinopfun X Z := twobinopfunpair ( funcomp ( pr1 f ) ( pr1 g ) ) ( istwobinopfuncomp f g ) .
+
+
+Definition twobinopmono ( X Y : setwith2binop ) : UU0 := total2 ( fun f : incl X Y => istwobinopfun f ) .
+Definition twobinopmonopair { X Y : setwith2binop } ( f : incl X Y ) ( is : istwobinopfun f ) : twobinopmono X Y := tpair _ f is .
+Definition pr1twobinopmono ( X Y : setwith2binop ) : twobinopmono X Y -> incl X Y := @pr1 _ _ .
+Coercion pr1twobinopmono : twobinopmono >-> incl .
+
+Definition twobinopincltotwobinopfun ( X Y : setwith2binop ) : twobinopmono X Y -> twobinopfun X Y := fun f => twobinopfunpair ( pr1 ( pr1 f ) ) ( pr2 f ) .
+Coercion twobinopincltotwobinopfun : twobinopmono >-> twobinopfun .
+
+Definition binop1mono { X Y : setwith2binop } ( f : twobinopmono X Y ) : binopmono ( setwithbinop1 X ) ( setwithbinop1 Y ) := @binopmonopair ( setwithbinop1 X ) ( setwithbinop1 Y ) ( pr1 f ) ( pr1 ( pr2 f ) ) .
+
+Definition binop2mono { X Y : setwith2binop } ( f : twobinopmono X Y ) : binopmono ( setwithbinop2 X ) ( setwithbinop2 Y ) := @binopmonopair ( setwithbinop2 X ) ( setwithbinop2 Y ) ( pr1 f ) ( pr2 ( pr2 f ) ) .
+
+Definition twobinopmonocomp { X Y Z : setwith2binop } ( f : twobinopmono X Y ) ( g : twobinopmono Y Z ) : twobinopmono X Z := twobinopmonopair ( inclcomp ( pr1 f ) ( pr1 g ) ) ( istwobinopfuncomp f g ) .
+
+Definition twobinopiso ( X Y : setwith2binop ) : UU0 := total2 ( fun f : weq X Y => istwobinopfun f ) .
+Definition twobinopisopair { X Y : setwith2binop } ( f : weq X Y ) ( is : istwobinopfun f ) : twobinopiso X Y := tpair _ f is .
+Definition pr1twobinopiso ( X Y : setwith2binop ) : twobinopiso X Y -> weq X Y := @pr1 _ _ .
+Coercion pr1twobinopiso : twobinopiso >-> weq .
+
+Definition twobinopisototwobinopmono ( X Y : setwith2binop ) : twobinopiso X Y -> twobinopmono X Y := fun f => twobinopmonopair ( pr1 f ) ( pr2 f ) .
+Coercion twobinopisototwobinopmono : twobinopiso >-> twobinopmono .
+
+Definition binop1iso { X Y : setwith2binop } ( f : twobinopiso X Y ) : binopiso ( setwithbinop1 X ) ( setwithbinop1 Y ) := @binopisopair ( setwithbinop1 X ) ( setwithbinop1 Y ) ( pr1 f ) ( pr1 ( pr2 f ) ) .
+
+Definition binop2iso { X Y : setwith2binop } ( f : twobinopiso X Y ) : binopiso ( setwithbinop2 X ) ( setwithbinop2 Y ) := @binopisopair ( setwithbinop2 X ) ( setwithbinop2 Y ) ( pr1 f ) ( pr2 ( pr2 f ) ) .
+Definition twobinopisocomp { X Y Z : setwith2binop } ( f : twobinopiso X Y ) ( g : twobinopiso Y Z ) : twobinopiso X Z := twobinopisopair ( weqcomp ( pr1 f ) ( pr1 g ) ) ( istwobinopfuncomp f g ) .
+
+Lemma istwobinopfuninvmap { X Y : setwith2binop } ( f : twobinopiso X Y ) : istwobinopfun ( invmap ( pr1 f ) ) .
+Proof . intros . set ( ax1f := pr1 ( pr2 f ) ) . set ( ax2f := pr2 ( pr2 f ) ) . split .
+
+
+intros a b . apply ( invmaponpathsweq ( pr1 f ) ) . rewrite ( homotweqinvweq ( pr1 f ) ( op1 a b ) ) . rewrite ( ax1f (invmap (pr1 f) a) (invmap (pr1 f) b) ) . rewrite ( homotweqinvweq ( pr1 f ) a ) . rewrite ( homotweqinvweq ( pr1 f ) b ) . apply idpath .
+intros a b . apply ( invmaponpathsweq ( pr1 f ) ) . rewrite ( homotweqinvweq ( pr1 f ) ( op2 a b ) ) . rewrite ( ax2f (invmap (pr1 f) a) (invmap (pr1 f) b) ) . rewrite ( homotweqinvweq ( pr1 f ) a ) . rewrite ( homotweqinvweq ( pr1 f ) b ) . apply idpath . Defined .
+
+Opaque istwobinopfuninvmap .
+
+Definition invtwobinopiso { X Y : setwith2binop } ( f : twobinopiso X Y ) : twobinopiso Y X := twobinopisopair ( invweq ( pr1 f ) ) ( istwobinopfuninvmap f ) .
+
+
+
+
+
+(** **** Transport of properties of a pair binary operations *)
+
+Lemma isldistrmonob { X Y : setwith2binop } ( f : twobinopmono X Y ) ( is : isldistr ( @op1 Y ) ( @op2 Y ) ) : isldistr ( @op1 X ) ( @op2 X ) .
+Proof . intros . set ( ax1f := pr1 ( pr2 f ) ) . set ( ax2f := pr2 ( pr2 f ) ) . intros a b c . apply ( invmaponpathsincl _ ( pr2 ( pr1 f ) ) ) . change ( paths ( (pr1 f) (op2 c (op1 a b)))
+ ( (pr1 f) (op1 (op2 c a) (op2 c b))) ) . rewrite ( ax2f c ( op1 a b ) ) . rewrite ( ax1f a b ) . rewrite ( ax1f ( op2 c a ) ( op2 c b ) ) . rewrite ( ax2f c a ) . rewrite ( ax2f c b ) . apply is . Defined .
+
+Opaque isldistrmonob .
+
+
+Lemma isrdistrmonob { X Y : setwith2binop } ( f : twobinopmono X Y ) ( is : isrdistr ( @op1 Y ) ( @op2 Y ) ) : isrdistr ( @op1 X ) ( @op2 X ) .
+Proof . intros . set ( ax1f := pr1 ( pr2 f ) ) . set ( ax2f := pr2 ( pr2 f ) ) . intros a b c . apply ( invmaponpathsincl _ ( pr2 ( pr1 f ) ) ) . change ( paths ( (pr1 f) (op2 (op1 a b) c))
+ ( (pr1 f) (op1 (op2 a c) (op2 b c))) ) . rewrite ( ax2f ( op1 a b ) c ) . rewrite ( ax1f a b ) . rewrite ( ax1f ( op2 a c ) ( op2 b c ) ) . rewrite ( ax2f a c ) . rewrite ( ax2f b c ) . apply is . Defined .
+
+Opaque isrdistrmonob .
+
+Definition isdistrmonob { X Y : setwith2binop } ( f : twobinopmono X Y ) ( is : isdistr ( @op1 Y ) ( @op2 Y ) ) : isdistr ( @op1 X ) ( @op2 X ) := dirprodpair ( isldistrmonob f ( pr1 is ) ) ( isrdistrmonob f ( pr2 is ) ) .
+
+Notation isldistrisob := isldistrmonob .
+Notation isrdistrisob := isrdistrmonob .
+Notation isdistrisob := isdistrmonob .
+
+Lemma isldistrisof { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : isldistr ( @op1 X ) ( @op2 X ) ) : isldistr ( @op1 Y ) ( @op2 Y ) .
+Proof . intros . apply ( isldistrisob ( invtwobinopiso f ) is ) . Defined .
+
+Lemma isrdistrisof { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : isrdistr ( @op1 X ) ( @op2 X ) ) : isrdistr ( @op1 Y ) ( @op2 Y ) .
+Proof . intros . apply ( isrdistrisob ( invtwobinopiso f ) is ) . Defined .
+
+Lemma isdistrisof { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : isdistr ( @op1 X ) ( @op2 X ) ) : isdistr ( @op1 Y ) ( @op2 Y ) .
+Proof . intros . apply ( isdistrisob ( invtwobinopiso f ) is ) . Defined .
+
+
+Definition isrigopsisof { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : isrigops ( @op1 X ) ( @op2 X ) ) : isrigops ( @op1 Y ) ( @op2 Y ) .
+Proof . intros. split . split with ( dirprodpair ( isabmonoidopisof ( binop1iso f ) ( rigop1axs_is is ) ) ( ismonoidopisof ( binop2iso f ) ( rigop2axs_is is ) ) ) . simpl . change (unel_is (ismonoidopisof (binop1iso f) (rigop1axs_is is))) with ( (pr1 f ) ( rigunel1_is is ) ) . split . intro y . rewrite ( pathsinv0 ( homotweqinvweq f y ) ) . rewrite ( pathsinv0 ( ( pr2 ( pr2 f ) ) _ _ ) ) . apply ( maponpaths ( pr1 f ) ) . apply ( rigmult0x_is is ) . intro y . rewrite ( pathsinv0 ( homotweqinvweq f y ) ) . rewrite ( pathsinv0 ( ( pr2 ( pr2 f ) ) _ _ ) ) . apply ( maponpaths ( pr1 f ) ) . apply ( rigmultx0_is is ) . apply ( isdistrisof f ) . apply ( rigdistraxs_is is ) . Defined .
+
+Definition isrigopsisob { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : isrigops ( @op1 Y ) ( @op2 Y ) ) : isrigops ( @op1 X ) ( @op2 X ) .
+Proof. intros . apply ( isrigopsisof ( invtwobinopiso f ) is ) . Defined .
+
+
+Definition isrngopsisof { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : isrngops ( @op1 X ) ( @op2 X ) ) : isrngops ( @op1 Y ) ( @op2 Y ) := dirprodpair ( dirprodpair ( isabgropisof ( binop1iso f ) ( rngop1axs_is is ) ) ( ismonoidopisof ( binop2iso f ) ( rngop2axs_is is ) ) ) ( isdistrisof f ( pr2 is ) ) .
+
+Definition isrngopsisob { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : isrngops ( @op1 Y ) ( @op2 Y ) ) : isrngops ( @op1 X ) ( @op2 X ) := dirprodpair ( dirprodpair ( isabgropisob ( binop1iso f ) ( rngop1axs_is is ) ) ( ismonoidopisob ( binop2iso f ) ( rngop2axs_is is ) ) ) ( isdistrisob f ( pr2 is ) ) .
+
+
+Definition iscommrngopsisof { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : iscommrngops ( @op1 X ) ( @op2 X ) ) : iscommrngops ( @op1 Y ) ( @op2 Y ) := dirprodpair ( isrngopsisof f is ) ( iscommisof ( binop2iso f ) ( pr2 is ) ) .
+
+Definition iscommrngopsisob { X Y : setwith2binop } ( f : twobinopiso X Y ) ( is : iscommrngops ( @op1 Y ) ( @op2 Y ) ) : iscommrngops ( @op1 X ) ( @op2 X ) := dirprodpair ( isrngopsisob f is ) ( iscommisob ( binop2iso f ) ( pr2 is ) ) .
+
+
+
+
+(** **** Subobjects *)
+
+Definition issubsetwith2binop { X : setwith2binop } ( A : hsubtypes X ) := dirprod ( forall a a' : A , A ( op1 ( pr1 a ) ( pr1 a' ) ) ) ( forall a a' : A , A ( op2 ( pr1 a ) ( pr1 a' ) ) ) .
+
+Lemma isapropissubsetwith2binop { X : setwith2binop } ( A : hsubtypes X ) : isaprop ( issubsetwith2binop A ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) .
+ apply impred . intro a . apply impred . intros a' . apply ( pr2 ( A ( op1 (pr1 a) (pr1 a')) ) ) . apply impred . intro a . apply impred . intros a' . apply ( pr2 ( A ( op2 (pr1 a) (pr1 a')) ) ) . Defined .
+
+Definition subsetswith2binop { X : setwith2binop } := total2 ( fun A : hsubtypes X => issubsetwith2binop A ) .
+Definition subsetswith2binoppair { X : setwith2binop } := tpair ( fun A : hsubtypes X => issubsetwith2binop A ) .
+Definition subsetswith2binopconstr { X : setwith2binop } := @subsetswith2binoppair X .
+Definition pr1subsetswith2binop ( X : setwith2binop ) : @subsetswith2binop X -> hsubtypes X := @pr1 _ ( fun A : hsubtypes X => issubsetwith2binop A ) .
+Coercion pr1subsetswith2binop : subsetswith2binop >-> hsubtypes .
+
+Definition totalsubsetwith2binop ( X : setwith2binop ) : @subsetswith2binop X .
+Proof . intros . split with ( fun x : X => htrue ) . split . intros x x' . apply tt . intros . apply tt . Defined .
+
+
+Definition carrierofsubsetwith2binop { X : setwith2binop } ( A : @subsetswith2binop X ) : setwith2binop .
+Proof . intros . set ( aset := ( hSetpair ( carrier A ) ( isasetsubset ( pr1carrier A ) ( setproperty X ) ( isinclpr1carrier A ) ) ) : hSet ) . split with aset .
+set ( subopp1 := ( fun a a' : A => carrierpair A ( op1 ( pr1carrier _ a ) ( pr1carrier _ a' ) ) ( pr1 ( pr2 A ) a a' ) ) : ( A -> A -> A ) ) .
+set ( subopp2 := ( fun a a' : A => carrierpair A ( op2 ( pr1carrier _ a ) ( pr1carrier _ a' ) ) ( pr2 ( pr2 A ) a a' ) ) : ( A -> A -> A ) ) .
+simpl . apply ( dirprodpair subopp1 subopp2 ) . Defined .
+
+Coercion carrierofsubsetwith2binop : subsetswith2binop >-> setwith2binop .
+
+
+(** **** Quotient objects *)
+
+Definition is2binophrel { X : setwith2binop } ( R : hrel X ) := dirprod ( @isbinophrel ( setwithbinop1 X ) R ) ( @isbinophrel ( setwithbinop2 X ) R ) .
+
+Lemma isapropis2binophrel { X : setwith2binop } ( R : hrel X ) : isaprop ( is2binophrel R ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply isapropisbinophrel . apply isapropisbinophrel .
+Defined .
+
+Lemma iscomp2binoptransrel { X : setwith2binop } ( R : hrel X ) ( is : istrans R ) ( isb : is2binophrel R ) : dirprod ( iscomprelrelfun2 R R ( @op1 X ) ) ( iscomprelrelfun2 R R ( @op2 X ) ) .
+Proof . intros . split . apply ( @iscompbinoptransrel ( setwithbinop1 X ) R is ( pr1 isb ) ) . apply ( @iscompbinoptransrel ( setwithbinop2 X ) R is ( pr2 isb ) ) . Defined .
+
+
+Definition twobinophrel { X : setwith2binop } := total2 ( fun R : hrel X => is2binophrel R ) .
+Definition twobinophrelpair { X : setwith2binop } := tpair ( fun R : hrel X => is2binophrel R ) .
+Definition pr1twobinophrel ( X : setwith2binop ) : @twobinophrel X -> hrel X := @pr1 _ ( fun R : hrel X => is2binophrel R ) .
+Coercion pr1twobinophrel : twobinophrel >-> hrel .
+
+Definition twobinoppo { X : setwith2binop } := total2 ( fun R : po X => is2binophrel R ) .
+Definition twobinoppopair { X : setwith2binop } := tpair ( fun R : po X => is2binophrel R ) .
+Definition pr1twobinoppo ( X : setwith2binop ) : @twobinoppo X -> po X := @pr1 _ ( fun R : po X => is2binophrel R ) .
+Coercion pr1twobinoppo : twobinoppo >-> po .
+
+Definition twobinopeqrel { X : setwith2binop } := total2 ( fun R : eqrel X => is2binophrel R ) .
+Definition twobinopeqrelpair { X : setwith2binop } := tpair ( fun R : eqrel X => is2binophrel R ) .
+Definition pr1twobinopeqrel ( X : setwith2binop ) : @twobinopeqrel X -> eqrel X := @pr1 _ ( fun R : eqrel X => is2binophrel R ) .
+Coercion pr1twobinopeqrel : twobinopeqrel >-> eqrel .
+
+Definition setwith2binopquot { X : setwith2binop } ( R : @twobinopeqrel X ) : setwith2binop .
+Proof . intros . split with ( setquotinset R ) . set ( qt := setquot R ) . set ( qtset := setquotinset R ) .
+assert ( iscomp1 : iscomprelrelfun2 R R ( @op1 X ) ) . apply ( pr1 ( iscomp2binoptransrel ( pr1 R ) ( eqreltrans _ ) ( pr2 R ) ) ) . set ( qtop1 := setquotfun2 R R ( @op1 X ) iscomp1 ) .
+assert ( iscomp2 : iscomprelrelfun2 R R ( @op2 X ) ) . apply ( pr2 ( iscomp2binoptransrel ( pr1 R ) ( eqreltrans _ ) ( pr2 R ) ) ) . set ( qtop2 := setquotfun2 R R ( @op2 X ) iscomp2 ) .
+simpl . apply ( dirprodpair qtop1 qtop2 ) . Defined .
+
+
+(** **** Direct products *)
+
+Definition setwith2binopdirprod ( X Y : setwith2binop ) : setwith2binop .
+Proof . intros . split with ( setdirprod X Y ) . simpl . apply ( dirprodpair ( fun xy xy' : _ => dirprodpair ( op1 ( pr1 xy ) ( pr1 xy' ) ) ( op1 ( pr2 xy ) ( pr2 xy' ) ) ) ( fun xy xy' : _ => dirprodpair ( op2 ( pr1 xy ) ( pr1 xy' ) ) ( op2 ( pr2 xy ) ( pr2 xy' ) ) ) ) . Defined .
+
+
+
+
+
+
+
+(* End of the file algebra1a.v *)
+
+
+
+
+
+(*
+*** Local Variables: ***
+*** coq-prog-name: "/opt/local/bin/coqtop" ***
+*** coq-prog-args: ("-emacs-U") ***
+*** End: ***
+ *)
View
1,021 hlevel2/algebra1b.v
@@ -0,0 +1,1021 @@
+(** * Algebra I. Part B. Monoids, abelian monoids groups, abelian groups. Vladimir Voevodsky. Aug. 2011 - .
+
+*)
+
+
+
+(** ** Preambule *)
+
+(** Settings *)
+
+Add Rec LoadPath "../Generalities".
+Add Rec LoadPath "../hlevel1".
+Add Rec LoadPath "../hlevel2".
+
+Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *)
+
+
+(** Imports *)
+
+Require Export algebra1a .
+
+
+(** To upstream files *)
+
+
+(** ** Standard Algebraic Structures *)
+
+
+(** *** Monoids *)
+
+
+(** **** Basic definitions *)
+
+
+
+Definition monoid := total2 ( fun X : setwithbinop => ismonoidop ( @op X ) ) .
+Definition monoidpair := tpair ( fun X : setwithbinop => ismonoidop ( @op X ) ) .
+Definition monoidconstr := monoidpair .
+Definition pr1monoid : monoid -> setwithbinop := @pr1 _ _ .
+Coercion pr1monoid : monoid >-> setwithbinop .
+
+Definition assocax ( X : monoid ) : isassoc ( @op X ) := pr1 ( pr2 X ) .
+Definition unel ( X : monoid) : X := pr1 ( pr2 ( pr2 X ) ) .
+Definition lunax ( X : monoid ) : islunit ( @op X ) ( unel X ) := pr1 ( pr2 ( pr2 ( pr2 X ) ) ) .
+Definition runax ( X : monoid ) : isrunit ( @op X ) ( unel X ) := pr2 ( pr2 ( pr2 ( pr2 X ) ) ) .
+
+Notation "x + y" := ( op x y ) : addmonoid_scope .
+Notation "0" := ( unel _ ) : addmonoid_scope .
+
+Delimit Scope addmonoid_scope with addmonoid.
+
+Notation "x * y" := ( op x y ) : multmonoid_scope .
+Notation "1" := ( unel _ ) : multmonoid_scope .
+
+Delimit Scope multmonoid_scope with multmonoid.
+
+
+
+(** **** Functions betweens monoids compatible with structure ( homomorphisms ) and their properties *)
+
+
+Definition ismonoidfun { X Y : monoid } ( f : X -> Y ) := dirprod ( isbinopfun f ) ( paths ( f ( unel X ) ) ( unel Y ) ) .
+
+Lemma isapropismonoidfun { X Y : monoid } ( f : X -> Y ) : isaprop ( ismonoidfun f ) .
+Proof . intros . apply isofhleveldirprod . apply isapropisbinopfun . apply ( setproperty Y ) . Defined .
+
+Definition monoidfun ( X Y : monoid ) : UU0 := total2 ( fun f : X -> Y => ismonoidfun f ) .
+Definition monoidfunconstr { X Y : monoid } { f : X -> Y } ( is : ismonoidfun f ) : monoidfun X Y := tpair _ f is .
+Definition pr1monoidfun ( X Y : monoid ) : monoidfun X Y -> ( X -> Y ) := @pr1 _ _ .
+
+Definition monoidfuntobinopfun ( X Y : monoid ) : monoidfun X Y -> binopfun X Y := fun f => binopfunpair ( pr1 f ) ( pr1 ( pr2 f ) ) .
+Coercion monoidfuntobinopfun : monoidfun >-> binopfun .
+
+
+Lemma isasetmonoidfun ( X Y : monoid ) : isaset ( monoidfun X Y ) .
+Proof . intros . apply ( isasetsubset ( pr1monoidfun X Y ) ) . change ( isofhlevel 2 ( X -> Y ) ) . apply impred . intro . apply ( setproperty Y ) . apply isinclpr1 . intro . apply isapropismonoidfun . Defined .
+
+
+Lemma ismonoidfuncomp { X Y Z : monoid } ( f : monoidfun X Y ) ( g : monoidfun Y Z ) : ismonoidfun ( funcomp ( pr1 f ) ( pr1 g ) ) .
+Proof . intros . split with ( isbinopfuncomp f g ) . unfold funcomp . rewrite ( pr2 ( pr2 f ) ) . apply ( pr2 ( pr2 g ) ) . Defined .
+
+Opaque ismonoidfuncomp .
+
+Definition monoidfuncomp { X Y Z : monoid } ( f : monoidfun X Y ) ( g : monoidfun Y Z ) : monoidfun X Z := monoidfunconstr ( ismonoidfuncomp f g ) .
+
+
+Definition monoidmono ( X Y : monoid ) : UU0 := total2 ( fun f : incl X Y => ismonoidfun f ) .
+Definition monoidmonopair { X Y : monoid } ( f : incl X Y ) ( is : ismonoidfun f ) : monoidmono X Y := tpair _ f is .
+Definition pr1monoidmono ( X Y : monoid ) : monoidmono X Y -> incl X Y := @pr1 _ _ .
+Coercion pr1monoidmono : monoidmono >-> incl .
+
+Definition monoidincltomonoidfun ( X Y : monoid ) : monoidmono X Y -> monoidfun X Y := fun f => monoidfunconstr ( pr2 f ) .
+Coercion monoidincltomonoidfun : monoidmono >-> monoidfun .
+
+Definition monoidmonotobinopmono ( X Y : monoid ) : monoidmono X Y -> binopmono X Y := fun f => binopmonopair ( pr1 f ) ( pr1 ( pr2 f ) ) .
+Coercion monoidmonotobinopmono : monoidmono >-> binopmono .
+
+Definition monoidmonocomp { X Y Z : monoid } ( f : monoidmono X Y ) ( g : monoidmono Y Z ) : monoidmono X Z := monoidmonopair ( inclcomp ( pr1 f ) ( pr1 g ) ) ( ismonoidfuncomp f g ) .
+
+
+Definition monoidiso ( X Y : monoid ) : UU0 := total2 ( fun f : weq X Y => ismonoidfun f ) .
+Definition monoidisopair { X Y : monoid } ( f : weq X Y ) ( is : ismonoidfun f ) : monoidiso X Y := tpair _ f is .
+Definition pr1monoidiso ( X Y : monoid ) : monoidiso X Y -> weq X Y := @pr1 _ _ .
+Coercion pr1monoidiso : monoidiso >-> weq .
+
+Definition monoidisotomonoidmono ( X Y : monoid ) : monoidiso X Y -> monoidmono X Y := fun f => monoidmonopair ( pr1 f ) ( pr2 f ) .
+Coercion monoidisotomonoidmono : monoidiso >-> monoidmono .
+
+Definition monoidisotobinopiso ( X Y : monoid ) : monoidiso X Y -> binopiso X Y := fun f => binopisopair ( pr1 f ) ( pr1 ( pr2 f ) ) .
+Coercion monoidisotobinopiso : monoidiso >-> binopiso .
+
+
+Lemma ismonoidfuninvmap { X Y : monoid } ( f : monoidiso X Y ) : ismonoidfun ( invmap ( pr1 f ) ) .
+Proof . intros . split with ( isbinopfuninvmap f ) . apply ( invmaponpathsweq ( pr1 f ) ) . rewrite ( homotweqinvweq ( pr1 f ) ) . apply ( pathsinv0 ( pr2 ( pr2 f ) ) ) . Defined .
+
+Opaque ismonoidfuninvmap .
+
+Definition invmonoidiso { X Y : monoid } ( f : monoidiso X Y ) : monoidiso Y X := monoidisopair ( invweq ( pr1 f ) ) ( ismonoidfuninvmap f ) .
+
+
+
+
+(** **** Subobjects *)
+
+Definition issubmonoid { X : monoid } ( A : hsubtypes X ) := dirprod ( issubsetwithbinop ( @op X ) A ) ( A ( unel X ) ) .
+
+Lemma isapropissubmonoid { X : monoid } ( A : hsubtypes X ) : isaprop ( issubmonoid A ) .
+Proof . intros . apply ( isofhleveldirprod 1 ) . apply isapropissubsetwithbinop . apply ( pr2 ( A ( unel X ) ) ) . Defined .
+
+Definition submonoids { X : monoid } := total2 ( fun A : hsubtypes X => issubmonoid A ) .
+Definition submonoidpair { X : monoid } := tpair ( fun A : hsubtypes X => issubmonoid A ) .
+Definition submonoidconstr { X : monoid } := @submonoidpair X .
+Definition pr1submonoids ( X : monoid ) : @submonoids X -> hsubtypes X := @pr1 _ _ .
+
+Definition totalsubmonoid ( X : monoid ) : @submonoids X .
+Proof . intro . split with ( fun x : _ => htrue ) . split . intros x x' . apply tt . apply tt . Defined .
+
+Definition submonoidstosubsetswithbinop ( X : monoid ) : @submonoids X -> @subsetswithbinop X := fun A : _ => subsetswithbinoppair ( pr1 A ) ( pr1 ( pr2 A ) ) .
+Coercion submonoidstosubsetswithbinop : submonoids >-> subsetswithbinop .
+
+Lemma ismonoidcarrier { X : monoid } ( A : @submonoids X ) : ismonoidop ( @op A ) .
+Proof . intros . split . intros a a' a'' . apply ( invmaponpathsincl _ ( isinclpr1carrier A ) ) . simpl . apply ( assocax X ) . split with ( carrierpair _ ( unel X ) ( pr2 ( pr2 A ) ) ) . split . simpl . intro a . apply ( invmaponpathsincl _ ( isinclpr1carrier A ) ) . simpl . apply ( lunax X ) . intro a . apply ( invmaponpathsincl _ ( isinclpr1carrier A ) ) . simpl . apply ( runax X ) . Defined .
+
+Definition carrierofsubmonoid { X : monoid } ( A : @submonoids X ) : monoid .
+Proof . intros . split with A . apply ismonoidcarrier . Defined .
+
+Coercion carrierofsubmonoid : submonoids >-> monoid .
+
+
+
+
+(** **** Quotient objects *)
+
+Lemma isassocquot { X : monoid } ( R : @binopeqrel X ) : isassoc ( @op ( setwithbinopquot R ) ) .
+Proof . intros . intros a b c . apply ( setquotuniv3prop R ( fun x x' x'' : setwithbinopquot R => hProppair _ ( setproperty ( setwithbinopquot R ) ( op ( op x x' ) x'' ) ( op x ( op x' x'' )) ) ) ) . intros x x' x'' . apply ( maponpaths ( setquotpr R ) ( assocax X x x' x'' ) ) . Defined .
+
+Opaque isassocquot .
+
+
+Lemma isunitquot { X : monoid } ( R : @binopeqrel X ) : isunit ( @op ( setwithbinopquot R ) ) ( setquotpr R ( pr1 ( pr2 ( pr2 X ) ) ) ) .
+Proof . intros . set ( qun := setquotpr R ( pr1 ( pr2 ( pr2 X ) ) ) ) . set ( qsetwithop := setwithbinopquot R ) . split .
+
+intro x . apply ( setquotunivprop R ( fun x => @eqset qsetwithop ( ( @op qsetwithop ) qun x ) x ) ) . simpl . intro x0 . apply ( maponpaths ( setquotpr R ) ( lunax X x0 ) ) .
+
+intro x . apply ( setquotunivprop R ( fun x => @eqset qsetwithop ( ( @op qsetwithop ) x qun ) x ) ) . simpl . intro x0 . apply ( maponpaths ( setquotpr R ) ( runax X x0 ) ) . Defined .
+
+Opaque isunitquot .
+
+
+Definition ismonoidquot { X : monoid } ( R : @binopeqrel X ) : ismonoidop ( @op ( setwithbinopquot R ) ) := tpair _ ( isassocquot R ) ( tpair _ ( setquotpr R ( pr1 ( pr2 ( pr2 X ) ) ) ) ( isunitquot R ) ) .
+
+Definition monoidquot { X : monoid } ( R : @binopeqrel X ) : monoid .
+Proof . intros . split with ( setwithbinopquot R ) . apply ismonoidquot . Defined .
+
+
+(** **** Direct products *)
+
+Lemma isassocdirprod ( X Y : monoid ) : isassoc ( @op ( setwithbinopdirprod X Y ) ) .
+Proof . intros . simpl . intros xy xy' xy'' . simpl . apply pathsdirprod . apply ( assocax X ) . apply ( assocax Y ) . Defined .
+
+Opaque isassocdirprod .
+
+Lemma isunitindirprod ( X Y : monoid ) : isunit ( @op ( setwithbinopdirprod X Y ) ) ( dirprodpair ( unel X ) ( unel Y ) ) .
+Proof . split .
+
+intro xy . destruct xy as [ x y ] . simpl . apply pathsdirprod . apply ( lunax X ) . apply ( lunax Y ) .
+intro xy . destruct xy as [ x y ] . simpl . apply pathsdirprod . apply ( runax X ) . apply ( runax Y ) . Defined .
+
+Opaque isunitindirprod .
+
+Definition ismonoiddirprod ( X Y : monoid ) : ismonoidop ( @op ( setwithbinopdirprod X Y ) ) := tpair _ ( isassocdirprod X Y ) ( tpair _ ( dirprodpair ( unel X ) ( unel Y ) ) ( isunitindirprod X Y ) ) .
+
+Definition monoiddirprod ( X Y : monoid ) : monoid .
+Proof . intros . split with ( setwithbinopdirprod X Y ) . apply ismonoiddirprod . Defined .
+
+
+
+
+
+
+(** *** Abelian ( commutative ) monoids *)
+
+
+(** **** Basic definitions *)
+
+
+Definition abmonoid := total2 ( fun X : setwithbinop => isabmonoidop ( @op X ) ) .
+Definition abmonoidpair := tpair ( fun X : setwithbinop => isabmonoidop ( @op X ) ) .
+Definition abmonoidconstr := abmonoidpair .
+
+Definition abmonoidtomonoid : abmonoid -> monoid := fun X : _ => monoidpair ( pr1 X ) ( pr1 ( pr2 X ) ) .
+Coercion abmonoidtomonoid : abmonoid >-> monoid .
+
+Definition commax ( X : abmonoid ) : iscomm ( @op X ) := pr2 ( pr2 X ) .
+
+Definition abmonoidrer ( X : abmonoid ) ( a b c d : X ) : paths ( op ( op a b ) ( op c d ) ) ( op ( op a c ) ( op b d ) ) := abmonoidoprer ( pr2 X ) a b c d .
+
+
+(** **** Subobjects *)
+
+Definition subabmonoids { X : abmonoid } := @submonoids X .
+Identity Coercion id_subabmonoids : subabmonoids >-> submonoids .
+
+Lemma iscommcarrier { X : abmonoid } ( A : @submonoids X ) : iscomm ( @op A ) .
+Proof . intros . intros a a' . apply ( invmaponpathsincl _ ( isinclpr1carrier A ) ) . simpl . apply ( pr2 ( pr2 X ) ) . Defined .
+
+Opaque iscommcarrier .
+
+Definition isabmonoidcarrier { X : abmonoid } ( A : @submonoids X ) : isabmonoidop ( @op A ) := dirprodpair ( ismonoidcarrier A ) ( iscommcarrier A ) .
+
+Definition carrierofsubabmonoid { X : abmonoid } ( A : @subabmonoids X ) : abmonoid .
+Proof . intros . unfold subabmonoids in A . split with A . apply isabmonoidcarrier . Defined .
+
+Coercion carrierofsubabmonoid : subabmonoids >-> abmonoid .
+
+
+
+
+(** **** Quotient objects *)
+
+Lemma iscommquot { X : abmonoid } ( R : @binopeqrel X ) : iscomm ( @op ( setwithbinopquot R ) ) .
+Proof . intros . set ( X0 := setwithbinopquot R ) . intros x x' . apply ( setquotuniv2prop R ( fun x x' : X0 => hProppair _ ( setproperty X0 ( op x x') ( op x' x) ) ) ) . intros x0 x0' . apply ( maponpaths ( setquotpr R ) ( ( commax X ) x0 x0' ) ) . Defined .
+
+Opaque iscommquot .
+
+Definition isabmonoidquot { X : abmonoid } ( R : @binopeqrel X ) : isabmonoidop ( @op ( setwithbinopquot R ) ) := dirprodpair ( ismonoidquot R ) ( iscommquot R ) .
+
+Definition abmonoidquot { X : abmonoid } ( R : @binopeqrel X ) : abmonoid .
+Proof . intros . split with ( setwithbinopquot R ) . apply isabmonoidquot . Defined .
+
+
+(** **** Direct products *)
+
+Lemma iscommdirprod ( X Y : abmonoid ) : iscomm ( @op ( setwithbinopdirprod X Y ) ) .
+Proof . intros . intros xy xy' . destruct xy as [ x y ] . destruct xy' as [ x' y' ] . simpl . apply pathsdirprod . apply ( commax X ) . apply ( commax Y ) . Defined .
+
+Opaque iscommdirprod .
+
+Definition isabmonoiddirprod ( X Y : abmonoid ) : isabmonoidop ( @op ( setwithbinopdirprod X Y ) ) := dirprodpair ( ismonoiddirprod X Y ) ( iscommdirprod X Y ) .
+
+Definition abmonoiddirprod ( X Y : abmonoid ) : abmonoid .
+Proof . intros . split with ( setwithbinopdirprod X Y ) . apply isabmonoiddirprod . Defined .
+
+
+
+
+(** **** Monoid of fractions of an abelian monoid
+
+Note : the following construction uses onbly associativity and commutativity of the [ abmonoid ] operations but does not use the unit element . *)
+
+Open Scope addmonoid_scope .
+
+Definition abmonoidfracopint ( X : abmonoid ) ( A : @submonoids X ) : binop ( dirprod X A ) := @op ( setwithbinopdirprod X A ) .
+
+Definition hrelabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : hrel ( setwithbinopdirprod X A ) := fun xa yb : dirprod X A => hexists ( fun a0 : A => paths ( ( ( pr1 xa ) + ( pr1 ( pr2 yb ) ) ) + ( pr1 a0 ) ) ( ( ( pr1 yb ) + ( pr1 ( pr2 xa ) ) + ( pr1 a0 ) ) ) ) .
+
+Lemma iseqrelabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : iseqrel ( hrelabmonoidfrac X A ) .
+Proof . intros . set ( assoc := assocax X ) . set ( comm := commax X ) . set ( R := hrelabmonoidfrac X A ) .
+
+assert ( symm : issymm R ) . intros xa yb . unfold R . simpl . apply hinhfun . intro eq1 . destruct eq1 as [ x1 eq1 ] . split with x1 . destruct x1 as [ x1 isx1 ] . simpl . apply ( pathsinv0 eq1 ) .
+
+assert ( trans : istrans R ) . unfold istrans . intros ab cd ef . simpl . apply hinhfun2 . destruct ab as [ a b ] . destruct cd as [ c d ] . destruct ef as [ e f ] . destruct b as [ b isb ] . destruct d as [ d isd ] . destruct f as [ f isf ] . intros eq1 eq2 . destruct eq1 as [ x1 eq1 ] . destruct eq2 as [ x2 eq2 ] . simpl in * . split with ( @op A ( tpair _ d isd ) ( @op A x1 x2 ) ) . destruct x1 as [ x1 isx1 ] . destruct x2 as [ x2 isx2 ] . destruct A as [ A ax ] . simpl in * . rewrite ( assoc a f ( d + ( x1 + x2 ) ) ) . rewrite ( comm f ( d + ( x1 + x2 ) ) ) . destruct ( assoc a ( d + ( x1 + x2 ) ) f ) . destruct ( assoc a d ( x1 + x2 ) ) . destruct ( assoc ( a + d ) x1 x2 ) . rewrite eq1 . rewrite ( comm x1 x2 ) . rewrite ( assoc e b ( d + ( x2 + x1 ) ) ) . rewrite ( comm b ( d + ( x2 + x1 ) ) ) . destruct ( assoc e ( d + ( x2 + x1 ) ) b ) . destruct ( assoc e d ( x2 + x1 ) ) . destruct ( assoc ( e + d ) x2 x1 ) . destruct eq2 . rewrite ( assoc ( c + b ) x1 x2 ) . rewrite ( assoc ( c + f ) x2 x1 ) . rewrite ( comm x1 x2 ) . rewrite ( assoc ( c + b ) ( x2 + x1 ) f ) . rewrite ( assoc ( c + f ) ( x2 + x1 ) b ) . rewrite ( comm ( x2 + x1 ) f ) . rewrite ( comm ( x2 + x1 ) b ) . destruct ( assoc ( c + b ) f ( x2 + x1 ) ) . destruct ( assoc ( c + f ) b ( x2 + x1 ) ) . rewrite ( assoc c b f ) . rewrite ( assoc c f b ) . rewrite ( comm b f ) . apply idpath .
+
+assert ( refl : isrefl R ) . intro xa . simpl . apply hinhpr . split with ( pr2 xa ) . apply idpath .
+
+apply ( iseqrelconstr trans refl symm ) . Defined .
+
+Opaque iseqrelabmonoidfrac .
+
+Definition eqrelabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : eqrel ( setwithbinopdirprod X A ) := eqrelpair ( hrelabmonoidfrac X A ) ( iseqrelabmonoidfrac X A ) .
+
+Lemma isbinophrelabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : @isbinophrel ( setwithbinopdirprod X A ) ( eqrelabmonoidfrac X A ) .
+Proof . intros . apply ( isbinopreflrel ( eqrelabmonoidfrac X A ) ( eqrelrefl ( eqrelabmonoidfrac X A ) ) ) . set ( rer := abmonoidoprer ( pr2 X ) ) . intros a b c d . simpl . apply hinhfun2 . destruct a as [ a a' ] . destruct a' as [ a' isa' ] . destruct b as [ b b' ] . destruct b' as [ b' isb' ] . destruct c as [ c c' ] . destruct c' as [ c' isc' ] . destruct d as [ d d' ] . destruct d' as [ d' isd' ] . intros ax ay . destruct ax as [ a1 eq1 ] . destruct ay as [ a2 eq2 ] . split with ( @op A a1 a2 ) . destruct a1 as [ a1 aa1 ] . destruct a2 as [ a2 aa2 ] . simpl in *. rewrite ( rer a c b' d' ) . rewrite ( rer b d a' c' ) . rewrite ( rer ( a + b' ) ( c + d' ) a1 a2 ) . rewrite ( rer ( b + a' ) ( d + c' ) a1 a2 ) . destruct eq1 . destruct eq2 . apply idpath . Defined .
+
+Opaque isbinophrelabmonoidfrac .
+
+Definition abmonoidfracop ( X : abmonoid ) ( A : @submonoids X ) : binop ( setquot ( hrelabmonoidfrac X A ) ) := setquotfun2 ( hrelabmonoidfrac X A ) ( eqrelabmonoidfrac X A ) ( abmonoidfracopint X A ) ( ( iscompbinoptransrel _ ( eqreltrans _ ) ( isbinophrelabmonoidfrac X A ) ) ) .
+
+Definition binopeqrelabmonoidfrac ( X : abmonoid ) ( A : @subabmonoids X ) : @binopeqrel ( abmonoiddirprod X A ) := @binopeqrelpair ( setwithbinopdirprod X A ) ( eqrelabmonoidfrac X A ) ( isbinophrelabmonoidfrac X A ) .
+
+Definition abmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : abmonoid := abmonoidquot ( binopeqrelabmonoidfrac X A ) .
+
+Definition prabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : X -> A -> abmonoidfrac X A := fun ( x : X ) ( a : A ) => setquotpr ( eqrelabmonoidfrac X A ) ( dirprodpair x a ) .
+
+(* ??? could the use of [ issubabmonoid ] in [ binopeqrelabmonoidfrac ] and [ submonoid ] in [ abmonoidfrac ] lead to complications for the unification machinery? See also [ abmonoidfracisbinoprelint ] below . *)
+
+Lemma invertibilityinabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : forall a a' : A , isinvertible ( @op ( abmonoidfrac X A ) ) ( prabmonoidfrac X A ( pr1 a ) a' ) .
+Proof . intros . set ( R := eqrelabmonoidfrac X A ) . unfold isinvertible .
+
+assert ( isl : islinvertible ( @op ( abmonoidfrac X A ) ) ( prabmonoidfrac X A ( pr1 a ) a' ) ) . unfold islinvertible . set ( f := fun x0 : abmonoidfrac X A => prabmonoidfrac X A (pr1 a) a' + x0 ) . set ( g := fun x0 : abmonoidfrac X A => prabmonoidfrac X A (pr1 a' ) a + x0 ) .
+assert ( egf : forall x0 : _ , paths ( g ( f x0 ) ) x0 ) . apply ( setquotunivprop R ( fun x0 : abmonoidfrac X A => eqset (g (f x0)) x0 ) ) . intro xb . simpl . apply ( iscompsetquotpr R ( @dirprodpair X A ( ( pr1 a' ) + ( ( pr1 a ) + ( pr1 xb ) ) ) ( ( @op A ) a ( ( @op A ) a' ( pr2 xb ) ) ) ) ) . simpl . apply hinhpr . split with ( unel A ) . unfold pr1carrier . simpl . set ( e := assocax X ( pr1 a ) ( pr1 a' ) ( pr1 ( pr2 xb ) ) ) . simpl in e . destruct e . set ( e := assocax X ( pr1 xb ) ( pr1 a + pr1 a' ) ( pr1 ( pr2 xb ) ) ) . simpl in e . destruct e . set ( e := assocax X ( pr1 a' ) ( pr1 a ) ( pr1 xb ) ) . simpl in e . destruct e . set ( e := commax X ( pr1 a ) ( pr1 a' ) ) . simpl in e . destruct e . set ( e := commax X ( pr1 a + pr1 a' ) ( pr1 xb ) ) . simpl in e . destruct e . apply idpath .
+assert ( efg : forall x0 : _ , paths ( f ( g x0 ) ) x0 ) . apply ( setquotunivprop R ( fun x0 : abmonoidfrac X A => eqset (f (g x0)) x0 ) ) . intro xb . simpl . apply ( iscompsetquotpr R ( @dirprodpair X A ( ( pr1 a ) + ( ( pr1 a' ) + ( pr1 xb ) ) ) ( ( @op A ) a' ( ( @op A ) a ( pr2 xb ) ) ) ) ) . simpl . apply hinhpr . split with ( unel A ) . unfold pr1carrier . simpl . set ( e := assocax X ( pr1 a' ) ( pr1 a ) ( pr1 ( pr2 xb ) ) ) . simpl in e . destruct e . set ( e := assocax X ( pr1 xb ) ( pr1 a' + pr1 a ) ( pr1 ( pr2 xb ) ) ) . simpl in e . destruct e . set ( e := assocax X ( pr1 a ) ( pr1 a' ) ( pr1 xb ) ) . simpl in e . destruct e . set ( e := commax X ( pr1 a' ) ( pr1 a ) ) . simpl in e . destruct e . set ( e := commax X ( pr1 a' + pr1 a ) ( pr1 xb ) ) . simpl in e . destruct e . apply idpath .
+apply ( gradth _ _ egf efg ) .
+
+apply ( dirprodpair isl ( weqlinvertiblerinvertible ( @op ( abmonoidfrac X A ) ) ( commax ( abmonoidfrac X A ) ) ( prabmonoidfrac X A ( pr1 a ) a' ) isl ) ) .
+Defined .
+
+
+(** **** Canonical homomorphism to the monoid of fractions *)
+
+Definition toabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) ( x : X ) : abmonoidfrac X A := setquotpr _ ( dirprodpair x ( unel A ) ) .
+
+Lemma isbinopfuntoabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : isbinopfun ( toabmonoidfrac X A ) .
+Proof . intros . unfold isbinopfun . intros x1 x2 . change ( paths ( setquotpr _ ( dirprodpair ( x1 + x2 ) ( @unel A ) ) ) ( setquotpr ( eqrelabmonoidfrac X A ) ( dirprodpair ( x1 + x2 ) ( ( unel A ) + ( unel A ) ) ) ) ) . apply ( maponpaths ( setquotpr _ ) ) . apply ( @pathsdirprod X A ) . apply idpath . apply ( pathsinv0 ( lunax A 0 ) ) . Defined .
+
+Lemma isunitalfuntoabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : paths ( toabmonoidfrac X A ( unel X ) ) ( unel ( abmonoidfrac X A ) ) .
+Proof . intros . apply idpath . Defined .
+
+Definition ismonoidfuntoabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : ismonoidfun ( toabmonoidfrac X A ) := dirprodpair ( isbinopfuntoabmonoidfrac X A ) ( isunitalfuntoabmonoidfrac X A ) .
+
+
+(** **** Abelian monoid of fractions in the case when elements of the localziation submonoid are cancelable *)
+
+Definition hrel0abmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : hrel ( dirprod X A ) := fun xa yb : setdirprod X A => eqset ( ( pr1 xa ) + ( pr1 ( pr2 yb ) ) ) ( ( pr1 yb ) + ( pr1 ( pr2 xa ) ) ) .
+
+Lemma weqhrelhrel0abmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) ( iscanc : forall a : A , isrcancelable ( @op X ) ( pr1carrier _ a ) ) ( xa xa' : dirprod X A ) : weq ( eqrelabmonoidfrac X A xa xa' ) ( hrel0abmonoidfrac X A xa xa' ) .
+Proof . intros . unfold eqrelabmonoidfrac . unfold hrelabmonoidfrac . simpl . apply weqimplimpl .
+
+apply ( @hinhuniv _ ( eqset (pr1 xa + pr1 (pr2 xa')) (pr1 xa' + pr1 (pr2 xa)) ) ) . intro ae . destruct ae as [ a eq ] . apply ( invmaponpathsincl _ ( iscanc a ) _ _ eq ) .
+intro eq . apply hinhpr . split with ( unel A ) . rewrite ( runax X ) . rewrite ( runax X ) . apply eq . apply ( isapropishinh _ ) . apply ( setproperty X ) . Defined .
+
+
+Lemma isinclprabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) ( iscanc : forall a : A , isrcancelable ( @op X ) ( pr1carrier _ a ) ) : forall a' : A , isincl ( fun x => prabmonoidfrac X A x a' ) .
+Proof . intros . apply isinclbetweensets . apply ( setproperty X ) . apply ( setproperty ( abmonoidfrac X A ) ) . intros x x' . intro e . set ( e' := invweq ( weqpathsinsetquot ( eqrelabmonoidfrac X A ) ( dirprodpair x a' ) ( dirprodpair x' a' ) ) e ) . set ( e'':= weqhrelhrel0abmonoidfrac X A iscanc ( dirprodpair _ _ ) ( dirprodpair _ _ ) e' ) . simpl in e'' . apply ( invmaponpathsincl _ ( iscanc a' ) ) . apply e'' . Defined .
+
+Definition isincltoabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) ( iscanc : forall a : A , isrcancelable ( @op X ) ( pr1carrier _ a ) ) : isincl ( toabmonoidfrac X A ) := isinclprabmonoidfrac X A iscanc ( unel A ) .
+
+
+Lemma isdeceqabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) ( iscanc : forall a : A , isrcancelable ( @op X ) ( pr1carrier _ a ) ) ( is : isdeceq X ) : isdeceq ( abmonoidfrac X A ) .
+Proof . intros . apply ( isdeceqsetquot ( eqrelabmonoidfrac X A ) ) . intros xa xa' . apply ( isdecpropweqb ( weqhrelhrel0abmonoidfrac X A iscanc xa xa' ) ) . apply isdecpropif . unfold isaprop . simpl . set ( int := setproperty X (pr1 xa + pr1 (pr2 xa')) (pr1 xa' + pr1 (pr2 xa))) . simpl in int . apply int . unfold hrel0abmonoidfrac . unfold eqset . simpl . apply ( is _ _ ) . Defined .
+
+
+
+(** **** Relations on the abelian monoid of fractions *)
+
+Definition abmonoidfracrelint ( X : abmonoid ) ( A : @subabmonoids X ) ( L : hrel X ) : hrel ( setwithbinopdirprod X A ) := fun xa yb => hexists ( fun c0 : A => L ( ( ( pr1 xa ) + ( pr1 ( pr2 yb ) ) ) + ( pr1 c0 ) ) ( ( ( pr1 yb ) + ( pr1 ( pr2 xa ) ) ) + ( pr1 c0 ) ) ) .
+
+Lemma iscomprelabmonoidfracrelint ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( is : ispartbinophrel A L ) : iscomprelrel ( eqrelabmonoidfrac X A ) ( abmonoidfracrelint X A L ) .
+Proof . intros . set ( assoc := ( assocax X ) : isassoc ( @op X ) ) . unfold isassoc in assoc . set ( comm := commax X ) . unfold iscomm in comm . set ( rer := abmonoidrer X ) . apply iscomprelrelif . apply ( eqrelsymm ( eqrelabmonoidfrac X A ) ) .
+
+intros xa xa' yb . unfold hrelabmonoidfrac . simpl . apply ( @hinhfun2 ) . intros t2e t2l . destruct t2e as [ c1a e ] . destruct t2l as [ c0a l ] . set ( x := pr1 xa ) . set ( a := pr1 ( pr2 xa ) ) . set ( x' := pr1 xa' ) . set ( a' := pr1 ( pr2 xa' ) ) . set ( y := pr1 yb ) . set ( b := pr1 ( pr2 yb ) ) . set ( c0 := pr1 c0a ) . set ( c1 := pr1 c1a ) . split with ( ( pr2 xa ) + c1a + c0a ) . change ( L ( ( x' + b ) + ( ( a + c1 ) + c0 ) ) ( ( y + a' ) + ( ( a + c1 ) + c0 ) ) ) . change ( paths ( x + a' + c1 ) ( x' + a + c1 ) ) in e . rewrite ( rer x' _ _ c0 ) . destruct ( assoc x' a c1 ) . destruct e . rewrite ( assoc x a' c1 ) . rewrite ( rer x _ _ c0 ) . rewrite ( assoc a c1 c0 ) . rewrite ( rer _ a' a _ ) . rewrite ( assoc a' c1 c0 ) . rewrite ( comm a' _ ) . rewrite ( comm c1 _ ) . rewrite ( assoc c0 c1 a' ) . destruct ( assoc ( x + b ) c0 ( @op X c1 a' ) ) . destruct ( assoc ( y + a ) c0 ( @op X c1 a' ) ) . apply ( ( pr2 is ) _ _ _ ( pr2 ( @op A c1a ( pr2 xa' ) ) ) l ) .
+
+intros xa yb yb' . unfold hrelabmonoidfrac . simpl . apply ( @hinhfun2 ) . intros t2e t2l . destruct t2e as [ c1a e ] . destruct t2l as [ c0a l ] . set ( x := pr1 xa ) . set ( a := pr1 ( pr2 xa ) ) . set ( y' := pr1 yb' ) . set ( b' := pr1 ( pr2 yb' ) ) . set ( y := pr1 yb ) . set ( b := pr1 ( pr2 yb ) ) . set ( c0 := pr1 c0a ) . set ( c1 := pr1 c1a ) . split with ( ( pr2 yb ) + c1a + c0a ) . change ( L ( ( x + b' ) + ( ( b + c1 ) + c0 ) ) ( ( y' + a ) + ( ( b + c1 ) + c0 ) ) ) . change ( paths ( y + b' + c1 ) ( y' + b + c1 ) ) in e . rewrite ( rer y' _ _ c0 ) . destruct ( assoc y' b c1 ) . destruct e . rewrite ( assoc y b' c1 ) . rewrite ( rer y _ _ c0 ) . rewrite ( assoc b c1 c0 ) . rewrite ( rer _ b' b _ ) . rewrite ( assoc b' c1 c0 ) . rewrite ( comm b' _ ) . rewrite ( comm c1 _ ) . rewrite ( assoc c0 c1 b' ) . destruct ( assoc ( x + b ) c0 ( @op X c1 b' ) ) . destruct ( assoc ( y + a ) c0 ( @op X c1 b' ) ) . apply ( ( pr2 is ) _ _ _ ( pr2 ( @op A c1a ( pr2 yb' ) ) ) l ) . Defined .
+
+Opaque iscomprelabmonoidfracrelint .
+
+Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) { L : hrel X } ( is : ispartbinophrel A L ) := quotrel ( iscomprelabmonoidfracrelint X A is ) .