Deploying to gh-pages from @ f717d46 🚀

Author: felixwellen

Cubical.Algebra.CommMonoid.Properties.html

@@ -58,4 +58,20 @@
  <a id="CommMonoidTheory.commAssocSwap"></a><a id="1873" href="Cubical.Algebra.CommMonoid.Properties.html#1873" class="Function">commAssocSwap</a> <a id="1887" class="Symbol">:</a> <a id="1889" class="Symbol">(</a><a id="1890" href="Cubical.Algebra.CommMonoid.Properties.html#1890" class="Bound">x</a> <a id="1892" href="Cubical.Algebra.CommMonoid.Properties.html#1892" class="Bound">y</a> <a id="1894" href="Cubical.Algebra.CommMonoid.Properties.html#1894" class="Bound">z</a> <a id="1896" href="Cubical.Algebra.CommMonoid.Properties.html#1896" class="Bound">w</a> <a id="1898" class="Symbol">:</a> <a id="1900" href="Cubical.Algebra.CommMonoid.Properties.html#1452" class="Function">M</a><a id="1901" class="Symbol">)</a> <a id="1903" class="Symbol">→</a> <a id="1905" class="Symbol">(</a><a id="1906" href="Cubical.Algebra.CommMonoid.Properties.html#1890" class="Bound">x</a> <a id="1908" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="1910" href="Cubical.Algebra.CommMonoid.Properties.html#1892" class="Bound">y</a><a id="1911" class="Symbol">)</a> <a id="1913" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="1915" class="Symbol">(</a><a id="1916" href="Cubical.Algebra.CommMonoid.Properties.html#1894" class="Bound">z</a> <a id="1918" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="1920" href="Cubical.Algebra.CommMonoid.Properties.html#1896" class="Bound">w</a><a id="1921" class="Symbol">)</a> <a id="1923" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="1925" class="Symbol">(</a><a id="1926" href="Cubical.Algebra.CommMonoid.Properties.html#1890" class="Bound">x</a> <a id="1928" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="1930" href="Cubical.Algebra.CommMonoid.Properties.html#1894" class="Bound">z</a><a id="1931" class="Symbol">)</a> <a id="1933" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="1935" class="Symbol">(</a><a id="1936" href="Cubical.Algebra.CommMonoid.Properties.html#1892" class="Bound">y</a> <a id="1938" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="1940" href="Cubical.Algebra.CommMonoid.Properties.html#1896" class="Bound">w</a><a id="1941" class="Symbol">)</a>
  <a id="1944" href="Cubical.Algebra.CommMonoid.Properties.html#1873" class="Function">commAssocSwap</a> <a id="1958" href="Cubical.Algebra.CommMonoid.Properties.html#1958" class="Bound">x</a> <a id="1960" href="Cubical.Algebra.CommMonoid.Properties.html#1960" class="Bound">y</a> <a id="1962" href="Cubical.Algebra.CommMonoid.Properties.html#1962" class="Bound">z</a> <a id="1964" href="Cubical.Algebra.CommMonoid.Properties.html#1964" class="Bound">w</a> <a id="1966" class="Symbol">=</a> <a id="1968" href="Cubical.Algebra.Semigroup.Base.html#1031" class="Function">·Assoc</a> <a id="1975" class="Symbol">(</a><a id="1976" href="Cubical.Algebra.CommMonoid.Properties.html#1958" class="Bound">x</a> <a id="1978" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="1980" href="Cubical.Algebra.CommMonoid.Properties.html#1960" class="Bound">y</a><a id="1981" class="Symbol">)</a> <a id="1983" href="Cubical.Algebra.CommMonoid.Properties.html#1962" class="Bound">z</a> <a id="1985" href="Cubical.Algebra.CommMonoid.Properties.html#1964" class="Bound">w</a> <a id="1987" href="Cubical.Foundations.Prelude.html#4007" class="Function Operator">∙∙</a> <a id="1990" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="1995" class="Symbol">(</a><a id="1996" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">_·</a> <a id="1999" href="Cubical.Algebra.CommMonoid.Properties.html#1964" class="Bound">w</a><a id="2000" class="Symbol">)</a> <a id="2002" class="Symbol">(</a><a id="2003" href="Cubical.Algebra.CommMonoid.Properties.html#1602" class="Function">commAssocr</a> <a id="2014" href="Cubical.Algebra.CommMonoid.Properties.html#1958" class="Bound">x</a> <a id="2016" href="Cubical.Algebra.CommMonoid.Properties.html#1960" class="Bound">y</a> <a id="2018" href="Cubical.Algebra.CommMonoid.Properties.html#1962" class="Bound">z</a><a id="2019" class="Symbol">)</a>
                                                <a id="2068" href="Cubical.Foundations.Prelude.html#4007" class="Function Operator">∙∙</a> <a id="2071" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="2075" class="Symbol">(</a><a id="2076" href="Cubical.Algebra.Semigroup.Base.html#1031" class="Function">·Assoc</a> <a id="2083" class="Symbol">(</a><a id="2084" href="Cubical.Algebra.CommMonoid.Properties.html#1958" class="Bound">x</a> <a id="2086" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="2088" href="Cubical.Algebra.CommMonoid.Properties.html#1962" class="Bound">z</a><a id="2089" class="Symbol">)</a> <a id="2091" href="Cubical.Algebra.CommMonoid.Properties.html#1960" class="Bound">y</a> <a id="2093" href="Cubical.Algebra.CommMonoid.Properties.html#1964" class="Bound">w</a><a id="2094" class="Symbol">)</a>
+
+ <a id="CommMonoidTheory.hasInverse"></a><a id="2098" href="Cubical.Algebra.CommMonoid.Properties.html#2098" class="Function">hasInverse</a> <a id="2109" class="Symbol">:</a> <a id="2111" class="Symbol">(</a><a id="2112" href="Cubical.Algebra.CommMonoid.Properties.html#2112" class="Bound">x</a> <a id="2114" class="Symbol">:</a> <a id="2116" href="Cubical.Algebra.CommMonoid.Properties.html#1452" class="Function">M</a><a id="2117" class="Symbol">)</a> <a id="2119" class="Symbol">→</a> <a id="2121" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="2126" href="Cubical.Algebra.CommMonoid.Properties.html#1405" class="Bound">ℓ</a>
+ <a id="2129" href="Cubical.Algebra.CommMonoid.Properties.html#2098" class="Function">hasInverse</a> <a id="2140" href="Cubical.Algebra.CommMonoid.Properties.html#2140" class="Bound">x</a> <a id="2142" class="Symbol">=</a> <a id="2144" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="2147" href="Cubical.Algebra.CommMonoid.Properties.html#2147" class="Bound">-x</a> <a id="2150" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="2152" href="Cubical.Algebra.CommMonoid.Properties.html#1452" class="Function">M</a> <a id="2154" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="2156" href="Cubical.Algebra.CommMonoid.Properties.html#2147" class="Bound">-x</a> <a id="2159" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="2161" href="Cubical.Algebra.CommMonoid.Properties.html#2140" class="Bound">x</a> <a id="2163" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="2165" href="Cubical.Algebra.CommMonoid.Base.html#991" class="Function">ε</a>
+
+ <a id="CommMonoidTheory.isPropHasInverse"></a><a id="2169" href="Cubical.Algebra.CommMonoid.Properties.html#2169" class="Function">isPropHasInverse</a> <a id="2186" class="Symbol">:</a> <a id="2188" class="Symbol">∀</a> <a id="2190" href="Cubical.Algebra.CommMonoid.Properties.html#2190" class="Bound">x</a> <a id="2192" class="Symbol">→</a> <a id="2194" href="Cubical.Foundations.Prelude.html#15547" class="Function">isProp</a> <a id="2201" class="Symbol">(</a><a id="2202" href="Cubical.Algebra.CommMonoid.Properties.html#2098" class="Function">hasInverse</a> <a id="2213" href="Cubical.Algebra.CommMonoid.Properties.html#2190" class="Bound">x</a><a id="2214" class="Symbol">)</a>
+ <a id="2217" href="Cubical.Algebra.CommMonoid.Properties.html#2169" class="Function">isPropHasInverse</a> <a id="2234" href="Cubical.Algebra.CommMonoid.Properties.html#2234" class="Bound">x</a> <a id="2236" href="Cubical.Algebra.CommMonoid.Properties.html#2236" class="Bound">yinv</a> <a id="2241" href="Cubical.Algebra.CommMonoid.Properties.html#2241" class="Bound">zinv</a>
+   <a id="2249" class="Symbol">=</a> <a id="2251" href="Cubical.Data.Sigma.Properties.html#13825" class="Function">Σ≡Prop</a> <a id="2258" class="Symbol">(λ</a> <a id="2261" href="Cubical.Algebra.CommMonoid.Properties.html#2261" class="Bound">a</a> <a id="2263" class="Symbol">→</a> <a id="2265" href="Cubical.Algebra.Semigroup.Base.html#1010" class="Function">is-set</a> <a id="2272" class="Symbol">(</a><a id="2273" href="Cubical.Algebra.CommMonoid.Properties.html#2261" class="Bound">a</a> <a id="2275" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Function Operator">·</a> <a id="2277" href="Cubical.Algebra.CommMonoid.Properties.html#2234" class="Bound">x</a><a id="2278" class="Symbol">)</a> <a id="2280" href="Cubical.Algebra.CommMonoid.Base.html#991" class="Function">ε</a><a id="2281" class="Symbol">)</a>
+    <a id="2287" class="Symbol">(</a><a id="2288" href="Cubical.Data.Sigma.Properties.html#2083" class="Function">PathPΣ</a> <a id="2295" class="Symbol">(</a><a id="2296" href="Cubical.Algebra.Monoid.Base.html#4323" class="Function">MonoidTheory.isPropHasInverse</a> <a id="2326" class="Symbol">(</a><a id="2327" href="Cubical.Algebra.CommMonoid.Base.html#2506" class="Function">CommMonoid→Monoid</a> <a id="2345" href="Cubical.Algebra.CommMonoid.Properties.html#1389" class="Bound">M&#39;</a><a id="2347" class="Symbol">)</a> <a id="2349" href="Cubical.Algebra.CommMonoid.Properties.html#2234" class="Bound">x</a>
+                                           <a id="2394" class="Symbol">(</a><a id="2395" href="Cubical.Algebra.CommMonoid.Properties.html#2561" class="Function">hasInverseToMonoid</a> <a id="2414" href="Cubical.Algebra.CommMonoid.Properties.html#2234" class="Bound">x</a> <a id="2416" href="Cubical.Algebra.CommMonoid.Properties.html#2236" class="Bound">yinv</a><a id="2420" class="Symbol">)</a>
+                                           <a id="2465" class="Symbol">(</a><a id="2466" href="Cubical.Algebra.CommMonoid.Properties.html#2561" class="Function">hasInverseToMonoid</a> <a id="2485" href="Cubical.Algebra.CommMonoid.Properties.html#2234" class="Bound">x</a> <a id="2487" href="Cubical.Algebra.CommMonoid.Properties.html#2241" class="Bound">zinv</a><a id="2491" class="Symbol">))</a>
+                                               <a id="2541" class="Symbol">.</a><a id="2542" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a><a id="2545" class="Symbol">)</a>
+   <a id="2550" class="Keyword">where</a>
+     <a id="2561" href="Cubical.Algebra.CommMonoid.Properties.html#2561" class="Function">hasInverseToMonoid</a> <a id="2580" class="Symbol">:</a> <a id="2582" class="Symbol">∀</a> <a id="2584" href="Cubical.Algebra.CommMonoid.Properties.html#2584" class="Bound">x</a>
+                        <a id="2610" class="Symbol">→</a> <a id="2612" href="Cubical.Algebra.CommMonoid.Properties.html#2098" class="Function">hasInverse</a> <a id="2623" href="Cubical.Algebra.CommMonoid.Properties.html#2584" class="Bound">x</a>
+                        <a id="2649" class="Symbol">→</a> <a id="2651" href="Cubical.Algebra.Monoid.Base.html#4225" class="Function">MonoidTheory.hasInverse</a> <a id="2675" class="Symbol">(</a><a id="2676" href="Cubical.Algebra.CommMonoid.Base.html#2506" class="Function">CommMonoid→Monoid</a> <a id="2694" href="Cubical.Algebra.CommMonoid.Properties.html#1389" class="Bound">M&#39;</a><a id="2696" class="Symbol">)</a> <a id="2698" href="Cubical.Algebra.CommMonoid.Properties.html#2584" class="Bound">x</a>
+     <a id="2705" href="Cubical.Algebra.CommMonoid.Properties.html#2561" class="Function">hasInverseToMonoid</a> <a id="2724" href="Cubical.Algebra.CommMonoid.Properties.html#2724" class="Bound">x</a> <a id="2726" class="Symbol">(</a><a id="2727" href="Cubical.Algebra.CommMonoid.Properties.html#2727" class="Bound">y</a> <a id="2729" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2731" href="Cubical.Algebra.CommMonoid.Properties.html#2731" class="Bound">yinv</a><a id="2735" class="Symbol">)</a> <a id="2737" class="Symbol">=</a> <a id="2739" href="Cubical.Algebra.CommMonoid.Properties.html#2727" class="Bound">y</a> <a id="2741" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2743" href="Cubical.Algebra.CommMonoid.Properties.html#2731" class="Bound">yinv</a> <a id="2748" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2750" href="Cubical.Algebra.CommMonoid.Base.html#741" class="Function">·Comm</a> <a id="2756" href="Cubical.Algebra.CommMonoid.Properties.html#2724" class="Bound">x</a> <a id="2758" href="Cubical.Algebra.CommMonoid.Properties.html#2727" class="Bound">y</a> <a id="2760" href="Cubical.Foundations.Prelude.html#5207" class="Function Operator">∙</a> <a id="2762" href="Cubical.Algebra.CommMonoid.Properties.html#2731" class="Bound">yinv</a>
 </pre></body></html>

Cubical.Algebra.CommRing.Localisation.Base.html

@@ -89,10 +89,10 @@
          <a id="2929" href="Cubical.Algebra.CommRing.Localisation.Base.html#2503" class="Bound">u</a> <a id="2931" href="Cubical.Algebra.CommRing.Base.html#1105" class="Function Operator">·</a> <a id="2933" href="Cubical.Algebra.CommRing.Localisation.Base.html#2452" class="Bound">s</a> <a id="2935" href="Cubical.Algebra.CommRing.Base.html#1105" class="Function Operator">·</a> <a id="2937" class="Symbol">(</a><a id="2938" href="Cubical.Algebra.CommRing.Localisation.Base.html#2520" class="Bound">v</a> <a id="2940" href="Cubical.Algebra.CommRing.Base.html#1105" class="Function Operator">·</a> <a id="2942" href="Cubical.Algebra.CommRing.Localisation.Base.html#2481" class="Bound">r&#39;&#39;</a> <a id="2946" href="Cubical.Algebra.CommRing.Base.html#1105" class="Function Operator">·</a> <a id="2948" href="Cubical.Algebra.CommRing.Localisation.Base.html#2468" class="Bound">s&#39;</a><a id="2950" class="Symbol">)</a> <a id="2952" href="Cubical.Foundations.Prelude.html#9052" class="Function">≡⟨</a> <a id="2955" href="Cubical.Tactics.CommRingSolver.Reflection.html#7086" class="Macro">solve!</a> <a id="2962" href="Cubical.Algebra.CommRing.Localisation.Base.html#1731" class="Bound">R&#39;</a> <a id="2965" href="Cubical.Foundations.Prelude.html#9052" class="Function">⟩</a>
          <a id="2976" href="Cubical.Algebra.CommRing.Localisation.Base.html#2503" class="Bound">u</a> <a id="2978" href="Cubical.Algebra.CommRing.Base.html#1105" class="Function Operator">·</a> <a id="2980" href="Cubical.Algebra.CommRing.Localisation.Base.html#2520" class="Bound">v</a> <a id="2982" href="Cubical.Algebra.CommRing.Base.html#1105" class="Function Operator">·</a> <a id="2984" href="Cubical.Algebra.CommRing.Localisation.Base.html#2468" class="Bound">s&#39;</a> <a id="2987" href="Cubical.Algebra.CommRing.Base.html#1105" class="Function Operator">·</a> <a id="2989" href="Cubical.Algebra.CommRing.Localisation.Base.html#2481" class="Bound">r&#39;&#39;</a> <a id="2993" href="Cubical.Algebra.CommRing.Base.html#1105" class="Function Operator">·</a> <a id="2995" href="Cubical.Algebra.CommRing.Localisation.Base.html#2452" class="Bound">s</a>   <a id="2999" href="Cubical.Foundations.Prelude.html#9599" class="Function Operator">∎</a>
 
- <a id="Loc.locIsEquivRel"></a><a id="3003" href="Cubical.Algebra.CommRing.Localisation.Base.html#3003" class="Function">locIsEquivRel</a> <a id="3017" class="Symbol">:</a> <a id="3019" href="Cubical.Relation.Binary.Base.html#3830" class="Record">isEquivRel</a> <a id="3030" href="Cubical.Algebra.CommRing.Localisation.Base.html#2062" class="Function Operator">_≈_</a>
- <a id="3035" href="Cubical.Relation.Binary.Base.html#3908" class="Field">isEquivRel.reflexive</a> <a id="3056" href="Cubical.Algebra.CommRing.Localisation.Base.html#3003" class="Function">locIsEquivRel</a> <a id="3070" class="Symbol">=</a> <a id="3072" href="Cubical.Algebra.CommRing.Localisation.Base.html#2251" class="Function">locRefl</a>
- <a id="3081" href="Cubical.Relation.Binary.Base.html#3933" class="Field">isEquivRel.symmetric</a> <a id="3102" href="Cubical.Algebra.CommRing.Localisation.Base.html#3003" class="Function">locIsEquivRel</a> <a id="3116" class="Symbol">=</a> <a id="3118" href="Cubical.Algebra.CommRing.Localisation.Base.html#2332" class="Function">locSym</a>
- <a id="3126" href="Cubical.Relation.Binary.Base.html#3957" class="Field">isEquivRel.transitive</a> <a id="3148" href="Cubical.Algebra.CommRing.Localisation.Base.html#3003" class="Function">locIsEquivRel</a> <a id="3162" class="Symbol">=</a> <a id="3164" href="Cubical.Algebra.CommRing.Localisation.Base.html#2414" class="Function">locTrans</a>
+ <a id="Loc.locIsEquivRel"></a><a id="3003" href="Cubical.Algebra.CommRing.Localisation.Base.html#3003" class="Function">locIsEquivRel</a> <a id="3017" class="Symbol">:</a> <a id="3019" href="Cubical.Relation.Binary.Base.html#3803" class="Record">isEquivRel</a> <a id="3030" href="Cubical.Algebra.CommRing.Localisation.Base.html#2062" class="Function Operator">_≈_</a>
+ <a id="3035" href="Cubical.Relation.Binary.Base.html#3881" class="Field">isEquivRel.reflexive</a> <a id="3056" href="Cubical.Algebra.CommRing.Localisation.Base.html#3003" class="Function">locIsEquivRel</a> <a id="3070" class="Symbol">=</a> <a id="3072" href="Cubical.Algebra.CommRing.Localisation.Base.html#2251" class="Function">locRefl</a>
+ <a id="3081" href="Cubical.Relation.Binary.Base.html#3906" class="Field">isEquivRel.symmetric</a> <a id="3102" href="Cubical.Algebra.CommRing.Localisation.Base.html#3003" class="Function">locIsEquivRel</a> <a id="3116" class="Symbol">=</a> <a id="3118" href="Cubical.Algebra.CommRing.Localisation.Base.html#2332" class="Function">locSym</a>
+ <a id="3126" href="Cubical.Relation.Binary.Base.html#3930" class="Field">isEquivRel.transitive</a> <a id="3148" href="Cubical.Algebra.CommRing.Localisation.Base.html#3003" class="Function">locIsEquivRel</a> <a id="3162" class="Symbol">=</a> <a id="3164" href="Cubical.Algebra.CommRing.Localisation.Base.html#2414" class="Function">locTrans</a>
 
  <a id="Loc._+ₗ_"></a><a id="3175" href="Cubical.Algebra.CommRing.Localisation.Base.html#3175" class="Function Operator">_+ₗ_</a> <a id="3180" class="Symbol">:</a> <a id="3182" href="Cubical.Algebra.CommRing.Localisation.Base.html#2173" class="Function">S⁻¹R</a> <a id="3187" class="Symbol">→</a> <a id="3189" href="Cubical.Algebra.CommRing.Localisation.Base.html#2173" class="Function">S⁻¹R</a> <a id="3194" class="Symbol">→</a> <a id="3196" href="Cubical.Algebra.CommRing.Localisation.Base.html#2173" class="Function">S⁻¹R</a>
  <a id="3202" href="Cubical.Algebra.CommRing.Localisation.Base.html#3175" class="Function Operator">_+ₗ_</a> <a id="3207" class="Symbol">=</a> <a id="3209" href="Cubical.HITs.SetQuotients.Properties.html#8391" class="Function">setQuotSymmBinOp</a> <a id="3226" href="Cubical.Algebra.CommRing.Localisation.Base.html#2251" class="Function">locRefl</a> <a id="3234" href="Cubical.Algebra.CommRing.Localisation.Base.html#2414" class="Function">locTrans</a> <a id="3243" href="Cubical.Algebra.CommRing.Localisation.Base.html#3339" class="Function Operator">_+ₚ_</a>