diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.generic_quotient.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.generic_quotient.html | 931 |
1 files changed, 0 insertions, 931 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html b/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html deleted file mode 100644 index f7138b1..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html +++ /dev/null @@ -1,931 +0,0 @@ -<!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. *)</span><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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/> -}.<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/V8.9.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/V8.9.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#249ace14cf68204fe02dd745e53cd64f"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#249ace14cf68204fe02dd745e53cd64f"><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/V8.9.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>.<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/> - -<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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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="3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.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="c3fdc30b5d212c820acf98356210d6f7"><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/V8.9.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="e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">"</span></a>x == y %[mod Q ]" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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="f562cbd652d1fe79fbd8d329b05b5257"><span class="id" title="notation">"</span></a>x = y %[mod Q ]" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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="9a82670521214c5e7453279f44112385"><span class="id" title="notation">"</span></a>x != y %[mod Q ]" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_Q</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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="fa232142435a5045b9ecd83984a98dc6"><span class="id" title="notation">"</span></a>x <> y %[mod Q ]" := (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#a0a5068f83a704fcfbda8cd473a6cfea"><span class="id" title="notation">≠</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.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/V8.9.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/V8.9.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#QuotTypePack"><span class="id" title="constructor">QuotTypePack</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="2b6ecaeff71b4103d20b05dbc196dba6"><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/V8.9.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/V8.9.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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_qT</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variant</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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#f562cbd652d1fe79fbd8d329b05b5257"><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#f562cbd652d1fe79fbd8d329b05b5257"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f562cbd652d1fe79fbd8d329b05b5257"><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#f562cbd652d1fe79fbd8d329b05b5257"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#5ed33d530eb2df93ae871226afbf3e57"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#5ed33d530eb2df93ae871226afbf3e57"><span class="id" title="notation">mpi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/> - -<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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#96bead841b87c72f1ae1be942b541e72"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#96bead841b87c72f1ae1be942b541e72"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#96bead841b87c72f1ae1be942b541e72"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#96bead841b87c72f1ae1be942b541e72"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#96bead841b87c72f1ae1be942b541e72"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#96bead841b87c72f1ae1be942b541e72"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">f</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">g</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">b</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">h</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">a</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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="b6c5c1f696ce64afe88ee35296e36c45"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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="7196b05d3ce94c1a0a37c47e249f5658"><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#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><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#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#7196b05d3ce94c1a0a37c47e249f5658"><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#7196b05d3ce94c1a0a37c47e249f5658"><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/V8.9.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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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/V8.9.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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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/V8.9.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/V8.9.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/V8.9.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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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/V8.9.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/V8.9.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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">(</span></a>@<a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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#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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/> - <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="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/V8.9.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/V8.9.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>).<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/V8.9.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>.<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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><span class="id" title="notation">mono</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_eqT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#fef9b78074f61857498e071064cb1961"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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="dc3d569865bd181e003ea2b17400befd"><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/V8.9.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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><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#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><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#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><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#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><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#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><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#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><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#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><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#9bbd910cbebcec91f8279b0711b4702d"><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#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><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#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><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="6ff9ee7bbd491e678d3e04bf949d2432"><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="4d3d4b86fbd3eb78da323770ca81f4c9"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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="971f678f3ae9445a25bea21a2820fb19"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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="7ef82da4fe197c18f5d75a707665b417"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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="2272c26679de0253de49a6f796cf16a1"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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">Variant</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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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> : <span class="id" title="var">core</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="b1ace5b69208b475ff605393d856b877"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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">Variant</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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.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="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#phantom"><span class="id" title="inductive">phantom</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><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/V8.9.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#f562cbd652d1fe79fbd8d329b05b5257"><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#f562cbd652d1fe79fbd8d329b05b5257"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f562cbd652d1fe79fbd8d329b05b5257"><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#f562cbd652d1fe79fbd8d329b05b5257"><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#e3392789fbfaf247c0fb823980d6e8ff"><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#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><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#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="0dc587318a1236d89082bca629a5db9b"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phantom"><span class="id" title="constructor">Phantom</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.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="3799fc59ee103320fa3882288df6a9c4"><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#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">==</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><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#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><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="4c1a397041f96fbe79230a11b61df725"><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#f562cbd652d1fe79fbd8d329b05b5257"><span class="id" title="notation">=</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f562cbd652d1fe79fbd8d329b05b5257"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f562cbd652d1fe79fbd8d329b05b5257"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><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#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f562cbd652d1fe79fbd8d329b05b5257"><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="0de2e52b5206502ead6aac26a224f122"><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#9a82670521214c5e7453279f44112385"><span class="id" title="notation">!=</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#9a82670521214c5e7453279f44112385"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#9a82670521214c5e7453279f44112385"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><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#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#9a82670521214c5e7453279f44112385"><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="bc2246d85f6f8bcbd04740c9653152f5"><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#fa232142435a5045b9ecd83984a98dc6"><span class="id" title="notation">≠</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#fa232142435a5045b9ecd83984a98dc6"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#fa232142435a5045b9ecd83984a98dc6"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><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#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#fa232142435a5045b9ecd83984a98dc6"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><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#0dc587318a1236d89082bca629a5db9b"><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#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><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#0dc587318a1236d89082bca629a5db9b"><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#3799fc59ee103320fa3882288df6a9c4"><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#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><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#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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#4c1a397041f96fbe79230a11b61df725"><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#4c1a397041f96fbe79230a11b61df725"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#4c1a397041f96fbe79230a11b61df725"><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#4c1a397041f96fbe79230a11b61df725"><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/V8.9.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#e3392789fbfaf247c0fb823980d6e8ff"><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#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><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#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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#f562cbd652d1fe79fbd8d329b05b5257"><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#f562cbd652d1fe79fbd8d329b05b5257"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f562cbd652d1fe79fbd8d329b05b5257"><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#f562cbd652d1fe79fbd8d329b05b5257"><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 |