Deploying to gh-pages from @ 5b96b28 🚀

Cubical.HITs.Nullification.html

@@ -5,4 +5,6 @@
 <a id="65" class="Keyword">open</a> <a id="70" class="Keyword">import</a> <a id="77" href="Cubical.HITs.Nullification.Base.html" class="Module">Cubical.HITs.Nullification.Base</a> <a id="109" class="Keyword">public</a>
 
 <a id="117" class="Keyword">open</a> <a id="122" class="Keyword">import</a> <a id="129" href="Cubical.HITs.Nullification.Properties.html" class="Module">Cubical.HITs.Nullification.Properties</a> <a id="167" class="Keyword">public</a>
+
+<a id="175" class="Keyword">open</a> <a id="180" class="Keyword">import</a> <a id="187" href="Cubical.HITs.Nullification.Topological.html" class="Module">Cubical.HITs.Nullification.Topological</a> <a id="226" class="Keyword">public</a>
 </pre></body></html>

Cubical.HITs.Truncation.FromNegTwo.Properties.html

@@ -20,7 +20,7 @@
 <a id="638" class="Keyword">open</a> <a id="643" class="Keyword">import</a> <a id="650" href="Cubical.Data.Sigma.html" class="Module">Cubical.Data.Sigma</a>
 <a id="669" class="Keyword">open</a> <a id="674" class="Keyword">import</a> <a id="681" href="Cubical.HITs.Sn.Base.html" class="Module">Cubical.HITs.Sn.Base</a>
 <a id="702" class="Keyword">open</a> <a id="707" class="Keyword">import</a> <a id="714" href="Cubical.HITs.Susp.Base.html" class="Module">Cubical.HITs.Susp.Base</a>
-<a id="737" class="Keyword">open</a> <a id="742" class="Keyword">import</a> <a id="749" href="Cubical.HITs.Nullification.html" class="Module">Cubical.HITs.Nullification</a> <a id="776" class="Symbol">as</a> <a id="779" class="Module">Null</a> <a id="784" class="Keyword">hiding</a> <a id="791" class="Symbol">(</a><a id="792" href="Cubical.HITs.Nullification.Properties.html#2332" class="Function">rec</a><a id="795" class="Symbol">;</a> <a id="797" href="Cubical.HITs.Nullification.Properties.html#3755" class="Function">elim</a><a id="801" class="Symbol">)</a>
+<a id="737" class="Keyword">open</a> <a id="742" class="Keyword">import</a> <a id="749" href="Cubical.HITs.Nullification.html" class="Module">Cubical.HITs.Nullification</a> <a id="776" class="Symbol">as</a> <a id="779" class="Module">Null</a> <a id="784" class="Keyword">hiding</a> <a id="791" class="Symbol">(</a><a id="792" href="Cubical.HITs.Nullification.Properties.html#2565" class="Function">rec</a><a id="795" class="Symbol">;</a> <a id="797" href="Cubical.HITs.Nullification.Properties.html#3858" class="Function">elim</a><a id="801" class="Symbol">)</a>
 
 <a id="804" class="Keyword">open</a> <a id="809" class="Keyword">import</a> <a id="816" href="Cubical.HITs.Truncation.FromNegTwo.Base.html" class="Module">Cubical.HITs.Truncation.FromNegTwo.Base</a>
 
@@ -122,15 +122,15 @@
       <a id="4984" class="Symbol">(</a><a id="4985" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1246" class="Generalizable">A</a> <a id="4987" class="Symbol">→</a> <a id="4989" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#4940" class="Bound">B</a><a id="4990" class="Symbol">)</a> <a id="4992" class="Symbol">→</a>
       <a id="5000" href="Cubical.HITs.Truncation.FromNegTwo.Base.html#1110" class="Function">hLevelTrunc</a> <a id="5012" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#4921" class="Bound">n</a> <a id="5014" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1246" class="Generalizable">A</a> <a id="5016" class="Symbol">→</a>
       <a id="5024" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#4940" class="Bound">B</a>
-<a id="5026" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#4914" class="Function">rec</a> <a id="5030" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5030" class="Bound">h</a> <a id="5032" class="Symbol">=</a> <a id="5034" href="Cubical.HITs.Nullification.Properties.html#2332" class="Function">Null.rec</a> <a id="5043" class="Symbol">(</a><a id="5044" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#3793" class="Function">isOfHLevel→isSnNull</a> <a id="5064" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5030" class="Bound">h</a><a id="5065" class="Symbol">)</a>
+<a id="5026" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#4914" class="Function">rec</a> <a id="5030" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5030" class="Bound">h</a> <a id="5032" class="Symbol">=</a> <a id="5034" href="Cubical.HITs.Nullification.Properties.html#2565" class="Function">Null.rec</a> <a id="5043" class="Symbol">(</a><a id="5044" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#3793" class="Function">isOfHLevel→isSnNull</a> <a id="5064" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5030" class="Bound">h</a><a id="5065" class="Symbol">)</a>
 
 <a id="elim"></a><a id="5068" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5068" class="Function">elim</a> <a id="5073" class="Symbol">:</a> <a id="5075" class="Symbol">{</a><a id="5076" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5076" class="Bound">n</a> <a id="5078" class="Symbol">:</a> <a id="5080" href="Cubical.Foundations.HLevels.html#854" class="Function">HLevel</a><a id="5086" class="Symbol">}</a>
        <a id="5095" class="Symbol">{</a><a id="5096" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5096" class="Bound">B</a> <a id="5098" class="Symbol">:</a> <a id="5100" href="Cubical.HITs.Truncation.FromNegTwo.Base.html#1110" class="Function">hLevelTrunc</a> <a id="5112" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5076" class="Bound">n</a> <a id="5114" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1246" class="Generalizable">A</a> <a id="5116" class="Symbol">→</a> <a id="5118" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="5123" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1231" class="Generalizable">ℓ&#39;</a><a id="5125" class="Symbol">}</a>
        <a id="5134" class="Symbol">(</a><a id="5135" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5135" class="Bound">hB</a> <a id="5138" class="Symbol">:</a> <a id="5140" class="Symbol">(</a><a id="5141" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5141" class="Bound">x</a> <a id="5143" class="Symbol">:</a> <a id="5145" href="Cubical.HITs.Truncation.FromNegTwo.Base.html#1110" class="Function">hLevelTrunc</a> <a id="5157" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5076" class="Bound">n</a> <a id="5159" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1246" class="Generalizable">A</a><a id="5160" class="Symbol">)</a> <a id="5162" class="Symbol">→</a> <a id="5164" href="Cubical.Foundations.HLevels.html#1313" class="Function">isOfHLevel</a> <a id="5175" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5076" class="Bound">n</a> <a id="5177" class="Symbol">(</a><a id="5178" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5096" class="Bound">B</a> <a id="5180" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5141" class="Bound">x</a><a id="5181" class="Symbol">))</a>
        <a id="5191" class="Symbol">(</a><a id="5192" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5192" class="Bound">g</a> <a id="5194" class="Symbol">:</a> <a id="5196" class="Symbol">(</a><a id="5197" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5197" class="Bound">a</a> <a id="5199" class="Symbol">:</a> <a id="5201" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1246" class="Generalizable">A</a><a id="5202" class="Symbol">)</a> <a id="5204" class="Symbol">→</a> <a id="5206" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5096" class="Bound">B</a> <a id="5208" class="Symbol">(</a><a id="5209" href="Cubical.HITs.Nullification.Base.html#475" class="InductiveConstructor Operator">∣</a> <a id="5211" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5197" class="Bound">a</a> <a id="5213" href="Cubical.HITs.Nullification.Base.html#475" class="InductiveConstructor Operator">∣</a><a id="5214" class="Symbol">))</a>
        <a id="5224" class="Symbol">(</a><a id="5225" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5225" class="Bound">x</a> <a id="5227" class="Symbol">:</a> <a id="5229" href="Cubical.HITs.Truncation.FromNegTwo.Base.html#1110" class="Function">hLevelTrunc</a> <a id="5241" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5076" class="Bound">n</a> <a id="5243" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1246" class="Generalizable">A</a><a id="5244" class="Symbol">)</a> <a id="5246" class="Symbol">→</a>
        <a id="5255" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5096" class="Bound">B</a> <a id="5257" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5225" class="Bound">x</a>
-<a id="5259" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5068" class="Function">elim</a> <a id="5264" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5264" class="Bound">hB</a> <a id="5267" class="Symbol">=</a> <a id="5269" href="Cubical.HITs.Nullification.Properties.html#3755" class="Function">Null.elim</a> <a id="5279" class="Symbol">(λ</a> <a id="5282" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5282" class="Bound">x</a> <a id="5284" class="Symbol">→</a> <a id="5286" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#3793" class="Function">isOfHLevel→isSnNull</a> <a id="5306" class="Symbol">(</a><a id="5307" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5264" class="Bound">hB</a> <a id="5310" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5282" class="Bound">x</a><a id="5311" class="Symbol">))</a>
+<a id="5259" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5068" class="Function">elim</a> <a id="5264" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5264" class="Bound">hB</a> <a id="5267" class="Symbol">=</a> <a id="5269" href="Cubical.HITs.Nullification.Properties.html#3858" class="Function">Null.elim</a> <a id="5279" class="Symbol">(λ</a> <a id="5282" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5282" class="Bound">x</a> <a id="5284" class="Symbol">→</a> <a id="5286" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#3793" class="Function">isOfHLevel→isSnNull</a> <a id="5306" class="Symbol">(</a><a id="5307" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5264" class="Bound">hB</a> <a id="5310" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5282" class="Bound">x</a><a id="5311" class="Symbol">))</a>
 
 <a id="elim2"></a><a id="5315" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5315" class="Function">elim2</a> <a id="5321" class="Symbol">:</a> <a id="5323" class="Symbol">{</a><a id="5324" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5324" class="Bound">n</a> <a id="5326" class="Symbol">:</a> <a id="5328" href="Cubical.Foundations.HLevels.html#854" class="Function">HLevel</a><a id="5334" class="Symbol">}</a>
   <a id="5338" class="Symbol">{</a><a id="5339" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5339" class="Bound">B</a> <a id="5341" class="Symbol">:</a> <a id="5343" href="Cubical.HITs.Truncation.FromNegTwo.Base.html#1110" class="Function">hLevelTrunc</a> <a id="5355" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5324" class="Bound">n</a> <a id="5357" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1246" class="Generalizable">A</a> <a id="5359" class="Symbol">→</a> <a id="5361" href="Cubical.HITs.Truncation.FromNegTwo.Base.html#1110" class="Function">hLevelTrunc</a> <a id="5373" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#5324" class="Bound">n</a> <a id="5375" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1246" class="Generalizable">A</a> <a id="5377" class="Symbol">→</a> <a id="5379" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="5384" href="Cubical.HITs.Truncation.FromNegTwo.Properties.html#1231" class="Generalizable">ℓ&#39;</a><a id="5386" class="Symbol">}</a>

Cubical.HITs.Truncation.Properties.html

@@ -26,7 +26,7 @@
 <a id="767" class="Keyword">open</a> <a id="772" class="Keyword">import</a> <a id="779" href="Cubical.HITs.Sn.Base.html" class="Module">Cubical.HITs.Sn.Base</a>
 <a id="800" class="Keyword">open</a> <a id="805" class="Keyword">import</a> <a id="812" href="Cubical.HITs.S1.html" class="Module">Cubical.HITs.S1</a> <a id="828" class="Keyword">hiding</a> <a id="835" class="Symbol">(</a><a id="836" href="Cubical.HITs.S1.Properties.html#434" class="Function">rec</a> <a id="840" class="Symbol">;</a> <a id="842" href="Cubical.HITs.S1.Properties.html#533" class="Function">elim</a><a id="846" class="Symbol">)</a>
 <a id="848" class="Keyword">open</a> <a id="853" class="Keyword">import</a> <a id="860" href="Cubical.HITs.Susp.Base.html" class="Module">Cubical.HITs.Susp.Base</a>
-<a id="883" class="Keyword">open</a> <a id="888" class="Keyword">import</a> <a id="895" href="Cubical.HITs.Nullification.html" class="Module">Cubical.HITs.Nullification</a> <a id="922" class="Symbol">as</a> <a id="925" class="Module">Null</a> <a id="930" class="Keyword">hiding</a> <a id="937" class="Symbol">(</a><a id="938" href="Cubical.HITs.Nullification.Properties.html#2332" class="Function">rec</a> <a id="942" class="Symbol">;</a> <a id="944" href="Cubical.HITs.Nullification.Properties.html#3755" class="Function">elim</a><a id="948" class="Symbol">)</a>
+<a id="883" class="Keyword">open</a> <a id="888" class="Keyword">import</a> <a id="895" href="Cubical.HITs.Nullification.html" class="Module">Cubical.HITs.Nullification</a> <a id="922" class="Symbol">as</a> <a id="925" class="Module">Null</a> <a id="930" class="Keyword">hiding</a> <a id="937" class="Symbol">(</a><a id="938" href="Cubical.HITs.Nullification.Properties.html#2565" class="Function">rec</a> <a id="942" class="Symbol">;</a> <a id="944" href="Cubical.HITs.Nullification.Properties.html#3858" class="Function">elim</a><a id="948" class="Symbol">)</a>
 
 <a id="951" class="Keyword">open</a> <a id="956" class="Keyword">import</a> <a id="963" href="Cubical.HITs.PropositionalTruncation.html" class="Module">Cubical.HITs.PropositionalTruncation</a> <a id="1000" class="Symbol">as</a> <a id="1003" class="Module">PropTrunc</a> <a id="1013" class="Keyword">using</a> <a id="1019" class="Symbol">(</a><a id="1020" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥_∥₁</a> <a id="1025" class="Symbol">;</a> <a id="1027" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣_∣₁</a> <a id="1032" class="Symbol">;</a> <a id="1034" href="Cubical.HITs.PropositionalTruncation.Base.html#308" class="InductiveConstructor">squash₁</a><a id="1041" class="Symbol">)</a>
 <a id="1043" class="Keyword">open</a> <a id="1048" class="Keyword">import</a> <a id="1055" href="Cubical.HITs.SetTruncation.html" class="Module">Cubical.HITs.SetTruncation</a>       <a id="1088" class="Symbol">as</a> <a id="1091" class="Module">SetTrunc</a>  <a id="1101" class="Keyword">using</a> <a id="1107" class="Symbol">(</a><a id="1108" href="Cubical.HITs.SetTruncation.Base.html#260" class="Datatype Operator">∥_∥₂</a><a id="1112" class="Symbol">;</a> <a id="1114" href="Cubical.HITs.SetTruncation.Base.html#299" class="InductiveConstructor Operator">∣_∣₂</a><a id="1118" class="Symbol">;</a> <a id="1120" href="Cubical.HITs.SetTruncation.Base.html#319" class="InductiveConstructor">squash₂</a><a id="1127" class="Symbol">)</a>

Cubical.Homotopy.Connected.html

@@ -26,7 +26,7 @@
 <a id="843" class="Keyword">open</a> <a id="848" class="Keyword">import</a> <a id="855" href="Cubical.Data.Sigma.html" class="Module">Cubical.Data.Sigma</a>
 <a id="874" class="Keyword">open</a> <a id="879" class="Keyword">import</a> <a id="886" href="Cubical.Data.Prod.Properties.html" class="Module">Cubical.Data.Prod.Properties</a>
 
-<a id="916" class="Keyword">open</a> <a id="921" class="Keyword">import</a> <a id="928" href="Cubical.HITs.Nullification.html" class="Module">Cubical.HITs.Nullification</a> <a id="955" class="Keyword">hiding</a> <a id="962" class="Symbol">(</a><a id="963" href="Cubical.HITs.Nullification.Properties.html#3755" class="Function">elim</a><a id="967" class="Symbol">)</a>
+<a id="916" class="Keyword">open</a> <a id="921" class="Keyword">import</a> <a id="928" href="Cubical.HITs.Nullification.html" class="Module">Cubical.HITs.Nullification</a> <a id="955" class="Keyword">hiding</a> <a id="962" class="Symbol">(</a><a id="963" href="Cubical.HITs.Nullification.Properties.html#3858" class="Function">elim</a><a id="967" class="Symbol">)</a>
 <a id="969" class="Keyword">open</a> <a id="974" class="Keyword">import</a> <a id="981" href="Cubical.HITs.Susp.html" class="Module">Cubical.HITs.Susp</a>
 <a id="999" class="Keyword">open</a> <a id="1004" class="Keyword">import</a> <a id="1011" href="Cubical.HITs.SmashProduct.html" class="Module">Cubical.HITs.SmashProduct</a>
 <a id="1037" class="Keyword">open</a> <a id="1042" class="Keyword">import</a> <a id="1049" href="Cubical.HITs.Pushout.html" class="Module">Cubical.HITs.Pushout</a>