diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.generic_quotient.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.generic_quotient.html | 933 |
1 files changed, 933 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html b/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html new file mode 100644 index 0000000..0faf773 --- /dev/null +++ b/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html @@ -0,0 +1,933 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>mathcomp.ssreflect.generic_quotient</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.ssreflect.generic_quotient</h1> + +<div class="code"> +<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. <br/> + -*- coding : utf-8 -*- *)</span><br/> + +<br/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + Provided a base type T, this files defines an interface for quotients Q + of the type T with explicit functions for canonical surjection (\pi + : T -> Q) and for choosing a representative (repr : Q -> T). It then + provide a helper to quotient T by a decidable equivalence relation (e + : rel T) if T is a choiceType (or encodable as a choiceType modulo e). + +<div class="paragraph"> </div> + + See "Pragamatic Quotient Types in Coq", proceedings of ITP2013, + by Cyril Cohen. + +<div class="paragraph"> </div> + +<a name="lab31"></a><h3 class="section">Generic Quotienting ***</h3> + + QuotClass (reprK : cancel repr pi) == builds the quotient which + canonical surjection function is pi and which + representative selection function is repr. + QuotType Q class == packs the quotClass class to build a quotType + You may declare such elements as Canonical + \pi_Q x == the class in Q of the element x of T + \pi x == the class of x where Q is inferred from the context + repr c == canonical representative in T of the class c + [quotType of Q] == clone of the canonical quotType structure of Q on T + x = y % [mod Q] := \pi_Q x = \pi_Q y + <-> x and y are equal modulo Q + x <> y % [mod Q] := \pi_Q x <> \pi_Q y + x == y % [mod Q] := \pi_Q x == \pi_Q y + x != y % [mod Q] := \pi_Q x != \pi_Q y + +<div class="paragraph"> </div> + + The quotient_scope is delimited by %qT + The most useful lemmas are piE and reprK + +<div class="paragraph"> </div> + +<a name="lab32"></a><h3 class="section">Morphisms ***</h3> + + One may declare existing functions and predicates as liftings of some + morphisms for a quotient. + PiMorph1 pi_f == where pi_f : {morph \pi : x / f x >-> fq x} + declares fq : Q -> Q as the lifting of f : T -> T + PiMorph2 pi_g == idem with pi_g : {morph \pi : x y / g x y >-> gq x y} + PiMono1 pi_p == idem with pi_p : {mono \pi : x / p x >-> pq x} + PiMono2 pi_r == idem with pi_r : {morph \pi : x y / r x y >-> rq x y} + PiMorph11 pi_f == idem with pi_f : {morph \pi : x / f x >-> fq x} + where fq : Q -> Q' and f : T -> T'. + PiMorph eq == Most general declaration of compatibility, + /!\ use with caution /!\ + One can use the following helpers to build the liftings which may or + may not satisfy the above properties (but if they do not, it is + probably not a good idea to define them): + lift_op1 Q f := lifts f : T -> T + lift_op2 Q g := lifts g : T -> T -> T + lift_fun1 Q p := lifts p : T -> R + lift_fun2 Q r := lifts r : T -> T -> R + lift_op11 Q Q' f := lifts f : T -> T' + There is also the special case of constants and embedding functions + that one may define and declare as compatible with Q using: + lift_cst Q x := lifts x : T to Q + PiConst c := declare the result c of the previous construction as + compatible with Q + lift_embed Q e := lifts e : R -> T to R -> Q + PiEmbed f := declare the result f of the previous construction as + compatible with Q + +<div class="paragraph"> </div> + +<a name="lab33"></a><h3 class="section">Quotients that have an eqType structure ***</h3> + + Having a canonical (eqQuotType e) structure enables piE to replace terms + of the form (x == y) by terms of the form (e x' y') if x and y are + canonical surjections of some x' and y'. + EqQuotType e Q m == builds an (eqQuotType e) structure on Q from the + morphism property m + where m : {mono \pi : x y / e x y >-> x == y} + [eqQuotType of Q] == clones the canonical eqQuotType structure of Q + +<div class="paragraph"> </div> + +<a name="lab34"></a><h3 class="section">Equivalence and quotient by an equivalence ***</h3> + + EquivRel r er es et == builds an equiv_rel structure based on the + reflexivity, symmetry and transitivity property + of a boolean relation. + {eq_quot e} == builds the quotType of T by equiv + where e : rel T is an equiv_rel + and T is a choiceType or a (choiceTypeMod e) + it is canonically an eqType, a choiceType, + a quotType and an eqQuotType. + x = y % [mod_eq e] := x = y % [mod {eq_quot e} ] + <-> x and y are equal modulo e + ... +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> + +<br/> +<span class="id" title="keyword">Reserved Notation</span> "\pi_ Q" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "\pi_ Q").<br/> +<span class="id" title="keyword">Reserved Notation</span> "\pi" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "\pi").<br/> +<span class="id" title="keyword">Reserved Notation</span> "{pi_ Q a }"<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">Q</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>, <span class="id" title="var">format</span> "{pi_ Q a }").<br/> +<span class="id" title="keyword">Reserved Notation</span> "{pi a }" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{pi a }").<br/> +<span class="id" title="keyword">Reserved Notation</span> "x == y %[mod_eq e ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/> + <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "'[hv ' x '/' == y '/' %[mod_eq e ] ']'").<br/> +<span class="id" title="keyword">Reserved Notation</span> "x = y %[mod_eq e ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/> + <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "'[hv ' x '/' = y '/' %[mod_eq e ] ']'").<br/> +<span class="id" title="keyword">Reserved Notation</span> "x != y %[mod_eq e ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/> + <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "'[hv ' x '/' != y '/' %[mod_eq e ] ']'").<br/> +<span class="id" title="keyword">Reserved Notation</span> "x <> y %[mod_eq e ]" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/> + <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "'[hv ' x '/' <> y '/' %[mod_eq e ] ']'").<br/> +<span class="id" title="keyword">Reserved Notation</span> "{eq_quot e }" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">e</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/> + <span class="id" title="var">format</span> "{eq_quot e }", <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>).<br/> + +<br/> +<span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">quotient_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">qT</span>.<br/> +<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">quotient_scope</span>.<br/> + +<br/> +</div> + +<div class="doc"> + Definition of the quotient interface. +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Section</span> <a name="QuotientDef"><span class="id" title="section">QuotientDef</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="QuotientDef.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>.<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="quot_mixin_of"><span class="id" title="record">quot_mixin_of</span></a> <span class="id" title="var">qT</span> := <a name="QuotClass"><span class="id" title="constructor">QuotClass</span></a> {<br/> + <a name="quot_repr"><span class="id" title="projection">quot_repr</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotientDef.T"><span class="id" title="variable">T</span></a>;<br/> + <a name="quot_pi"><span class="id" title="projection">quot_pi</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotientDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_repr"><span class="id" title="method">quot_repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_pi"><span class="id" title="method">quot_pi</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_mixin_of"><span class="id" title="record">quot_mixin_of</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="quotType"><span class="id" title="record">quotType</span></a> := <a name="QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> {<br/> + <a name="quot_sort"><span class="id" title="projection">quot_sort</span></a> :> <span class="id" title="keyword">Type</span>;<br/> + <a name="quot_class"><span class="id" title="projection">quot_class</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_sort"><span class="id" title="method">quot_sort</span></a>;<br/> + <span class="id" title="var">_</span> : <span class="id" title="keyword">Type</span><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="QuotType_pack"><span class="id" title="definition">QuotType_pack</span></a> <span class="id" title="var">qT</span> <span class="id" title="var">m</span> := @<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="QuotientDef.qT"><span class="id" title="variable">qT</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="pi_phant"><span class="id" title="definition">pi_phant</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotientDef.qT"><span class="id" title="variable">qT</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_pi"><span class="id" title="projection">quot_pi</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class"><span class="id" title="projection">quot_class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotientDef.qT"><span class="id" title="variable">qT</span></a>).<br/> +<span class="id" title="keyword">Definition</span> <a name="repr_of"><span class="id" title="definition">repr_of</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_repr"><span class="id" title="projection">quot_repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class"><span class="id" title="projection">quot_class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotientDef.qT"><span class="id" title="variable">qT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="repr_ofK"><span class="id" title="lemma">repr_ofK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr_of"><span class="id" title="definition">repr_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ea81395f0d53b7276a127ad9654321da"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ea81395f0d53b7276a127ad9654321da"><span class="id" title="notation">pi</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="QuotType_clone"><span class="id" title="definition">QuotType_clone</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) <span class="id" title="var">qT</span> <span class="id" title="var">cT</span> <br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class"><span class="id" title="projection">quot_class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#cT"><span class="id" title="variable">cT</span></a> := @<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotientDef"><span class="id" title="section">QuotientDef</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + Protecting some symbols. +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="PiSig"><span class="id" title="module">PiSig</span></a>.<br/> +<span class="id" title="keyword">Parameter</span> <a name="PiSig.f"><span class="id" title="axiom">f</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>), <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a>.<br/> +<span class="id" title="keyword">Axiom</span> <a name="PiSig.E"><span class="id" title="axiom">E</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiSig.f"><span class="id" title="axiom">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_phant"><span class="id" title="definition">pi_phant</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiSig"><span class="id" title="module">PiSig</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Module</span> <a name="Pi"><span class="id" title="module">Pi</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiSig"><span class="id" title="module">PiSig</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Pi.f"><span class="id" title="definition">f</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_phant"><span class="id" title="definition">pi_phant</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Pi.E"><span class="id" title="definition">E</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#erefl"><span class="id" title="abbreviation">erefl</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Pi.f"><span class="id" title="definition">f</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Pi"><span class="id" title="module">Pi</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Module</span> <a name="MPi"><span class="id" title="module">MPi</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiSig"><span class="id" title="module">PiSig</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="MPi.f"><span class="id" title="definition">f</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_phant"><span class="id" title="definition">pi_phant</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="MPi.E"><span class="id" title="definition">E</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#erefl"><span class="id" title="abbreviation">erefl</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#MPi.f"><span class="id" title="definition">f</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#MPi"><span class="id" title="module">MPi</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="ReprSig"><span class="id" title="module">ReprSig</span></a>.<br/> +<span class="id" title="keyword">Parameter</span> <a name="ReprSig.f"><span class="id" title="axiom">f</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>), <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>.<br/> +<span class="id" title="keyword">Axiom</span> <a name="ReprSig.E"><span class="id" title="axiom">E</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ReprSig.f"><span class="id" title="axiom">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr_of"><span class="id" title="definition">repr_of</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ReprSig"><span class="id" title="module">ReprSig</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Module</span> <a name="Repr"><span class="id" title="module">Repr</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ReprSig"><span class="id" title="module">ReprSig</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Repr.f"><span class="id" title="definition">f</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr_of"><span class="id" title="definition">repr_of</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Repr.E"><span class="id" title="definition">E</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#erefl"><span class="id" title="abbreviation">erefl</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Repr.f"><span class="id" title="definition">f</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Repr"><span class="id" title="module">Repr</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + Fancy Notations +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="repr"><span class="id" title="abbreviation">repr</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f"><span class="id" title="axiom">Repr.f</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">"</span></a>\pi_ Q" := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f"><span class="id" title="axiom">Pi.f</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">Q</span>)) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="f090f187f28139994197271ddc594c91"><span class="id" title="notation">"</span></a>\pi" := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f"><span class="id" title="axiom">Pi.f</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">_</span>)) (<span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="433801266bfe38f0ebd6037860203596"><span class="id" title="notation">"</span></a>x == y %[mod Q ]" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">"</span></a>x = y %[mod Q ]" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">"</span></a>x != y %[mod Q ]" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">"</span></a>x <> y %[mod Q ]" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">quotient_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">mpi_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#E"><span class="id" title="axiom">MPi.E</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#E"><span class="id" title="axiom">Pi.E</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">repr_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#E"><span class="id" title="axiom">Repr.E</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_mixin_of"><span class="id" title="record">quot_mixin_of</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="QuotType"><span class="id" title="abbreviation">QuotType</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">m</span> := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotType_pack"><span class="id" title="definition">QuotType_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">Q</span> <span class="id" title="var">m</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">"</span></a>[ 'quotType' 'of' Q ]" := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotType_clone"><span class="id" title="definition">QuotType_clone</span></a> <span class="id" title="var">_</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'quotType' 'of' Q ]") : <span class="id" title="var">form_scope</span>.<br/> + +<br/> + +<br/> +</div> + +<div class="doc"> + Exporting the theory +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Section</span> <a name="QuotTypeTheory"><span class="id" title="section">QuotTypeTheory</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="QuotTypeTheory.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>.<br/> +<span class="id" title="keyword">Variable</span> <a name="QuotTypeTheory.qT"><span class="id" title="variable">qT</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.T"><span class="id" title="variable">T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="reprK"><span class="id" title="lemma">reprK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">CoInductive</span> <a name="pi_spec"><span class="id" title="inductive">pi_spec</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span> :=<br/> + <a name="PiSpec"><span class="id" title="constructor">PiSpec</span></a> <span class="id" title="var">y</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.qT"><span class="id" title="variable">qT</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">]</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_spec"><span class="id" title="inductive">pi_spec</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="piP"><span class="id" title="lemma">piP</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_spec"><span class="id" title="inductive">pi_spec</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="mpiE"><span class="id" title="lemma">mpiE</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#8ca1ec8fcbe3863f23d46cc84b94a995"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#8ca1ec8fcbe3863f23d46cc84b94a995"><span class="id" title="notation">mpi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="quotW"><span class="id" title="lemma">quotW</span></a> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.T"><span class="id" title="variable">T</span></a>, <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#P"><span class="id" title="variable">P</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.qT"><span class="id" title="variable">qT</span></a>, <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="quotP"><span class="id" title="lemma">quotP</span></a> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.T"><span class="id" title="variable">T</span></a>, <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#P"><span class="id" title="variable">P</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory.qT"><span class="id" title="variable">qT</span></a>, <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypeTheory"><span class="id" title="section">QuotTypeTheory</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + About morphisms +<div class="paragraph"> </div> + + This was pi_morph T (x : T) := PiMorph { pi_op : T; _ : x = pi_op }. +</div> +<div class="code"> +<span class="id" title="keyword">Structure</span> <a name="equal_to"><span class="id" title="record">equal_to</span></a> <span class="id" title="var">T</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) := <a name="EqualTo"><span class="id" title="constructor">EqualTo</span></a> {<br/> + <a name="equal_val"><span class="id" title="projection">equal_val</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="method">equal_val</span></a><br/> +}.<br/> +<span class="id" title="keyword">Lemma</span> <a name="equal_toE"><span class="id" title="lemma">equal_toE</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_to"><span class="id" title="record">equal_to</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="projection">equal_val</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="piE"><span class="id" title="abbreviation">piE</span></a> := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_toE"><span class="id" title="lemma">equal_toE</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>).<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">equal_to_pi</span> <span class="id" title="var">T</span> (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) :=<br/> + @<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#erefl"><span class="id" title="abbreviation">erefl</span></a> <span class="id" title="var">_</span>).<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Morphism"><span class="id" title="section">Morphism</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> <a name="Morphism.T"><span class="id" title="variable">T</span></a> <a name="Morphism.U"><span class="id" title="variable">U</span></a> : <span class="id" title="keyword">Type</span>.<br/> +<span class="id" title="keyword">Variable</span> (<a name="Morphism.qT"><span class="id" title="variable">qT</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a>).<br/> +<span class="id" title="keyword">Variable</span> (<a name="Morphism.qU"><span class="id" title="variable">qU</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.U"><span class="id" title="variable">U</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Variable</span> (<a name="Morphism.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a>) (<a name="Morphism.g"><span class="id" title="variable">g</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a>) (<a name="Morphism.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.U"><span class="id" title="variable">U</span></a>) (<a name="Morphism.r"><span class="id" title="variable">r</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.U"><span class="id" title="variable">U</span></a>).<br/> +<span class="id" title="keyword">Variable</span> (<a name="Morphism.fq"><span class="id" title="variable">fq</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a>) (<a name="Morphism.gq"><span class="id" title="variable">gq</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a>) (<a name="Morphism.pq"><span class="id" title="variable">pq</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.U"><span class="id" title="variable">U</span></a>) (<a name="Morphism.rq"><span class="id" title="variable">rq</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.U"><span class="id" title="variable">U</span></a>).<br/> +<span class="id" title="keyword">Variable</span> (<a name="Morphism.h"><span class="id" title="variable">h</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.U"><span class="id" title="variable">U</span></a>) (<a name="Morphism.hq"><span class="id" title="variable">hq</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.qU"><span class="id" title="variable">qU</span></a>).<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Morphism.pi_f"><span class="id" title="variable">pi_f</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.fq"><span class="id" title="variable">fq</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Morphism.pi_g"><span class="id" title="variable">pi_g</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.gq"><span class="id" title="variable">gq</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Morphism.pi_p"><span class="id" title="variable">pi_p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.pq"><span class="id" title="variable">pq</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fcecf6c7c5b99f975a4e95451ce580e5"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Morphism.pi_r"><span class="id" title="variable">pi_r</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.rq"><span class="id" title="variable">rq</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Morphism.pi_h"><span class="id" title="variable">pi_h</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a>), <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qU</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.hq"><span class="id" title="variable">hq</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="Morphism.a"><span class="id" title="variable">a</span></a> <a name="Morphism.b"><span class="id" title="variable">b</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.T"><span class="id" title="variable">T</span></a>) (<a name="Morphism.x"><span class="id" title="variable">x</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_to"><span class="id" title="record">equal_to</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a>)) (<a name="Morphism.y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_to"><span class="id" title="record">equal_to</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b"><span class="id" title="variable">b</span></a>)).<br/> + +<br/> +</div> + +<div class="doc"> + Internal Lemmmas : do not use directly +</div> +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="pi_morph1"><span class="id" title="lemma">pi_morph1</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">f</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.fq"><span class="id" title="variable">fq</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="projection">equal_val</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.x"><span class="id" title="variable">x</span></a>). <br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_morph2"><span class="id" title="lemma">pi_morph2</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">g</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">b</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.gq"><span class="id" title="variable">gq</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="projection">equal_val</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="projection">equal_val</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.y"><span class="id" title="variable">y</span></a>). <br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_mono1"><span class="id" title="lemma">pi_mono1</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.pq"><span class="id" title="variable">pq</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="projection">equal_val</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.x"><span class="id" title="variable">x</span></a>). <br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_mono2"><span class="id" title="lemma">pi_mono2</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.rq"><span class="id" title="variable">rq</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="projection">equal_val</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="projection">equal_val</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.y"><span class="id" title="variable">y</span></a>). <br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_morph11"><span class="id" title="lemma">pi_morph11</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">h</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.hq"><span class="id" title="variable">hq</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_val"><span class="id" title="projection">equal_val</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism.x"><span class="id" title="variable">x</span></a>). <br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Morphism"><span class="id" title="section">Morphism</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="d589722c5f693f7a057267b2fb730ebf"><span class="id" title="notation">"</span></a>{pi_ Q a }" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_to"><span class="id" title="record">equal_to</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">a</span>)) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">"</span></a>{pi a }" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equal_to"><span class="id" title="record">equal_to</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">a</span></a>)) : <span class="id" title="var">quotient_scope</span>.<br/> + +<br/> +</div> + +<div class="doc"> + Declaration of morphisms +</div> +<div class="code"> +<span class="id" title="keyword">Notation</span> <a name="PiMorph"><span class="id" title="abbreviation">PiMorph</span></a> <span class="id" title="var">pi_x</span> := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> <span class="id" title="var">pi_x</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="PiMorph1"><span class="id" title="abbreviation">PiMorph1</span></a> <span class="id" title="var">pi_f</span> :=<br/> + (<span class="id" title="keyword">fun</span> <span class="id" title="var">a</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">}</span></a>) ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_morph1"><span class="id" title="lemma">pi_morph1</span></a> <span class="id" title="var">pi_f</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="PiMorph2"><span class="id" title="abbreviation">PiMorph2</span></a> <span class="id" title="var">pi_g</span> :=<br/> + (<span class="id" title="keyword">fun</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">}</span></a>) ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_morph2"><span class="id" title="lemma">pi_morph2</span></a> <span class="id" title="var">pi_g</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="PiMono1"><span class="id" title="abbreviation">PiMono1</span></a> <span class="id" title="var">pi_p</span> :=<br/> + (<span class="id" title="keyword">fun</span> <span class="id" title="var">a</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">}</span></a>) ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_mono1"><span class="id" title="lemma">pi_mono1</span></a> <span class="id" title="var">pi_p</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="PiMono2"><span class="id" title="abbreviation">PiMono2</span></a> <span class="id" title="var">pi_r</span> :=<br/> + (<span class="id" title="keyword">fun</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">}</span></a>) ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_mono2"><span class="id" title="lemma">pi_mono2</span></a> <span class="id" title="var">pi_r</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="PiMorph11"><span class="id" title="abbreviation">PiMorph11</span></a> <span class="id" title="var">pi_f</span> :=<br/> + (<span class="id" title="keyword">fun</span> <span class="id" title="var">a</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#00d3e1ef19e0b132c50cc1db7d7746c2"><span class="id" title="notation">}</span></a>) ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_morph11"><span class="id" title="lemma">pi_morph11</span></a> <span class="id" title="var">pi_f</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)).<br/> + +<br/> +</div> + +<div class="doc"> + lifiting helpers +</div> +<div class="code"> +<span class="id" title="keyword">Notation</span> <a name="lift_op1"><span class="id" title="abbreviation">lift_op1</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">f</span> := (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <span class="id" title="var">Q</span> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> (<span class="id" title="var">f</span> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <span class="id" title="var">Q</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="lift_op2"><span class="id" title="abbreviation">lift_op2</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">g</span> := <br/> + (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <span class="id" title="var">Q</span> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> (<span class="id" title="var">g</span> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <span class="id" title="var">Q</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="lift_fun1"><span class="id" title="abbreviation">lift_fun1</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">f</span> := (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <span class="id" title="var">Q</span> ⇒ <span class="id" title="var">f</span> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>))).<br/> +<span class="id" title="keyword">Notation</span> <a name="lift_fun2"><span class="id" title="abbreviation">lift_fun2</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">g</span> := (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <span class="id" title="var">Q</span> ⇒ <span class="id" title="var">g</span> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>))).<br/> +<span class="id" title="keyword">Notation</span> <a name="lift_op11"><span class="id" title="abbreviation">lift_op11</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">Q'</span> <span class="id" title="var">f</span> := (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <span class="id" title="var">Q</span> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q'</span></a> (<span class="id" title="var">f</span> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <span class="id" title="var">Q'</span>)).<br/> + +<br/> +</div> + +<div class="doc"> + constant declaration +</div> +<div class="code"> +<span class="id" title="keyword">Notation</span> <a name="lift_cst"><span class="id" title="abbreviation">lift_cst</span></a> <span class="id" title="var">Q</span> <span class="id" title="var">x</span> := (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <span class="id" title="var">Q</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="PiConst"><span class="id" title="abbreviation">PiConst</span></a> <span class="id" title="var">a</span> := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">a</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#lock"><span class="id" title="lemma">lock</span></a> <span class="id" title="var">_</span>)).<br/> + +<br/> +</div> + +<div class="doc"> + embedding declaration, please don't redefine \pi +</div> +<div class="code"> +<span class="id" title="keyword">Notation</span> <a name="lift_embed"><span class="id" title="abbreviation">lift_embed</span></a> <span class="id" title="var">qT</span> <span class="id" title="var">e</span> := (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> (<span class="id" title="var">e</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <span class="id" title="var">qT</span>)).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_lock"><span class="id" title="lemma">eq_lock</span></a> <span class="id" title="var">T</span> <span class="id" title="var">T'</span> <span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">(</span></a>@<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T'"><span class="id" title="variable">T'</span></a>) (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="PiEmbed"><span class="id" title="abbreviation">PiEmbed</span></a> <span class="id" title="var">e</span> := <br/> + (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ @<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqualTo"><span class="id" title="constructor">EqualTo</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<span class="id" title="var">e</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_lock"><span class="id" title="lemma">eq_lock</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">_</span></a>) <span class="id" title="var">_</span>)).<br/> + +<br/> +</div> + +<div class="doc"> + About eqQuotType +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Section</span> <a name="EqQuotTypeStructure"><span class="id" title="section">EqQuotTypeStructure</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="EqQuotTypeStructure.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>.<br/> +<span class="id" title="keyword">Variable</span> <a name="EqQuotTypeStructure.eq_quot_op"><span class="id" title="variable">eq_quot_op</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypeStructure.T"><span class="id" title="variable">T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="eq_quot_mixin_of"><span class="id" title="definition">eq_quot_mixin_of</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">qc</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypeStructure.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a>)<br/> + (<span class="id" title="var">ec</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.class_of"><span class="id" title="abbreviation">Equality.class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a>) :=<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotTypePack"><span class="id" title="constructor">QuotTypePack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">/</span></a><br/> + <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypeStructure.eq_quot_op"><span class="id" title="variable">eq_quot_op</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">>-></span></a> @<a class="idref" href="mathcomp.ssreflect.eqtype.html#eq_op"><span class="id" title="definition">eq_op</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Pack"><span class="id" title="constructor">Equality.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec"><span class="id" title="variable">ec</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="eq_quot_class_of"><span class="id" title="record">eq_quot_class_of</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a name="EqQuotClass"><span class="id" title="constructor">EqQuotClass</span></a> {<br/> + <a name="eq_quot_quot_class"><span class="id" title="projection">eq_quot_quot_class</span></a> :> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class_of"><span class="id" title="abbreviation">quot_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypeStructure.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <a name="eq_quot_eq_mixin"><span class="id" title="projection">eq_quot_eq_mixin</span></a> :> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.class_of"><span class="id" title="abbreviation">Equality.class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a>;<br/> + <a name="pi_eq_quot_mixin"><span class="id" title="projection">pi_eq_quot_mixin</span></a> :> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_mixin_of"><span class="id" title="definition">eq_quot_mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_quot_class"><span class="id" title="method">eq_quot_quot_class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_eq_mixin"><span class="id" title="method">eq_quot_eq_mixin</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="eqQuotType"><span class="id" title="record">eqQuotType</span></a> : <span class="id" title="keyword">Type</span> := <a name="EqQuotTypePack"><span class="id" title="constructor">EqQuotTypePack</span></a> {<br/> + <a name="eq_quot_sort"><span class="id" title="projection">eq_quot_sort</span></a> :> <span class="id" title="keyword">Type</span>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class_of"><span class="id" title="record">eq_quot_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_sort"><span class="id" title="method">eq_quot_sort</span></a>;<br/> + <span class="id" title="var">_</span> : <span class="id" title="keyword">Type</span><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">eqT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType"><span class="id" title="record">eqQuotType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="eq_quot_class"><span class="id" title="definition">eq_quot_class</span></a> <span class="id" title="var">eqT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class_of"><span class="id" title="record">eq_quot_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqT"><span class="id" title="variable">eqT</span></a> :=<br/> + <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypePack"><span class="id" title="constructor">EqQuotTypePack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">cT</span> <span class="id" title="var">_</span> <span class="id" title="keyword">as</span> <span class="id" title="var">qT'</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqT"><span class="id" title="variable">eqT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class_of"><span class="id" title="record">eq_quot_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT'"><span class="id" title="variable">qT'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">cT</span>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqQuotType_eqType</span> <span class="id" title="var">eqT</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqT"><span class="id" title="variable">eqT</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class"><span class="id" title="definition">eq_quot_class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqT"><span class="id" title="variable">eqT</span></a>).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqQuotType_quotType</span> <span class="id" title="var">eqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotType"><span class="id" title="abbreviation">QuotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqT"><span class="id" title="variable">eqT</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class"><span class="id" title="definition">eq_quot_class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqT"><span class="id" title="variable">eqT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_eqType"><span class="id" title="definition">eqQuotType_eqType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_eqType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_eqType"><span class="id" title="definition">eqQuotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_eqType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_eqType"><span class="id" title="definition">eqType</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_quotType"><span class="id" title="definition">eqQuotType_quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_quotType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_quotType"><span class="id" title="definition">eqQuotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_quotType"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType_quotType"><span class="id" title="definition">quotType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="EqQuotType_pack"><span class="id" title="definition">EqQuotType_pack</span></a> <span class="id" title="var">Q</span> :=<br/> + <span class="id" title="keyword">fun</span> (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypeStructure.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">eT</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) <span class="id" title="var">qc</span> <span class="id" title="var">ec</span> <br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quot_class"><span class="id" title="projection">quot_class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qc"><span class="id" title="variable">qc</span></a> & <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.class"><span class="id" title="definition">Equality.class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eT"><span class="id" title="variable">eT</span></a>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec"><span class="id" title="variable">ec</span></a> ⇒ <br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">m</span> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypePack"><span class="id" title="constructor">EqQuotTypePack</span></a> (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotClass"><span class="id" title="constructor">EqQuotClass</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qc"><span class="id" title="variable">qc</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec"><span class="id" title="variable">ec</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="EqQuotType_clone"><span class="id" title="definition">EqQuotType_clone</span></a> (<span class="id" title="var">Q</span> : <span class="id" title="keyword">Type</span>) <span class="id" title="var">eqT</span> <span class="id" title="var">cT</span> <br/> + <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_class"><span class="id" title="definition">eq_quot_class</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqT"><span class="id" title="variable">eqT</span></a>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#cT"><span class="id" title="variable">cT</span></a> := @<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypePack"><span class="id" title="constructor">EqQuotTypePack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Q"><span class="id" title="variable">Q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_eq_quot"><span class="id" title="lemma">pi_eq_quot</span></a> <span class="id" title="var">eqT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_eqT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypeStructure.eq_quot_op"><span class="id" title="variable">eq_quot_op</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#aed5e67b67900c70888bda2ff72f1de4"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_eq_quot_mono</span> <span class="id" title="var">eqT</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMono2"><span class="id" title="abbreviation">PiMono2</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#pi_eq_quot"><span class="id" title="lemma">pi_eq_quot</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqT"><span class="id" title="variable">eqT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTypeStructure"><span class="id" title="section">EqQuotTypeStructure</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="EqQuotType"><span class="id" title="abbreviation">EqQuotType</span></a> <span class="id" title="var">e</span> <span class="id" title="var">Q</span> <span class="id" title="var">m</span> := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotType_pack"><span class="id" title="definition">EqQuotType_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">e</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">m</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">"</span></a>[ 'eqQuotType' e 'of' Q ]" := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotType_clone"><span class="id" title="definition">EqQuotType_clone</span></a> <span class="id" title="var">_</span> <span class="id" title="var">e</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'eqQuotType' e 'of' Q ]") : <span class="id" title="var">form_scope</span>.<br/> + +<br/> +</div> + +<div class="doc"> + Even if a quotType is a natural subType, we do not make this subType + canonical, to allow the user to define the subtyping he wants. However + one can: +<ul class="doclist"> +<li> get the eqMixin and the choiceMixin by subtyping + +</li> +<li> get the subType structure and maybe declare it Canonical. +</li> +</ul> + +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Module</span> <a name="QuotSubType"><span class="id" title="module">QuotSubType</span></a>.<br/> +<span class="id" title="keyword">Section</span> <a name="QuotSubType.SubTypeMixin"><span class="id" title="section">SubTypeMixin</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="QuotSubType.SubTypeMixin.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>.<br/> +<span class="id" title="keyword">Variable</span> <a name="QuotSubType.SubTypeMixin.qT"><span class="id" title="variable">qT</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.SubTypeMixin.T"><span class="id" title="variable">T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="QuotSubType.Sub"><span class="id" title="definition">Sub</span></a> <span class="id" title="var">x</span> (<span class="id" title="var">px</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="QuotSubType.qreprK"><span class="id" title="lemma">qreprK</span></a> <span class="id" title="var">x</span> <span class="id" title="var">Px</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.Sub"><span class="id" title="definition">Sub</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Px"><span class="id" title="variable">Px</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="QuotSubType.sortPx"><span class="id" title="lemma">sortPx</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.SubTypeMixin.qT"><span class="id" title="variable">qT</span></a>) : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_qT</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="QuotSubType.sort_Sub"><span class="id" title="lemma">sort_Sub</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.SubTypeMixin.qT"><span class="id" title="variable">qT</span></a>) : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.Sub"><span class="id" title="definition">Sub</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.sortPx"><span class="id" title="lemma">sortPx</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="QuotSubType.reprP"><span class="id" title="lemma">reprP</span></a> <span class="id" title="var">K</span> (<span class="id" title="var">PK</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">Px</span>, <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#K"><span class="id" title="variable">K</span></a> (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.Sub"><span class="id" title="definition">Sub</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#Px"><span class="id" title="variable">Px</span></a>)) <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#u"><span class="id" title="variable">u</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">subType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#SubType"><span class="id" title="constructor">SubType</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.reprP"><span class="id" title="lemma">reprP</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.qreprK"><span class="id" title="lemma">qreprK</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="QuotSubType.eqMixin"><span class="id" title="definition">eqMixin</span></a> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.SubTypeMixin.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation"><:]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.SubTypeMixin.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.eqMixin"><span class="id" title="definition">eqMixin</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.SubTypeMixin"><span class="id" title="section">SubTypeMixin</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="QuotSubType.choiceMixin"><span class="id" title="definition">choiceMixin</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) :=<br/> + <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">choiceType</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a> (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.choiceMixin"><span class="id" title="definition">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="QuotSubType.countMixin"><span class="id" title="definition">countMixin</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) :=<br/> + <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">countType</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) (<span class="id" title="var">qT</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a> (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.countMixin"><span class="id" title="definition">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qT"><span class="id" title="variable">qT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="QuotSubType.finType"><span class="id" title="section">finType</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="QuotSubType.finType.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="QuotSubType.finType.qT"><span class="id" title="variable">qT</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#quotType"><span class="id" title="record">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">subCountType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.finType.qT"><span class="id" title="variable">qT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="QuotSubType.finMixin"><span class="id" title="definition">finMixin</span></a> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.finType.qT"><span class="id" title="variable">qT</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType.finType"><span class="id" title="section">finType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotSubType"><span class="id" title="module">QuotSubType</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="d742d727e2d59dc6166ae1de34a4d8ac"><span class="id" title="notation">"</span></a>[ 'subType' Q 'of' T 'by' %/ ]" :=<br/> +(@<a class="idref" href="mathcomp.ssreflect.eqtype.html#SubType"><span class="id" title="constructor">SubType</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">Q</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#reprP"><span class="id" title="lemma">QuotSubType.reprP</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>) (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#qreprK"><span class="id" title="lemma">QuotSubType.qreprK</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>))<br/> +(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'subType' Q 'of' T 'by' %/ ]") : <span class="id" title="var">form_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="7435dce9122598a71cc10264af72d448"><span class="id" title="notation">"</span></a>[ 'eqMixin' 'of' Q 'by' <:%/ ]" := <br/> + (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqMixin"><span class="id" title="definition">QuotSubType.eqMixin</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.class_of"><span class="id" title="abbreviation">Equality.class_of</span></a> <span class="id" title="var">Q</span>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'eqMixin' 'of' Q 'by' <:%/ ]") : <span class="id" title="var">form_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="a1351eda67af6754507914014591d475"><span class="id" title="notation">"</span></a>[ 'choiceMixin' 'of' Q 'by' <:%/ ]" := <br/> + (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#choiceMixin"><span class="id" title="definition">QuotSubType.choiceMixin</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.mixin_of"><span class="id" title="record">Choice.mixin_of</span></a> <span class="id" title="var">Q</span>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'choiceMixin' 'of' Q 'by' <:%/ ]") : <span class="id" title="var">form_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="fe775fb80a928ad3cb11ed2321d0ade9"><span class="id" title="notation">"</span></a>[ 'countMixin' 'of' Q 'by' <:%/ ]" := <br/> + (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#countMixin"><span class="id" title="definition">QuotSubType.countMixin</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin_of"><span class="id" title="record">Countable.mixin_of</span></a> <span class="id" title="var">Q</span>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'countMixin' 'of' Q 'by' <:%/ ]") : <span class="id" title="var">form_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="28958bf2299a14c58256988b5130e610"><span class="id" title="notation">"</span></a>[ 'finMixin' 'of' Q 'by' <:%/ ]" := <br/> + (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#finMixin"><span class="id" title="definition">QuotSubType.finMixin</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.mixin_of"><span class="id" title="record">Finite.mixin_of</span></a> <span class="id" title="var">Q</span>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'finMixin' 'of' Q 'by' <:%/ ]") : <span class="id" title="var">form_scope</span>.<br/> + +<br/> +</div> + +<div class="doc"> + Definition of a (decidable) equivalence relation +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Section</span> <a name="EquivRel"><span class="id" title="section">EquivRel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="EquivRel.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="left_trans"><span class="id" title="lemma">left_trans</span></a> (<span class="id" title="var">e</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.T"><span class="id" title="variable">T</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#symmetric"><span class="id" title="definition">symmetric</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#left_transitive"><span class="id" title="definition">left_transitive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="right_trans"><span class="id" title="lemma">right_trans</span></a> (<span class="id" title="var">e</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.T"><span class="id" title="variable">T</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#symmetric"><span class="id" title="definition">symmetric</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#right_transitive"><span class="id" title="definition">right_transitive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a>.<br/> + +<br/> +<span class="id" title="keyword">CoInductive</span> <a name="equiv_class_of"><span class="id" title="inductive">equiv_class_of</span></a> (<span class="id" title="var">equiv</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.T"><span class="id" title="variable">T</span></a>) :=<br/> + <a name="EquivClass"><span class="id" title="constructor">EquivClass</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflexive"><span class="id" title="definition">reflexive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv"><span class="id" title="variable">equiv</span></a> & <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#symmetric"><span class="id" title="definition">symmetric</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv"><span class="id" title="variable">equiv</span></a> & <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv"><span class="id" title="variable">equiv</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="equiv_rel"><span class="id" title="record">equiv_rel</span></a> := <a name="EquivRelPack"><span class="id" title="constructor">EquivRelPack</span></a> {<br/> + <a name="equiv"><span class="id" title="projection">equiv</span></a> :> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.T"><span class="id" title="variable">T</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_class_of"><span class="id" title="inductive">equiv_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv"><span class="id" title="method">equiv</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="EquivRel.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_rel"><span class="id" title="record">equiv_rel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="equiv_class"><span class="id" title="definition">equiv_class</span></a> :=<br/> + <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRelPack"><span class="id" title="constructor">EquivRelPack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">ce</span> <span class="id" title="keyword">as</span> <span class="id" title="var">e'</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.e"><span class="id" title="variable">e</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_class_of"><span class="id" title="inductive">equiv_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e'"><span class="id" title="variable">e'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">ce</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="equiv_pack"><span class="id" title="definition">equiv_pack</span></a> (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">ce</span> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ce"><span class="id" title="variable">ce</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_class"><span class="id" title="definition">equiv_class</span></a> :=<br/> + @<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRelPack"><span class="id" title="constructor">EquivRelPack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ce"><span class="id" title="variable">ce</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="equiv_refl"><span class="id" title="lemma">equiv_refl</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="equiv_sym"><span class="id" title="lemma">equiv_sym</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#symmetric"><span class="id" title="definition">symmetric</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.e"><span class="id" title="variable">e</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="equiv_trans"><span class="id" title="lemma">equiv_trans</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.e"><span class="id" title="variable">e</span></a>. <br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_op_trans"><span class="id" title="lemma">eq_op_trans</span></a> (<span class="id" title="var">T'</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> (@<a class="idref" href="mathcomp.ssreflect.eqtype.html#eq_op"><span class="id" title="definition">eq_op</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T'"><span class="id" title="variable">T'</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="equiv_ltrans"><span class="id" title="lemma">equiv_ltrans</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#left_transitive"><span class="id" title="definition">left_transitive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.e"><span class="id" title="variable">e</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="equiv_rtrans"><span class="id" title="lemma">equiv_rtrans</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#right_transitive"><span class="id" title="definition">right_transitive</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel.e"><span class="id" title="variable">e</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel"><span class="id" title="section">EquivRel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">equiv_refl</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="EquivRel"><span class="id" title="abbreviation">EquivRel</span></a> <span class="id" title="var">r</span> <span class="id" title="var">er</span> <span class="id" title="var">es</span> <span class="id" title="var">et</span> := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRelPack"><span class="id" title="constructor">EquivRelPack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">r</span> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivClass"><span class="id" title="constructor">EquivClass</span></a> <span class="id" title="var">er</span> <span class="id" title="var">es</span> <span class="id" title="var">et</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="d18580a19ed48e5e2474d6b85859423a"><span class="id" title="notation">"</span></a>[ 'equiv_rel' 'of' e ]" := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_pack"><span class="id" title="definition">equiv_pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">e</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'equiv_rel' 'of' e ]") : <span class="id" title="var">form_scope</span>.<br/> + +<br/> +</div> + +<div class="doc"> + Encoding to another type modulo an equivalence +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Section</span> <a name="EncodingModuloRel"><span class="id" title="section">EncodingModuloRel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="EncodingModuloRel.D"><span class="id" title="variable">D</span></a> <a name="EncodingModuloRel.E"><span class="id" title="variable">E</span></a> : <span class="id" title="keyword">Type</span>) (<a name="EncodingModuloRel.ED"><span class="id" title="variable">ED</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a>) (<a name="EncodingModuloRel.DE"><span class="id" title="variable">DE</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#E"><span class="id" title="variable">E</span></a>) (<a name="EncodingModuloRel.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a>).<br/> + +<br/> +<span class="id" title="keyword">CoInductive</span> <a name="encModRel_class_of"><span class="id" title="inductive">encModRel_class_of</span></a> (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.D"><span class="id" title="variable">D</span></a>) :=<br/> + <a name="EncModRelClassPack"><span class="id" title="constructor">EncModRelClassPack</span></a> <span class="id" title="keyword">of</span> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.ED"><span class="id" title="variable">ED</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.DE"><span class="id" title="variable">DE</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) & (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.e"><span class="id" title="variable">e</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="encModRel"><span class="id" title="record">encModRel</span></a> := <a name="EncModRelPack"><span class="id" title="constructor">EncModRelPack</span></a> {<br/> + <a name="enc_mod_rel"><span class="id" title="projection">enc_mod_rel</span></a> :> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.D"><span class="id" title="variable">D</span></a>;<br/> + <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encModRel_class_of"><span class="id" title="inductive">encModRel_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#enc_mod_rel"><span class="id" title="method">enc_mod_rel</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="EncodingModuloRel.r"><span class="id" title="variable">r</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encModRel"><span class="id" title="record">encModRel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="encModRelClass"><span class="id" title="definition">encModRelClass</span></a> := <br/> + <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncModRelPack"><span class="id" title="constructor">EncModRelPack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">c</span> <span class="id" title="keyword">as</span> <span class="id" title="var">r'</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encModRel_class_of"><span class="id" title="inductive">encModRel_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#r'"><span class="id" title="variable">r'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">c</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="encModRelP"><span class="id" title="definition">encModRelP</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.D"><span class="id" title="variable">D</span></a>) : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.ED"><span class="id" title="variable">ED</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.DE"><span class="id" title="variable">DE</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="encModRelE"><span class="id" title="definition">encModRelE</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.r"><span class="id" title="variable">r</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.e"><span class="id" title="variable">e</span></a>. <br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="encoded_equiv"><span class="id" title="definition">encoded_equiv</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.E"><span class="id" title="variable">E</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.ED"><span class="id" title="variable">ED</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel.ED"><span class="id" title="variable">ED</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloRel"><span class="id" title="section">EncodingModuloRel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="EncModRelClass"><span class="id" title="abbreviation">EncModRelClass</span></a> <span class="id" title="var">m</span> :=<br/> + (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncModRelClassPack"><span class="id" title="constructor">EncModRelClassPack</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">_</span> ⇒ <span class="id" title="var">m</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#erefl"><span class="id" title="abbreviation">erefl</span></a> <span class="id" title="var">_</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="EncModRel"><span class="id" title="abbreviation">EncModRel</span></a> <span class="id" title="var">r</span> <span class="id" title="var">m</span> := (@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncModRelPack"><span class="id" title="constructor">EncModRelPack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">r</span> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncModRelClass"><span class="id" title="abbreviation">EncModRelClass</span></a> <span class="id" title="var">m</span>)).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="EncodingModuloEquiv"><span class="id" title="section">EncodingModuloEquiv</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="EncodingModuloEquiv.D"><span class="id" title="variable">D</span></a> <a name="EncodingModuloEquiv.E"><span class="id" title="variable">E</span></a> : <span class="id" title="keyword">Type</span>) (<a name="EncodingModuloEquiv.ED"><span class="id" title="variable">ED</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a>) (<a name="EncodingModuloEquiv.DE"><span class="id" title="variable">DE</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#E"><span class="id" title="variable">E</span></a>) (<a name="EncodingModuloEquiv.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_rel"><span class="id" title="record">equiv_rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a>).<br/> +<span class="id" title="keyword">Variable</span> (<a name="EncodingModuloEquiv.r"><span class="id" title="variable">r</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encModRel"><span class="id" title="record">encModRel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.ED"><span class="id" title="variable">ED</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.DE"><span class="id" title="variable">DE</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.e"><span class="id" title="variable">e</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="enc_mod_rel_is_equiv"><span class="id" title="lemma">enc_mod_rel_is_equiv</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_class_of"><span class="id" title="inductive">equiv_class_of</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#enc_mod_rel"><span class="id" title="projection">enc_mod_rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.r"><span class="id" title="variable">r</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="enc_mod_rel_equiv_rel"><span class="id" title="definition">enc_mod_rel_equiv_rel</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRelPack"><span class="id" title="constructor">EquivRelPack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#enc_mod_rel_is_equiv"><span class="id" title="lemma">enc_mod_rel_is_equiv</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="encModEquivP"><span class="id" title="definition">encModEquivP</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.D"><span class="id" title="variable">D</span></a>) : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.ED"><span class="id" title="variable">ED</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.DE"><span class="id" title="variable">DE</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="encoded_equivE"><span class="id" title="lemma">encoded_equivE</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e'"><span class="id" title="abbreviation">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.ED"><span class="id" title="variable">ED</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.ED"><span class="id" title="variable">ED</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="encoded_equiv_is_equiv"><span class="id" title="lemma">encoded_equiv_is_equiv</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_class_of"><span class="id" title="inductive">equiv_class_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e'"><span class="id" title="abbreviation">e'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">encoded_equiv_equiv_rel</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRelPack"><span class="id" title="constructor">EquivRelPack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encoded_equiv_is_equiv"><span class="id" title="lemma">encoded_equiv_is_equiv</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="encoded_equivP"><span class="id" title="lemma">encoded_equivP</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e'"><span class="id" title="abbreviation">e'</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.DE"><span class="id" title="variable">DE</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv.ED"><span class="id" title="variable">ED</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncodingModuloEquiv"><span class="id" title="section">EncodingModuloEquiv</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + Quotient by a equivalence relation +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Module</span> <a name="EquivQuot"><span class="id" title="module">EquivQuot</span></a>.<br/> +<span class="id" title="keyword">Section</span> <a name="EquivQuot.EquivQuot"><span class="id" title="section">EquivQuot</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="EquivQuot.EquivQuot.D"><span class="id" title="variable">D</span></a> : <span class="id" title="keyword">Type</span>) (<a name="EquivQuot.EquivQuot.C"><span class="id" title="variable">C</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<a name="EquivQuot.EquivQuot.CD"><span class="id" title="variable">CD</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#C"><span class="id" title="variable">C</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a>) (<a name="EquivQuot.EquivQuot.DC"><span class="id" title="variable">DC</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#C"><span class="id" title="variable">C</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="EquivQuot.EquivQuot.eD"><span class="id" title="variable">eD</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_rel"><span class="id" title="record">equiv_rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.D"><span class="id" title="variable">D</span></a>) (<a name="EquivQuot.EquivQuot.encD"><span class="id" title="variable">encD</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encModRel"><span class="id" title="record">encModRel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.CD"><span class="id" title="variable">CD</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.DC"><span class="id" title="variable">DC</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eD"><span class="id" title="variable">eD</span></a>).<br/> +<span class="id" title="keyword">Notation</span> <a name="EquivQuot.eC"><span class="id" title="abbreviation">eC</span></a> := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encoded_equiv"><span class="id" title="definition">encoded_equiv</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.encD"><span class="id" title="variable">encD</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="EquivQuot.canon"><span class="id" title="definition">canon</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.eC"><span class="id" title="abbreviation">eC</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="EquivQuot.equivQuotient"><span class="id" title="record">equivQuotient</span></a> := <a name="EquivQuot.EquivQuotient"><span class="id" title="constructor">EquivQuotient</span></a> {<br/> + <a name="EquivQuot.erepr"><span class="id" title="projection">erepr</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.C"><span class="id" title="variable">C</span></a>;<br/> + <span class="id" title="var">_</span> : (<a class="idref" href="mathcomp.ssreflect.eqtype.html#frel"><span class="id" title="definition">frel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.canon"><span class="id" title="definition">canon</span></a>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#erepr"><span class="id" title="method">erepr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#erepr"><span class="id" title="method">erepr</span></a><br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="EquivQuot.type_of"><span class="id" title="definition">type_of</span></a> <span class="id" title="keyword">of</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phantom"><span class="id" title="inductive">phantom</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <span class="id" title="var">_</span>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.encD"><span class="id" title="variable">encD</span></a>) := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.equivQuotient"><span class="id" title="record">equivQuotient</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="EquivQuot.canon_id"><span class="id" title="lemma">canon_id</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, (<a class="idref" href="mathcomp.ssreflect.eqtype.html#invariant"><span class="id" title="definition">invariant</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.canon"><span class="id" title="definition">canon</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.canon"><span class="id" title="definition">canon</span></a>) <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="EquivQuot.pi"><span class="id" title="definition">pi</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuotient"><span class="id" title="constructor">EquivQuotient</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.canon_id"><span class="id" title="lemma">canon_id</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="EquivQuot.ereprK"><span class="id" title="lemma">ereprK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.erepr"><span class="id" title="projection">erepr</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.pi"><span class="id" title="definition">pi</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">encD_equiv_rel</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRelPack"><span class="id" title="constructor">EquivRelPack</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#enc_mod_rel_is_equiv"><span class="id" title="lemma">enc_mod_rel_is_equiv</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.encD"><span class="id" title="variable">encD</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="EquivQuot.pi_CD"><span class="id" title="lemma">pi_CD</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.C"><span class="id" title="variable">C</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.pi"><span class="id" title="definition">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.pi"><span class="id" title="definition">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.eC"><span class="id" title="abbreviation">eC</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="EquivQuot.pi_DC"><span class="id" title="lemma">pi_DC</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.D"><span class="id" title="variable">D</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.pi"><span class="id" title="definition">pi</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.DC"><span class="id" title="variable">DC</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.pi"><span class="id" title="definition">pi</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.DC"><span class="id" title="variable">DC</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>)) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.eD"><span class="id" title="variable">eD</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="EquivQuot.equivQTP"><span class="id" title="lemma">equivQTP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.CD"><span class="id" title="variable">CD</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.erepr"><span class="id" title="projection">erepr</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.pi"><span class="id" title="definition">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.DC"><span class="id" title="variable">DC</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="EquivQuot.quotClass"><span class="id" title="definition">quotClass</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotClass"><span class="id" title="constructor">QuotClass</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.equivQTP"><span class="id" title="lemma">equivQTP</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">quotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#QuotType"><span class="id" title="abbreviation">QuotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.qT"><span class="id" title="abbreviation">qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.quotClass"><span class="id" title="definition">quotClass</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="EquivQuot.eqmodP"><span class="id" title="lemma">eqmodP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.qT"><span class="id" title="abbreviation">qT</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">]</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.eD"><span class="id" title="variable">eD</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="EquivQuot.eqMixin"><span class="id" title="lemma">eqMixin</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.mixin_of"><span class="id" title="record">Equality.mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.qT"><span class="id" title="abbreviation">qT</span></a>. <br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.qT"><span class="id" title="abbreviation">qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.eqMixin"><span class="id" title="lemma">eqMixin</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="EquivQuot.choiceMixin"><span class="id" title="definition">choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.ereprK"><span class="id" title="lemma">ereprK</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.qT"><span class="id" title="abbreviation">qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.choiceMixin"><span class="id" title="definition">choiceMixin</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="EquivQuot.eqmodE"><span class="id" title="lemma">eqmodE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.qT"><span class="id" title="abbreviation">qT</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.eD"><span class="id" title="variable">eD</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqQuotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotType"><span class="id" title="abbreviation">EqQuotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot.eD"><span class="id" title="variable">eD</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.qT"><span class="id" title="abbreviation">qT</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.eqmodE"><span class="id" title="lemma">eqmodE</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot.EquivQuot"><span class="id" title="section">EquivQuot</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuot"><span class="id" title="module">EquivQuot</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">EquivQuot.quotType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">EquivQuot.eqType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">EquivQuot.choiceType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">EquivQuot.eqQuotType</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">"</span></a>{eq_quot e }" :=<br/> +(@<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#type_of"><span class="id" title="definition">EquivQuot.type_of</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phantom"><span class="id" title="constructor">Phantom</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">e</span>)) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">"</span></a>x == y %[mod_eq r ]" := (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">==</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">eq_quot</span></a> <span class="id" title="var">r</span><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="7cb336db394e2084be9172e06d707a2e"><span class="id" title="notation">"</span></a>x = y %[mod_eq r ]" := (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">=</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">eq_quot</span></a> <span class="id" title="var">r</span><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="dfbb5750f40d4eb61b889b287d9255ed"><span class="id" title="notation">"</span></a>x != y %[mod_eq r ]" := (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">!=</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">eq_quot</span></a> <span class="id" title="var">r</span><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#64dce3fc11e63c73e37431825b6bda70"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">quotient_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="3c6202054dc10892e8276e82e996200f"><span class="id" title="notation">"</span></a>x <> y %[mod_eq r ]" := (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">≠</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">eq_quot</span></a> <span class="id" title="var">r</span><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c19d82d8c4200cd8b2206f1641e1d5ca"><span class="id" title="notation">]</span></a>) : <span class="id" title="var">quotient_scope</span>.<br/> + +<br/> +</div> + +<div class="doc"> + If the type is directly a choiceType, no need to encode +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Section</span> <a name="DefaultEncodingModuloRel"><span class="id" title="section">DefaultEncodingModuloRel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="DefaultEncodingModuloRel.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<a name="DefaultEncodingModuloRel.r"><span class="id" title="variable">r</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="defaultEncModRelClass"><span class="id" title="definition">defaultEncModRelClass</span></a> :=<br/> + @<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncModRelClassPack"><span class="id" title="constructor">EncModRelClassPack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#DefaultEncodingModuloRel.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#DefaultEncodingModuloRel.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#DefaultEncodingModuloRel.r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#DefaultEncodingModuloRel.r"><span class="id" title="variable">r</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <span class="id" title="var">rxx</span> ⇒ <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#rxx"><span class="id" title="variable">rxx</span></a>) (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#erefl"><span class="id" title="abbreviation">erefl</span></a> <span class="id" title="var">_</span>).<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">defaultEncModRel</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EncModRelPack"><span class="id" title="constructor">EncModRelPack</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#defaultEncModRelClass"><span class="id" title="definition">defaultEncModRelClass</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#DefaultEncodingModuloRel"><span class="id" title="section">DefaultEncodingModuloRel</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + Recovering a potential countable type structure +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Section</span> <a name="CountEncodingModuloRel"><span class="id" title="section">CountEncodingModuloRel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="CountEncodingModuloRel.D"><span class="id" title="variable">D</span></a> : <span class="id" title="keyword">Type</span>) (<a name="CountEncodingModuloRel.C"><span class="id" title="variable">C</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) (<a name="CountEncodingModuloRel.CD"><span class="id" title="variable">CD</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#C"><span class="id" title="variable">C</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a>) (<a name="CountEncodingModuloRel.DC"><span class="id" title="variable">DC</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#C"><span class="id" title="variable">C</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="CountEncodingModuloRel.eD"><span class="id" title="variable">eD</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_rel"><span class="id" title="record">equiv_rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#CountEncodingModuloRel.D"><span class="id" title="variable">D</span></a>) (<a name="CountEncodingModuloRel.encD"><span class="id" title="variable">encD</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encModRel"><span class="id" title="record">encModRel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#CountEncodingModuloRel.CD"><span class="id" title="variable">CD</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#CountEncodingModuloRel.DC"><span class="id" title="variable">DC</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eD"><span class="id" title="variable">eD</span></a>).<br/> +<span class="id" title="keyword">Notation</span> <a name="eC"><span class="id" title="abbreviation">eC</span></a> := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#encoded_equiv"><span class="id" title="definition">encoded_equiv</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#CountEncodingModuloRel.encD"><span class="id" title="variable">encD</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="eq_quot_countMixin"><span class="id" title="lemma">eq_quot_countMixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin_of"><span class="id" title="record">Countable.mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">eq_quot</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#CountEncodingModuloRel.encD"><span class="id" title="variable">encD</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">}</span></a>.<br/> + <span class="id" title="keyword">Canonical</span> <span class="id" title="var">eq_quot_countType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">eq_quot</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#CountEncodingModuloRel.encD"><span class="id" title="variable">encD</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eq_quot_countMixin"><span class="id" title="lemma">eq_quot_countMixin</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#CountEncodingModuloRel"><span class="id" title="section">CountEncodingModuloRel</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="EquivQuotTheory"><span class="id" title="section">EquivQuotTheory</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="EquivQuotTheory.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<a name="EquivQuotTheory.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#equiv_rel"><span class="id" title="record">equiv_rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) (<a name="EquivQuotTheory.Q"><span class="id" title="variable">Q</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType"><span class="id" title="record">eqQuotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eqmodE"><span class="id" title="lemma">eqmodE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">mod_eq</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuotTheory.e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuotTheory.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eqmodP"><span class="id" title="lemma">eqmodP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7cb336db394e2084be9172e06d707a2e"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7cb336db394e2084be9172e06d707a2e"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7cb336db394e2084be9172e06d707a2e"><span class="id" title="notation">mod_eq</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuotTheory.e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7cb336db394e2084be9172e06d707a2e"><span class="id" title="notation">]</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuotTheory.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivQuotTheory"><span class="id" title="section">EquivQuotTheory</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="EqQuotTheory"><span class="id" title="section">EqQuotTheory</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="EqQuotTheory.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>) (<a name="EqQuotTheory.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#T"><span class="id" title="variable">T</span></a>) (<a name="EqQuotTheory.Q"><span class="id" title="variable">Q</span></a> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#eqQuotType"><span class="id" title="record">eqQuotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e"><span class="id" title="variable">e</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eqquotE"><span class="id" title="lemma">eqquotE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTheory.Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTheory.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eqquotP"><span class="id" title="lemma">eqquotP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTheory.Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#1d0bea61314a6549a966f59a90fca2c5"><span class="id" title="notation">]</span></a>) (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTheory.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EqQuotTheory"><span class="id" title="section">EqQuotTheory</span></a>.<br/> + +<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file |