Deploying to gh-pages from @ cd94b8c 🚀

Author: mortberg

Cubical.Categories.Functor.Properties.html

@@ -304,7 +304,7 @@
     <a id="10217" href="Cubical.Categories.Functor.Properties.html#10217" class="Function">isFaithfulG∘F</a> <a id="10231" class="Symbol">:</a> <a id="10233" href="Cubical.Categories.Functor.Base.html#942" class="Function">isFaithful</a> <a id="10244" class="Symbol">(</a><a id="10245" href="Cubical.Categories.Functor.Properties.html#9399" class="Bound">G</a> <a id="10247" href="Cubical.Categories.Functor.Base.html#4744" class="Function Operator">∘F</a> <a id="10250" href="Cubical.Categories.Functor.Properties.html#9381" class="Bound">F</a><a id="10251" class="Symbol">)</a>
     <a id="10257" href="Cubical.Categories.Functor.Properties.html#10217" class="Function">isFaithfulG∘F</a> <a id="10271" href="Cubical.Categories.Functor.Properties.html#10271" class="Bound">x</a> <a id="10273" href="Cubical.Categories.Functor.Properties.html#10273" class="Bound">y</a> <a id="10275" class="Symbol">=</a>
       <a id="10283" href="Cubical.Functions.Embedding.html#1582" class="Function">isEmbedding→Inj</a>
-        <a id="10307" class="Symbol">(</a><a id="10308" href="Cubical.Functions.Embedding.html#8508" class="Function">compEmbedding</a>
+        <a id="10307" class="Symbol">(</a><a id="10308" href="Cubical.Functions.Embedding.html#8612" class="Function">compEmbedding</a>
         <a id="10330" class="Symbol">((λ</a> <a id="10334" href="Cubical.Categories.Functor.Properties.html#10334" class="Bound">v</a> <a id="10336" class="Symbol">→</a> <a id="10338" href="Cubical.Categories.Functor.Base.html#604" class="Field">F-hom</a> <a id="10344" href="Cubical.Categories.Functor.Properties.html#9399" class="Bound">G</a> <a id="10346" href="Cubical.Categories.Functor.Properties.html#10334" class="Bound">v</a><a id="10347" class="Symbol">)</a> <a id="10349" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a>
           <a id="10361" class="Symbol">(</a><a id="10362" href="Cubical.Functions.Embedding.html#5099" class="Function">injEmbedding</a> <a id="10375" class="Symbol">(</a><a id="10376" href="Cubical.Categories.Functor.Properties.html#9413" class="Bound">E</a> <a id="10378" class="Symbol">.</a><a id="10379" href="Cubical.Categories.Category.Base.html#807" class="Field">isSetHom</a><a id="10387" class="Symbol">)</a> <a id="10389" class="Symbol">(</a><a id="10390" href="Cubical.Categories.Functor.Properties.html#10174" class="Bound">isFaithfulG</a> <a id="10402" class="Symbol">(</a><a id="10403" href="Cubical.Categories.Functor.Properties.html#9381" class="Bound">F</a> <a id="10405" href="Cubical.Categories.Functor.Base.html#3683" class="Function Operator">⟅</a> <a id="10407" href="Cubical.Categories.Functor.Properties.html#10271" class="Bound">x</a> <a id="10409" href="Cubical.Categories.Functor.Base.html#3683" class="Function Operator">⟆</a><a id="10410" class="Symbol">)</a> <a id="10412" class="Symbol">(</a><a id="10413" href="Cubical.Categories.Functor.Properties.html#9381" class="Bound">F</a> <a id="10415" href="Cubical.Categories.Functor.Base.html#3683" class="Function Operator">⟅</a> <a id="10417" href="Cubical.Categories.Functor.Properties.html#10273" class="Bound">y</a> <a id="10419" href="Cubical.Categories.Functor.Base.html#3683" class="Function Operator">⟆</a><a id="10420" class="Symbol">)</a> <a id="10422" class="Symbol">_</a> <a id="10424" class="Symbol">_)))</a>
         <a id="10437" class="Symbol">((λ</a> <a id="10441" href="Cubical.Categories.Functor.Properties.html#10441" class="Bound">z</a> <a id="10443" class="Symbol">→</a> <a id="10445" href="Cubical.Categories.Functor.Base.html#604" class="Field">F-hom</a> <a id="10451" href="Cubical.Categories.Functor.Properties.html#9381" class="Bound">F</a> <a id="10453" href="Cubical.Categories.Functor.Properties.html#10441" class="Bound">z</a><a id="10454" class="Symbol">)</a> <a id="10456" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a>

Cubical.Codata.Conat.Properties.html

@@ -259,7 +259,7 @@
   <a id="7186" class="Keyword">module</a> <a id="7193" href="Cubical.Codata.Conat.Properties.html#7193" class="Module">_</a> <a id="7195" class="Symbol">(</a><a id="7196" href="Cubical.Codata.Conat.Properties.html#7196" class="Bound">f</a> <a id="7198" class="Symbol">:</a> <a id="7200" href="Cubical.Codata.Conat.Base.html#855" class="Record">Conat</a> <a id="7206" class="Symbol">→</a> <a id="7208" href="Agda.Builtin.Nat.html#203" class="Datatype">Nat.ℕ</a><a id="7213" class="Symbol">)</a> <a id="7215" class="Symbol">(</a><a id="7216" href="Cubical.Codata.Conat.Properties.html#7216" class="Bound">emb</a> <a id="7220" class="Symbol">:</a> <a id="7222" href="Cubical.Functions.Embedding.html#1319" class="Function">isEmbedding</a> <a id="7234" href="Cubical.Codata.Conat.Properties.html#7196" class="Bound">f</a><a id="7235" class="Symbol">)</a> <a id="7237" class="Keyword">where</a>
     <a id="7247" href="Cubical.Codata.Conat.Properties.html#7247" class="Function">discreteConat</a> <a id="7261" class="Symbol">:</a> <a id="7263" href="Cubical.Relation.Nullary.Base.html#1515" class="Function">Discrete</a> <a id="7272" href="Cubical.Codata.Conat.Base.html#855" class="Record">Conat</a>
     <a id="7282" href="Cubical.Codata.Conat.Properties.html#7247" class="Function">discreteConat</a>
-      <a id="7302" class="Symbol">=</a> <a id="7304" href="Cubical.Functions.Embedding.html#6286" class="Function">Embedding-into-Discrete→Discrete</a> <a id="7337" class="Symbol">(</a><a id="7338" href="Cubical.Codata.Conat.Properties.html#7196" class="Bound">f</a> <a id="7340" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="7342" href="Cubical.Codata.Conat.Properties.html#7216" class="Bound">emb</a><a id="7345" class="Symbol">)</a> <a id="7347" href="Cubical.Data.Nat.Properties.html#3394" class="Function">Nat.discreteℕ</a>
+      <a id="7302" class="Symbol">=</a> <a id="7304" href="Cubical.Functions.Embedding.html#6390" class="Function">Embedding-into-Discrete→Discrete</a> <a id="7337" class="Symbol">(</a><a id="7338" href="Cubical.Codata.Conat.Properties.html#7196" class="Bound">f</a> <a id="7340" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="7342" href="Cubical.Codata.Conat.Properties.html#7216" class="Bound">emb</a><a id="7345" class="Symbol">)</a> <a id="7347" href="Cubical.Data.Nat.Properties.html#3394" class="Function">Nat.discreteℕ</a>
 
     <a id="7366" href="Cubical.Codata.Conat.Properties.html#7366" class="Function">wlpo&#39;</a> <a id="7372" class="Symbol">:</a> <a id="7374" href="Cubical.Axiom.Omniscience.html#1399" class="Function">Omni.WLPO&#39;</a> <a id="7385" href="Agda.Builtin.Nat.html#203" class="Datatype">Nat.ℕ</a>
     <a id="7395" href="Cubical.Codata.Conat.Properties.html#7366" class="Function">wlpo&#39;</a> <a id="7401" href="Cubical.Codata.Conat.Properties.html#7401" class="Bound">α</a> <a id="7403" class="Keyword">with</a> <a id="7408" href="Cubical.Codata.Conat.Properties.html#7247" class="Function">discreteConat</a> <a id="7422" class="Symbol">(</a><a id="7423" href="Cubical.Codata.Conat.Properties.html#6152" class="Function">search</a> <a id="7430" href="Cubical.Codata.Conat.Properties.html#7401" class="Bound">α</a><a id="7431" class="Symbol">)</a> <a id="7433" href="Cubical.Codata.Conat.Properties.html#1707" class="Function">∞</a>

Cubical.Codata.M.helper.html

@@ -32,7 +32,7 @@
   <a id="836" class="Symbol">→</a> <a id="838" class="Symbol">∀</a> <a id="840" class="Symbol">{</a><a id="841" href="Cubical.Codata.M.helper.html#841" class="Bound">f</a> <a id="843" href="Cubical.Codata.M.helper.html#843" class="Bound">g</a> <a id="845" class="Symbol">:</a> <a id="847" href="Cubical.Codata.M.helper.html#805" class="Bound">C</a> <a id="849" class="Symbol">-&gt;</a> <a id="852" href="Cubical.Codata.M.helper.html#801" class="Bound">A</a><a id="853" class="Symbol">}</a>
   <a id="857" class="Symbol">→</a> <a id="859" class="Symbol">(</a><a id="860" href="Cubical.Codata.M.helper.html#860" class="Bound">x</a> <a id="862" class="Symbol">:</a> <a id="864" href="Cubical.Codata.M.helper.html#805" class="Bound">C</a><a id="865" class="Symbol">)</a> <a id="867" class="Symbol">→</a> <a id="869" class="Symbol">(</a><a id="870" href="Cubical.Foundations.Isomorphism.html#856" class="Field">Iso.fun</a> <a id="878" href="Cubical.Codata.M.helper.html#818" class="Bound">isom</a> <a id="883" class="Symbol">(</a><a id="884" href="Cubical.Codata.M.helper.html#841" class="Bound">f</a> <a id="886" href="Cubical.Codata.M.helper.html#860" class="Bound">x</a><a id="887" class="Symbol">)</a> <a id="889" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="891" href="Cubical.Foundations.Isomorphism.html#856" class="Field">Iso.fun</a> <a id="899" href="Cubical.Codata.M.helper.html#818" class="Bound">isom</a> <a id="904" class="Symbol">(</a><a id="905" href="Cubical.Codata.M.helper.html#843" class="Bound">g</a> <a id="907" href="Cubical.Codata.M.helper.html#860" class="Bound">x</a><a id="908" class="Symbol">))</a> <a id="911" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="913" class="Symbol">(</a><a id="914" href="Cubical.Codata.M.helper.html#841" class="Bound">f</a> <a id="916" href="Cubical.Codata.M.helper.html#860" class="Bound">x</a> <a id="918" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="920" href="Cubical.Codata.M.helper.html#843" class="Bound">g</a> <a id="922" href="Cubical.Codata.M.helper.html#860" class="Bound">x</a><a id="923" class="Symbol">)</a>
 <a id="925" href="Cubical.Codata.M.helper.html#772" class="Function">iso→fun-Injection</a> <a id="943" class="Symbol">{</a><a id="944" class="Argument">A</a> <a id="946" class="Symbol">=</a> <a id="948" href="Cubical.Codata.M.helper.html#948" class="Bound">A</a><a id="949" class="Symbol">}</a> <a id="951" class="Symbol">{</a><a id="952" href="Cubical.Codata.M.helper.html#952" class="Bound">B</a><a id="953" class="Symbol">}</a> <a id="955" class="Symbol">{</a><a id="956" href="Cubical.Codata.M.helper.html#956" class="Bound">C</a><a id="957" class="Symbol">}</a> <a id="959" href="Cubical.Codata.M.helper.html#959" class="Bound">isom</a> <a id="964" class="Symbol">{</a><a id="965" class="Argument">f</a> <a id="967" class="Symbol">=</a> <a id="969" href="Cubical.Codata.M.helper.html#969" class="Bound">f</a><a id="970" class="Symbol">}</a> <a id="972" class="Symbol">{</a><a id="973" href="Cubical.Codata.M.helper.html#973" class="Bound">g</a><a id="974" class="Symbol">}</a> <a id="976" class="Symbol">=</a>
-  <a id="980" href="Cubical.Functions.Embedding.html#6031" class="Function">isEmbedding→Injection</a> <a id="1002" class="Symbol">{</a><a id="1003" class="Argument">A</a> <a id="1005" class="Symbol">=</a> <a id="1007" href="Cubical.Codata.M.helper.html#948" class="Bound">A</a><a id="1008" class="Symbol">}</a> <a id="1010" class="Symbol">{</a><a id="1011" href="Cubical.Codata.M.helper.html#952" class="Bound">B</a><a id="1012" class="Symbol">}</a> <a id="1014" class="Symbol">{</a><a id="1015" href="Cubical.Codata.M.helper.html#956" class="Bound">C</a><a id="1016" class="Symbol">}</a> <a id="1018" class="Symbol">(</a><a id="1019" href="Cubical.Foundations.Isomorphism.html#856" class="Field">Iso.fun</a> <a id="1027" href="Cubical.Codata.M.helper.html#959" class="Bound">isom</a><a id="1031" class="Symbol">)</a> <a id="1033" class="Symbol">(</a><a id="1034" href="Cubical.Functions.Embedding.html#5815" class="Function">iso→isEmbedding</a> <a id="1050" class="Symbol">{</a><a id="1051" class="Argument">A</a> <a id="1053" class="Symbol">=</a> <a id="1055" href="Cubical.Codata.M.helper.html#948" class="Bound">A</a><a id="1056" class="Symbol">}</a> <a id="1058" class="Symbol">{</a><a id="1059" href="Cubical.Codata.M.helper.html#952" class="Bound">B</a><a id="1060" class="Symbol">}</a> <a id="1062" href="Cubical.Codata.M.helper.html#959" class="Bound">isom</a><a id="1066" class="Symbol">)</a> <a id="1068" class="Symbol">{</a><a id="1069" class="Argument">f</a> <a id="1071" class="Symbol">=</a> <a id="1073" href="Cubical.Codata.M.helper.html#969" class="Bound">f</a><a id="1074" class="Symbol">}</a> <a id="1076" class="Symbol">{</a><a id="1077" class="Argument">g</a> <a id="1079" class="Symbol">=</a> <a id="1081" href="Cubical.Codata.M.helper.html#973" class="Bound">g</a><a id="1082" class="Symbol">}</a>
+  <a id="980" href="Cubical.Functions.Embedding.html#6135" class="Function">isEmbedding→Injection</a> <a id="1002" class="Symbol">{</a><a id="1003" class="Argument">A</a> <a id="1005" class="Symbol">=</a> <a id="1007" href="Cubical.Codata.M.helper.html#948" class="Bound">A</a><a id="1008" class="Symbol">}</a> <a id="1010" class="Symbol">{</a><a id="1011" href="Cubical.Codata.M.helper.html#952" class="Bound">B</a><a id="1012" class="Symbol">}</a> <a id="1014" class="Symbol">{</a><a id="1015" href="Cubical.Codata.M.helper.html#956" class="Bound">C</a><a id="1016" class="Symbol">}</a> <a id="1018" class="Symbol">(</a><a id="1019" href="Cubical.Foundations.Isomorphism.html#856" class="Field">Iso.fun</a> <a id="1027" href="Cubical.Codata.M.helper.html#959" class="Bound">isom</a><a id="1031" class="Symbol">)</a> <a id="1033" class="Symbol">(</a><a id="1034" href="Cubical.Functions.Embedding.html#5815" class="Function">iso→isEmbedding</a> <a id="1050" class="Symbol">{</a><a id="1051" class="Argument">A</a> <a id="1053" class="Symbol">=</a> <a id="1055" href="Cubical.Codata.M.helper.html#948" class="Bound">A</a><a id="1056" class="Symbol">}</a> <a id="1058" class="Symbol">{</a><a id="1059" href="Cubical.Codata.M.helper.html#952" class="Bound">B</a><a id="1060" class="Symbol">}</a> <a id="1062" href="Cubical.Codata.M.helper.html#959" class="Bound">isom</a><a id="1066" class="Symbol">)</a> <a id="1068" class="Symbol">{</a><a id="1069" class="Argument">f</a> <a id="1071" class="Symbol">=</a> <a id="1073" href="Cubical.Codata.M.helper.html#969" class="Bound">f</a><a id="1074" class="Symbol">}</a> <a id="1076" class="Symbol">{</a><a id="1077" class="Argument">g</a> <a id="1079" class="Symbol">=</a> <a id="1081" href="Cubical.Codata.M.helper.html#973" class="Bound">g</a><a id="1082" class="Symbol">}</a>
 
 <a id="1085" class="Keyword">abstract</a>
   <a id="iso→Pi-fun-Injection"></a><a id="1096" href="Cubical.Codata.M.helper.html#1096" class="Function">iso→Pi-fun-Injection</a> <a id="1117" class="Symbol">:</a>