Deploying to gh-pages from @ 86485a5 🚀

Author: felixwellen

Cubical.Algebra.Group.Instances.IntMod.html

@@ -57,11 +57,11 @@
 <a id="reduce-[]"></a><a id="2456" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2456" class="Function">reduce-[]</a> <a id="2466" class="Symbol">:</a> <a id="2468" class="Symbol">∀</a> <a id="2470" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2470" class="Bound">x</a> <a id="2472" class="Symbol">→</a> <a id="2474" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#696" class="Function">reduce</a> <a id="2481" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">Quo.[</a> <a id="2487" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2470" class="Bound">x</a> <a id="2489" class="Symbol">.</a><a id="2490" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="2494" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">]</a> <a id="2496" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="2498" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2470" class="Bound">x</a>
      <a id="2505" class="Comment">-- equivalent to: Sigma.[ s .fst ] ≡ x</a>
 <a id="2544" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2456" class="Function">reduce-[]</a> <a id="2554" class="Symbol">((</a><a id="2556" href="Cubical.Data.Int.MoreInts.QuoInt.Base.html#771" class="InductiveConstructor">signed</a> <a id="2563" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2563" class="Bound">s</a> <a id="2565" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2565" class="Bound">a</a> <a id="2567" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2569" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2569" class="Bound">b</a><a id="2570" class="Symbol">)</a> <a id="2572" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2574" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2574" class="Bound">cp</a><a id="2576" class="Symbol">)</a> <a id="2578" class="Symbol">=</a>
-  <a id="2582" href="Cubical.Data.Sigma.Properties.html#13802" class="Function">Σ≡Prop</a> <a id="2589" class="Symbol">(λ</a> <a id="2592" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2592" class="Bound">_</a> <a id="2594" class="Symbol">→</a> <a id="2596" href="Cubical.Data.Nat.GCD.html#1047" class="Function">isPropIsGCD</a><a id="2607" class="Symbol">)</a> <a id="2609" class="Symbol">(</a><a id="2610" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2213" class="Function">toCoprime-eq₂</a> <a id="2624" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2563" class="Bound">s</a> <a id="2626" class="Symbol">(</a><a id="2627" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2565" class="Bound">a</a> <a id="2629" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2631" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2569" class="Bound">b</a><a id="2632" class="Symbol">)</a> <a id="2634" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2574" class="Bound">cp</a><a id="2636" class="Symbol">)</a>
+  <a id="2582" href="Cubical.Data.Sigma.Properties.html#13802" class="Function">Σ≡Prop</a> <a id="2589" class="Symbol">(λ</a> <a id="2592" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2592" class="Bound">_</a> <a id="2594" class="Symbol">→</a> <a id="2596" href="Cubical.Data.Nat.GCD.html#1214" class="Function">isPropIsGCD</a><a id="2607" class="Symbol">)</a> <a id="2609" class="Symbol">(</a><a id="2610" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2213" class="Function">toCoprime-eq₂</a> <a id="2624" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2563" class="Bound">s</a> <a id="2626" class="Symbol">(</a><a id="2627" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2565" class="Bound">a</a> <a id="2629" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2631" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2569" class="Bound">b</a><a id="2632" class="Symbol">)</a> <a id="2634" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2574" class="Bound">cp</a><a id="2636" class="Symbol">)</a>
 <a id="2638" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2456" class="Function">reduce-[]</a> <a id="2648" class="Symbol">((</a><a id="2650" href="Cubical.Data.Int.MoreInts.QuoInt.Base.html#805" class="InductiveConstructor">posneg</a> <a id="2657" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2657" class="Bound">i</a> <a id="2659" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2661" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2661" class="Bound">b</a><a id="2662" class="Symbol">)</a> <a id="2664" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2666" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2666" class="Bound">cp</a><a id="2668" class="Symbol">)</a> <a id="2670" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2670" class="Bound">j</a> <a id="2672" class="Symbol">=</a>
   <a id="2676" href="Cubical.Foundations.Prelude.html#18383" class="Function">isSet→isSet&#39;</a> <a id="2689" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Base.html#490" class="Function">Sigma.isSetℚ</a>
-    <a id="2706" class="Symbol">(</a><a id="2707" href="Cubical.Data.Sigma.Properties.html#13802" class="Function">Σ≡Prop</a> <a id="2714" class="Symbol">(λ</a> <a id="2717" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2717" class="Bound">_</a> <a id="2719" class="Symbol">→</a> <a id="2721" href="Cubical.Data.Nat.GCD.html#1047" class="Function">isPropIsGCD</a><a id="2732" class="Symbol">)</a> <a id="2734" class="Symbol">(</a><a id="2735" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2213" class="Function">toCoprime-eq₂</a> <a id="2749" href="Cubical.Data.Int.MoreInts.QuoInt.Base.html#660" class="InductiveConstructor">spos</a> <a id="2754" class="Symbol">(</a><a id="2755" class="Number">0</a> <a id="2757" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2759" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2661" class="Bound">b</a><a id="2760" class="Symbol">)</a> <a id="2762" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2666" class="Bound">cp</a><a id="2764" class="Symbol">))</a>
-    <a id="2771" class="Symbol">(</a><a id="2772" href="Cubical.Data.Sigma.Properties.html#13802" class="Function">Σ≡Prop</a> <a id="2779" class="Symbol">(λ</a> <a id="2782" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2782" class="Bound">_</a> <a id="2784" class="Symbol">→</a> <a id="2786" href="Cubical.Data.Nat.GCD.html#1047" class="Function">isPropIsGCD</a><a id="2797" class="Symbol">)</a> <a id="2799" class="Symbol">(</a><a id="2800" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2213" class="Function">toCoprime-eq₂</a> <a id="2814" href="Cubical.Data.Int.MoreInts.QuoInt.Base.html#686" class="InductiveConstructor">sneg</a> <a id="2819" class="Symbol">(</a><a id="2820" class="Number">0</a> <a id="2822" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2824" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2661" class="Bound">b</a><a id="2825" class="Symbol">)</a> <a id="2827" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2666" class="Bound">cp</a><a id="2829" class="Symbol">))</a>
+    <a id="2706" class="Symbol">(</a><a id="2707" href="Cubical.Data.Sigma.Properties.html#13802" class="Function">Σ≡Prop</a> <a id="2714" class="Symbol">(λ</a> <a id="2717" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2717" class="Bound">_</a> <a id="2719" class="Symbol">→</a> <a id="2721" href="Cubical.Data.Nat.GCD.html#1214" class="Function">isPropIsGCD</a><a id="2732" class="Symbol">)</a> <a id="2734" class="Symbol">(</a><a id="2735" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2213" class="Function">toCoprime-eq₂</a> <a id="2749" href="Cubical.Data.Int.MoreInts.QuoInt.Base.html#660" class="InductiveConstructor">spos</a> <a id="2754" class="Symbol">(</a><a id="2755" class="Number">0</a> <a id="2757" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2759" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2661" class="Bound">b</a><a id="2760" class="Symbol">)</a> <a id="2762" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2666" class="Bound">cp</a><a id="2764" class="Symbol">))</a>
+    <a id="2771" class="Symbol">(</a><a id="2772" href="Cubical.Data.Sigma.Properties.html#13802" class="Function">Σ≡Prop</a> <a id="2779" class="Symbol">(λ</a> <a id="2782" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2782" class="Bound">_</a> <a id="2784" class="Symbol">→</a> <a id="2786" href="Cubical.Data.Nat.GCD.html#1214" class="Function">isPropIsGCD</a><a id="2797" class="Symbol">)</a> <a id="2799" class="Symbol">(</a><a id="2800" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2213" class="Function">toCoprime-eq₂</a> <a id="2814" href="Cubical.Data.Int.MoreInts.QuoInt.Base.html#686" class="InductiveConstructor">sneg</a> <a id="2819" class="Symbol">(</a><a id="2820" class="Number">0</a> <a id="2822" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2824" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2661" class="Bound">b</a><a id="2825" class="Symbol">)</a> <a id="2827" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2666" class="Bound">cp</a><a id="2829" class="Symbol">))</a>
     <a id="2836" class="Symbol">(λ</a> <a id="2839" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2839" class="Bound">i</a> <a id="2841" class="Symbol">→</a> <a id="2843" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Base.html#681" class="Function Operator">Sigma.[</a> <a id="2851" href="Cubical.Data.Int.MoreInts.QuoInt.Base.html#805" class="InductiveConstructor">posneg</a> <a id="2858" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2839" class="Bound">i</a> <a id="2860" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2862" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2661" class="Bound">b</a> <a id="2864" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Base.html#681" class="Function Operator">]</a><a id="2865" class="Symbol">)</a> <a id="2867" class="Symbol">(λ</a> <a id="2870" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2870" class="Bound">i</a> <a id="2872" class="Symbol">→</a> <a id="2874" class="Symbol">(</a><a id="2875" href="Cubical.Data.Int.MoreInts.QuoInt.Base.html#805" class="InductiveConstructor">posneg</a> <a id="2882" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2870" class="Bound">i</a> <a id="2884" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2886" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2661" class="Bound">b</a><a id="2887" class="Symbol">)</a> <a id="2889" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2891" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2666" class="Bound">cp</a><a id="2893" class="Symbol">)</a> <a id="2895" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2657" class="Bound">i</a> <a id="2897" href="Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties.html#2670" class="Bound">j</a>