Deploying to gh-pages from @ 7a6d419 🚀

Author: mortberg

Cubical.Categories.Constructions.Elements.Properties.html

@@ -9,22 +9,22 @@
 <a id="144" class="Keyword">open</a> <a id="149" class="Keyword">import</a> <a id="156" href="Cubical.Categories.Category.Base.html" class="Module">Cubical.Categories.Category.Base</a>
 <a id="189" class="Keyword">open</a> <a id="194" class="Keyword">import</a> <a id="201" href="Cubical.Categories.Functor.Base.html" class="Module">Cubical.Categories.Functor.Base</a>
 <a id="233" class="Keyword">open</a> <a id="238" class="Keyword">import</a> <a id="245" href="Cubical.Categories.Constructions.Elements.html" class="Module">Cubical.Categories.Constructions.Elements</a>
-<a id="287" class="Keyword">open</a> <a id="292" href="Cubical.Categories.Constructions.Elements.html#798" class="Module">Covariant</a>
+<a id="287" class="Keyword">open</a> <a id="292" href="Cubical.Categories.Constructions.Elements.html#504" class="Module">Covariant</a>
 <a id="302" class="Keyword">open</a> <a id="307" class="Keyword">import</a> <a id="314" href="Cubical.Categories.Functors.HomFunctor.html" class="Module">Cubical.Categories.Functors.HomFunctor</a>
 <a id="353" class="Keyword">open</a> <a id="358" class="Keyword">import</a> <a id="365" href="Cubical.Categories.Constructions.BinProduct.html" class="Module">Cubical.Categories.Constructions.BinProduct</a>
 
 <a id="410" class="Keyword">private</a>
   <a id="420" class="Keyword">variable</a>
     <a id="433" href="Cubical.Categories.Constructions.TwistedArrow.html#433" class="Generalizable">ℓ</a> <a id="435" href="Cubical.Categories.Constructions.TwistedArrow.html#435" class="Generalizable">ℓ&#39;</a> <a id="438" class="Symbol">:</a> <a id="440" href="Agda.Primitive.html#742" class="Postulate">Level</a>
 <a id="TwistedArrowCategory"></a><a id="446" href="Cubical.Categories.Constructions.TwistedArrow.html#446" class="Function">TwistedArrowCategory</a> <a id="467" class="Symbol">:</a> <a id="469" class="Symbol">(</a><a id="470" href="Cubical.Categories.Constructions.TwistedArrow.html#470" class="Bound">C</a> <a id="472" class="Symbol">:</a> <a id="474" href="Cubical.Categories.Category.Base.html#311" class="Record">Category</a> <a id="483" href="Cubical.Categories.Constructions.TwistedArrow.html#433" class="Generalizable">ℓ</a> <a id="485" href="Cubical.Categories.Constructions.TwistedArrow.html#435" class="Generalizable">ℓ&#39;</a><a id="487" class="Symbol">)</a> <a id="489" class="Symbol">→</a> <a id="491" href="Cubical.Categories.Category.Base.html#311" class="Record">Category</a> <a id="500" class="Symbol">(</a><a id="501" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="507" href="Cubical.Categories.Constructions.TwistedArrow.html#433" class="Generalizable">ℓ</a> <a id="509" href="Cubical.Categories.Constructions.TwistedArrow.html#435" class="Generalizable">ℓ&#39;</a><a id="511" class="Symbol">)</a> <a id="513" href="Cubical.Categories.Constructions.TwistedArrow.html#435" class="Generalizable">ℓ&#39;</a>
-<a id="516" href="Cubical.Categories.Constructions.TwistedArrow.html#446" class="Function">TwistedArrowCategory</a> <a id="537" href="Cubical.Categories.Constructions.TwistedArrow.html#537" class="Bound">C</a> <a id="539" class="Symbol">=</a> <a id="541" href="Cubical.Categories.Constructions.Elements.html#1092" class="Function Operator">∫</a> <a id="543" href="Cubical.Categories.Functors.HomFunctor.html#395" class="Function">HomFunctor</a> <a id="554" href="Cubical.Categories.Constructions.TwistedArrow.html#537" class="Bound">C</a>
+<a id="516" href="Cubical.Categories.Constructions.TwistedArrow.html#446" class="Function">TwistedArrowCategory</a> <a id="537" href="Cubical.Categories.Constructions.TwistedArrow.html#537" class="Bound">C</a> <a id="539" class="Symbol">=</a> <a id="541" href="Cubical.Categories.Constructions.Elements.html#821" class="Function Operator">∫</a> <a id="543" href="Cubical.Categories.Functors.HomFunctor.html#395" class="Function">HomFunctor</a> <a id="554" href="Cubical.Categories.Constructions.TwistedArrow.html#537" class="Bound">C</a>
 
 <a id="TwistedEnds"></a><a id="557" href="Cubical.Categories.Constructions.TwistedArrow.html#557" class="Function">TwistedEnds</a> <a id="569" class="Symbol">:</a> <a id="571" class="Symbol">(</a><a id="572" href="Cubical.Categories.Constructions.TwistedArrow.html#572" class="Bound">C</a> <a id="574" class="Symbol">:</a> <a id="576" href="Cubical.Categories.Category.Base.html#311" class="Record">Category</a> <a id="585" href="Cubical.Categories.Constructions.TwistedArrow.html#433" class="Generalizable">ℓ</a> <a id="587" href="Cubical.Categories.Constructions.TwistedArrow.html#435" class="Generalizable">ℓ&#39;</a><a id="589" class="Symbol">)</a> <a id="591" class="Symbol">→</a> <a id="593" href="Cubical.Categories.Functor.Base.html#418" class="Record">Functor</a> <a id="601" class="Symbol">(</a><a id="602" href="Cubical.Categories.Constructions.TwistedArrow.html#446" class="Function">TwistedArrowCategory</a> <a id="623" href="Cubical.Categories.Constructions.TwistedArrow.html#572" class="Bound">C</a><a id="624" class="Symbol">)</a> <a id="626" class="Symbol">(</a><a id="627" href="Cubical.Categories.Constructions.TwistedArrow.html#572" class="Bound">C</a> <a id="629" href="Cubical.Categories.Category.Base.html#4469" class="Function Operator">^op</a> <a id="633" href="Cubical.Categories.Constructions.BinProduct.html#422" class="Function Operator">×C</a> <a id="636" href="Cubical.Categories.Constructions.TwistedArrow.html#572" class="Bound">C</a><a id="637" class="Symbol">)</a>
-<a id="639" href="Cubical.Categories.Constructions.TwistedArrow.html#557" class="Function">TwistedEnds</a> <a id="651" href="Cubical.Categories.Constructions.TwistedArrow.html#651" class="Bound">C</a> <a id="653" class="Symbol">=</a> <a id="655" href="Cubical.Categories.Constructions.Elements.html#3384" class="Function">ForgetElements</a> <a id="670" class="Symbol">(</a><a id="671" href="Cubical.Categories.Functors.HomFunctor.html#395" class="Function">HomFunctor</a> <a id="682" href="Cubical.Categories.Constructions.TwistedArrow.html#651" class="Bound">C</a><a id="683" class="Symbol">)</a>
+<a id="639" href="Cubical.Categories.Constructions.TwistedArrow.html#557" class="Function">TwistedEnds</a> <a id="651" href="Cubical.Categories.Constructions.TwistedArrow.html#651" class="Bound">C</a> <a id="653" class="Symbol">=</a> <a id="655" href="Cubical.Categories.Constructions.Elements.html#1782" class="Function">ForgetElements</a> <a id="670" class="Symbol">(</a><a id="671" href="Cubical.Categories.Functors.HomFunctor.html#395" class="Function">HomFunctor</a> <a id="682" href="Cubical.Categories.Constructions.TwistedArrow.html#651" class="Bound">C</a><a id="683" class="Symbol">)</a>
 
 <a id="TwistedDom"></a><a id="686" href="Cubical.Categories.Constructions.TwistedArrow.html#686" class="Function">TwistedDom</a> <a id="697" class="Symbol">:</a> <a id="699" class="Symbol">(</a><a id="700" href="Cubical.Categories.Constructions.TwistedArrow.html#700" class="Bound">C</a> <a id="702" class="Symbol">:</a> <a id="704" href="Cubical.Categories.Category.Base.html#311" class="Record">Category</a> <a id="713" href="Cubical.Categories.Constructions.TwistedArrow.html#433" class="Generalizable">ℓ</a> <a id="715" href="Cubical.Categories.Constructions.TwistedArrow.html#435" class="Generalizable">ℓ&#39;</a><a id="717" class="Symbol">)</a> <a id="719" class="Symbol">→</a> <a id="721" href="Cubical.Categories.Functor.Base.html#418" class="Record">Functor</a> <a id="729" class="Symbol">((</a><a id="731" href="Cubical.Categories.Constructions.TwistedArrow.html#446" class="Function">TwistedArrowCategory</a> <a id="752" href="Cubical.Categories.Constructions.TwistedArrow.html#700" class="Bound">C</a><a id="753" class="Symbol">)</a> <a id="755" href="Cubical.Categories.Category.Base.html#4469" class="Function Operator">^op</a><a id="758" class="Symbol">)</a> <a id="760" href="Cubical.Categories.Constructions.TwistedArrow.html#700" class="Bound">C</a>
-<a id="762" href="Cubical.Categories.Constructions.TwistedArrow.html#686" class="Function">TwistedDom</a> <a id="773" href="Cubical.Categories.Constructions.TwistedArrow.html#773" class="Bound">C</a> <a id="775" class="Symbol">=</a> <a id="777" class="Symbol">((</a><a id="779" href="Cubical.Categories.Constructions.BinProduct.html#935" class="Function">Fst</a> <a id="783" class="Symbol">(</a><a id="784" href="Cubical.Categories.Constructions.TwistedArrow.html#773" class="Bound">C</a> <a id="786" href="Cubical.Categories.Category.Base.html#4469" class="Function Operator">^op</a><a id="789" class="Symbol">)</a> <a id="791" href="Cubical.Categories.Constructions.TwistedArrow.html#773" class="Bound">C</a><a id="792" class="Symbol">)</a> <a id="794" href="Cubical.Categories.Functor.Base.html#5007" class="Function Operator">^opF</a><a id="798" class="Symbol">)</a> <a id="800" href="Cubical.Categories.Functor.Base.html#4744" class="Function Operator">∘F</a> <a id="803" class="Symbol">(</a><a id="804" href="Cubical.Categories.Constructions.Elements.html#3384" class="Function">ForgetElements</a> <a id="819" class="Symbol">(</a><a id="820" href="Cubical.Categories.Functors.HomFunctor.html#395" class="Function">HomFunctor</a> <a id="831" href="Cubical.Categories.Constructions.TwistedArrow.html#773" class="Bound">C</a><a id="832" class="Symbol">)</a> <a id="834" href="Cubical.Categories.Functor.Base.html#5007" class="Function Operator">^opF</a><a id="838" class="Symbol">)</a>
+<a id="762" href="Cubical.Categories.Constructions.TwistedArrow.html#686" class="Function">TwistedDom</a> <a id="773" href="Cubical.Categories.Constructions.TwistedArrow.html#773" class="Bound">C</a> <a id="775" class="Symbol">=</a> <a id="777" class="Symbol">((</a><a id="779" href="Cubical.Categories.Constructions.BinProduct.html#935" class="Function">Fst</a> <a id="783" class="Symbol">(</a><a id="784" href="Cubical.Categories.Constructions.TwistedArrow.html#773" class="Bound">C</a> <a id="786" href="Cubical.Categories.Category.Base.html#4469" class="Function Operator">^op</a><a id="789" class="Symbol">)</a> <a id="791" href="Cubical.Categories.Constructions.TwistedArrow.html#773" class="Bound">C</a><a id="792" class="Symbol">)</a> <a id="794" href="Cubical.Categories.Functor.Base.html#5007" class="Function Operator">^opF</a><a id="798" class="Symbol">)</a> <a id="800" href="Cubical.Categories.Functor.Base.html#4744" class="Function Operator">∘F</a> <a id="803" class="Symbol">(</a><a id="804" href="Cubical.Categories.Constructions.Elements.html#1782" class="Function">ForgetElements</a> <a id="819" class="Symbol">(</a><a id="820" href="Cubical.Categories.Functors.HomFunctor.html#395" class="Function">HomFunctor</a> <a id="831" href="Cubical.Categories.Constructions.TwistedArrow.html#773" class="Bound">C</a><a id="832" class="Symbol">)</a> <a id="834" href="Cubical.Categories.Functor.Base.html#5007" class="Function Operator">^opF</a><a id="838" class="Symbol">)</a>
 
 <a id="TwistedCod"></a><a id="841" href="Cubical.Categories.Constructions.TwistedArrow.html#841" class="Function">TwistedCod</a> <a id="852" class="Symbol">:</a> <a id="854" class="Symbol">(</a><a id="855" href="Cubical.Categories.Constructions.TwistedArrow.html#855" class="Bound">C</a> <a id="857" class="Symbol">:</a> <a id="859" href="Cubical.Categories.Category.Base.html#311" class="Record">Category</a> <a id="868" href="Cubical.Categories.Constructions.TwistedArrow.html#433" class="Generalizable">ℓ</a> <a id="870" href="Cubical.Categories.Constructions.TwistedArrow.html#435" class="Generalizable">ℓ&#39;</a><a id="872" class="Symbol">)</a> <a id="874" class="Symbol">→</a> <a id="876" href="Cubical.Categories.Functor.Base.html#418" class="Record">Functor</a> <a id="884" class="Symbol">(</a><a id="885" href="Cubical.Categories.Constructions.TwistedArrow.html#446" class="Function">TwistedArrowCategory</a> <a id="906" href="Cubical.Categories.Constructions.TwistedArrow.html#855" class="Bound">C</a><a id="907" class="Symbol">)</a> <a id="909" href="Cubical.Categories.Constructions.TwistedArrow.html#855" class="Bound">C</a>
-<a id="911" href="Cubical.Categories.Constructions.TwistedArrow.html#841" class="Function">TwistedCod</a> <a id="922" href="Cubical.Categories.Constructions.TwistedArrow.html#922" class="Bound">C</a> <a id="924" class="Symbol">=</a> <a id="926" class="Symbol">(</a><a id="927" href="Cubical.Categories.Constructions.BinProduct.html#1101" class="Function">Snd</a> <a id="931" class="Symbol">(</a><a id="932" href="Cubical.Categories.Constructions.TwistedArrow.html#922" class="Bound">C</a> <a id="934" href="Cubical.Categories.Category.Base.html#4469" class="Function Operator">^op</a><a id="937" class="Symbol">)</a> <a id="939" href="Cubical.Categories.Constructions.TwistedArrow.html#922" class="Bound">C</a><a id="940" class="Symbol">)</a> <a id="942" href="Cubical.Categories.Functor.Base.html#4744" class="Function Operator">∘F</a> <a id="945" href="Cubical.Categories.Constructions.Elements.html#3384" class="Function">ForgetElements</a> <a id="960" class="Symbol">(</a><a id="961" href="Cubical.Categories.Functors.HomFunctor.html#395" class="Function">HomFunctor</a> <a id="972" href="Cubical.Categories.Constructions.TwistedArrow.html#922" class="Bound">C</a><a id="973" class="Symbol">)</a>
+<a id="911" href="Cubical.Categories.Constructions.TwistedArrow.html#841" class="Function">TwistedCod</a> <a id="922" href="Cubical.Categories.Constructions.TwistedArrow.html#922" class="Bound">C</a> <a id="924" class="Symbol">=</a> <a id="926" class="Symbol">(</a><a id="927" href="Cubical.Categories.Constructions.BinProduct.html#1101" class="Function">Snd</a> <a id="931" class="Symbol">(</a><a id="932" href="Cubical.Categories.Constructions.TwistedArrow.html#922" class="Bound">C</a> <a id="934" href="Cubical.Categories.Category.Base.html#4469" class="Function Operator">^op</a><a id="937" class="Symbol">)</a> <a id="939" href="Cubical.Categories.Constructions.TwistedArrow.html#922" class="Bound">C</a><a id="940" class="Symbol">)</a> <a id="942" href="Cubical.Categories.Functor.Base.html#4744" class="Function Operator">∘F</a> <a id="945" href="Cubical.Categories.Constructions.Elements.html#1782" class="Function">ForgetElements</a> <a id="960" class="Symbol">(</a><a id="961" href="Cubical.Categories.Functors.HomFunctor.html#395" class="Function">HomFunctor</a> <a id="972" href="Cubical.Categories.Constructions.TwistedArrow.html#922" class="Bound">C</a><a id="973" class="Symbol">)</a>
 </pre></body></html>