Deploying to gh-pages from @ 7461251 🚀

Cubical.Categories.Constructions.TwistedArrow.html

@@ -10,22 +10,22 @@
 <a id="167" class="Keyword">open</a> <a id="172" class="Keyword">import</a> <a id="179" href="Cubical.Categories.Category.Base.html" class="Module">Cubical.Categories.Category.Base</a>
 <a id="212" class="Keyword">open</a> <a id="217" class="Keyword">import</a> <a id="224" href="Cubical.Categories.Functor.Base.html" class="Module">Cubical.Categories.Functor.Base</a>
 <a id="256" class="Keyword">open</a> <a id="261" class="Keyword">import</a> <a id="268" href="Cubical.Categories.Constructions.Elements.html" class="Module">Cubical.Categories.Constructions.Elements</a>
-<a id="310" class="Keyword">open</a> <a id="315" href="Cubical.Categories.Constructions.Elements.html#587" class="Module">Covariant</a>
+<a id="310" class="Keyword">open</a> <a id="315" href="Cubical.Categories.Constructions.Elements.html#758" class="Module">Covariant</a>
 <a id="325" class="Keyword">open</a> <a id="330" class="Keyword">import</a> <a id="337" href="Cubical.Categories.Functors.HomFunctor.html" class="Module">Cubical.Categories.Functors.HomFunctor</a>
 <a id="376" class="Keyword">open</a> <a id="381" class="Keyword">import</a> <a id="388" href="Cubical.Categories.Constructions.BinProduct.html" class="Module">Cubical.Categories.Constructions.BinProduct</a>
 
 <a id="433" class="Keyword">private</a>
   <a id="443" class="Keyword">variable</a>
     <a id="456" href="Cubical.Categories.Constructions.TwistedArrow.html#456" class="Generalizable">ℓ</a> <a id="458" href="Cubical.Categories.Constructions.TwistedArrow.html#458" class="Generalizable">ℓ&#39;</a> <a id="461" class="Symbol">:</a> <a id="463" href="Agda.Primitive.html#591" class="Postulate">Level</a>
 <a id="TwistedArrowCategory"></a><a id="469" href="Cubical.Categories.Constructions.TwistedArrow.html#469" class="Function">TwistedArrowCategory</a> <a id="490" class="Symbol">:</a> <a id="492" class="Symbol">(</a><a id="493" href="Cubical.Categories.Constructions.TwistedArrow.html#493" class="Bound">C</a> <a id="495" class="Symbol">:</a> <a id="497" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="506" href="Cubical.Categories.Constructions.TwistedArrow.html#456" class="Generalizable">ℓ</a> <a id="508" href="Cubical.Categories.Constructions.TwistedArrow.html#458" class="Generalizable">ℓ&#39;</a><a id="510" class="Symbol">)</a> <a id="512" class="Symbol">→</a> <a id="514" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="523" class="Symbol">(</a><a id="524" href="Agda.Primitive.html#804" class="Primitive">ℓ-max</a> <a id="530" href="Cubical.Categories.Constructions.TwistedArrow.html#456" class="Generalizable">ℓ</a> <a id="532" href="Cubical.Categories.Constructions.TwistedArrow.html#458" class="Generalizable">ℓ&#39;</a><a id="534" class="Symbol">)</a> <a id="536" href="Cubical.Categories.Constructions.TwistedArrow.html#458" class="Generalizable">ℓ&#39;</a>
-<a id="539" href="Cubical.Categories.Constructions.TwistedArrow.html#469" class="Function">TwistedArrowCategory</a> <a id="560" href="Cubical.Categories.Constructions.TwistedArrow.html#560" class="Bound">C</a> <a id="562" class="Symbol">=</a> <a id="564" href="Cubical.Categories.Constructions.Elements.html#901" class="Function Operator">∫</a> <a id="566" href="Cubical.Categories.Functors.HomFunctor.html#418" class="Function">HomFunctor</a> <a id="577" href="Cubical.Categories.Constructions.TwistedArrow.html#560" class="Bound">C</a>
+<a id="539" href="Cubical.Categories.Constructions.TwistedArrow.html#469" class="Function">TwistedArrowCategory</a> <a id="560" href="Cubical.Categories.Constructions.TwistedArrow.html#560" class="Bound">C</a> <a id="562" class="Symbol">=</a> <a id="564" href="Cubical.Categories.Constructions.Elements.html#1052" class="Function Operator">∫</a> <a id="566" href="Cubical.Categories.Functors.HomFunctor.html#418" class="Function">HomFunctor</a> <a id="577" href="Cubical.Categories.Constructions.TwistedArrow.html#560" class="Bound">C</a>
 
 <a id="TwistedEnds"></a><a id="580" href="Cubical.Categories.Constructions.TwistedArrow.html#580" class="Function">TwistedEnds</a> <a id="592" class="Symbol">:</a> <a id="594" class="Symbol">(</a><a id="595" href="Cubical.Categories.Constructions.TwistedArrow.html#595" class="Bound">C</a> <a id="597" class="Symbol">:</a> <a id="599" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="608" href="Cubical.Categories.Constructions.TwistedArrow.html#456" class="Generalizable">ℓ</a> <a id="610" href="Cubical.Categories.Constructions.TwistedArrow.html#458" class="Generalizable">ℓ&#39;</a><a id="612" class="Symbol">)</a> <a id="614" class="Symbol">→</a> <a id="616" href="Cubical.Categories.Functor.Base.html#397" class="Record">Functor</a> <a id="624" class="Symbol">(</a><a id="625" href="Cubical.Categories.Constructions.TwistedArrow.html#469" class="Function">TwistedArrowCategory</a> <a id="646" href="Cubical.Categories.Constructions.TwistedArrow.html#595" class="Bound">C</a><a id="647" class="Symbol">)</a> <a id="649" class="Symbol">(</a><a id="650" href="Cubical.Categories.Constructions.TwistedArrow.html#595" class="Bound">C</a> <a id="652" href="Cubical.Categories.Category.Base.html#4091" class="Function Operator">^op</a> <a id="656" href="Cubical.Categories.Constructions.BinProduct.html#445" class="Function Operator">×C</a> <a id="659" href="Cubical.Categories.Constructions.TwistedArrow.html#595" class="Bound">C</a><a id="660" class="Symbol">)</a>
-<a id="662" href="Cubical.Categories.Constructions.TwistedArrow.html#580" class="Function">TwistedEnds</a> <a id="674" href="Cubical.Categories.Constructions.TwistedArrow.html#674" class="Bound">C</a> <a id="676" class="Symbol">=</a> <a id="678" href="Cubical.Categories.Constructions.Elements.html#2948" class="Function">ForgetElements</a> <a id="693" class="Symbol">(</a><a id="694" href="Cubical.Categories.Functors.HomFunctor.html#418" class="Function">HomFunctor</a> <a id="705" href="Cubical.Categories.Constructions.TwistedArrow.html#674" class="Bound">C</a><a id="706" class="Symbol">)</a>
+<a id="662" href="Cubical.Categories.Constructions.TwistedArrow.html#580" class="Function">TwistedEnds</a> <a id="674" href="Cubical.Categories.Constructions.TwistedArrow.html#674" class="Bound">C</a> <a id="676" class="Symbol">=</a> <a id="678" href="Cubical.Categories.Constructions.Elements.html#3031" class="Function">ForgetElements</a> <a id="693" class="Symbol">(</a><a id="694" href="Cubical.Categories.Functors.HomFunctor.html#418" class="Function">HomFunctor</a> <a id="705" href="Cubical.Categories.Constructions.TwistedArrow.html#674" class="Bound">C</a><a id="706" class="Symbol">)</a>
 
 <a id="TwistedDom"></a><a id="709" href="Cubical.Categories.Constructions.TwistedArrow.html#709" class="Function">TwistedDom</a> <a id="720" class="Symbol">:</a> <a id="722" class="Symbol">(</a><a id="723" href="Cubical.Categories.Constructions.TwistedArrow.html#723" class="Bound">C</a> <a id="725" class="Symbol">:</a> <a id="727" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="736" href="Cubical.Categories.Constructions.TwistedArrow.html#456" class="Generalizable">ℓ</a> <a id="738" href="Cubical.Categories.Constructions.TwistedArrow.html#458" class="Generalizable">ℓ&#39;</a><a id="740" class="Symbol">)</a> <a id="742" class="Symbol">→</a> <a id="744" href="Cubical.Categories.Functor.Base.html#397" class="Record">Functor</a> <a id="752" class="Symbol">((</a><a id="754" href="Cubical.Categories.Constructions.TwistedArrow.html#469" class="Function">TwistedArrowCategory</a> <a id="775" href="Cubical.Categories.Constructions.TwistedArrow.html#723" class="Bound">C</a><a id="776" class="Symbol">)</a> <a id="778" href="Cubical.Categories.Category.Base.html#4091" class="Function Operator">^op</a><a id="781" class="Symbol">)</a> <a id="783" href="Cubical.Categories.Constructions.TwistedArrow.html#723" class="Bound">C</a>
-<a id="785" href="Cubical.Categories.Constructions.TwistedArrow.html#709" class="Function">TwistedDom</a> <a id="796" href="Cubical.Categories.Constructions.TwistedArrow.html#796" class="Bound">C</a> <a id="798" class="Symbol">=</a> <a id="800" class="Symbol">((</a><a id="802" href="Cubical.Categories.Constructions.BinProduct.html#958" class="Function">Fst</a> <a id="806" class="Symbol">(</a><a id="807" href="Cubical.Categories.Constructions.TwistedArrow.html#796" class="Bound">C</a> <a id="809" href="Cubical.Categories.Category.Base.html#4091" class="Function Operator">^op</a><a id="812" class="Symbol">)</a> <a id="814" href="Cubical.Categories.Constructions.TwistedArrow.html#796" class="Bound">C</a><a id="815" class="Symbol">)</a> <a id="817" href="Cubical.Categories.Functor.Base.html#4955" class="Function Operator">^opF</a><a id="821" class="Symbol">)</a> <a id="823" href="Cubical.Categories.Functor.Base.html#4428" class="Function">∘F</a> <a id="826" class="Symbol">(</a><a id="827" href="Cubical.Categories.Constructions.Elements.html#2948" class="Function">ForgetElements</a> <a id="842" class="Symbol">(</a><a id="843" href="Cubical.Categories.Functors.HomFunctor.html#418" class="Function">HomFunctor</a> <a id="854" href="Cubical.Categories.Constructions.TwistedArrow.html#796" class="Bound">C</a><a id="855" class="Symbol">)</a> <a id="857" href="Cubical.Categories.Functor.Base.html#4955" class="Function Operator">^opF</a><a id="861" class="Symbol">)</a>
+<a id="785" href="Cubical.Categories.Constructions.TwistedArrow.html#709" class="Function">TwistedDom</a> <a id="796" href="Cubical.Categories.Constructions.TwistedArrow.html#796" class="Bound">C</a> <a id="798" class="Symbol">=</a> <a id="800" class="Symbol">((</a><a id="802" href="Cubical.Categories.Constructions.BinProduct.html#958" class="Function">Fst</a> <a id="806" class="Symbol">(</a><a id="807" href="Cubical.Categories.Constructions.TwistedArrow.html#796" class="Bound">C</a> <a id="809" href="Cubical.Categories.Category.Base.html#4091" class="Function Operator">^op</a><a id="812" class="Symbol">)</a> <a id="814" href="Cubical.Categories.Constructions.TwistedArrow.html#796" class="Bound">C</a><a id="815" class="Symbol">)</a> <a id="817" href="Cubical.Categories.Functor.Base.html#4955" class="Function Operator">^opF</a><a id="821" class="Symbol">)</a> <a id="823" href="Cubical.Categories.Functor.Base.html#4428" class="Function">∘F</a> <a id="826" class="Symbol">(</a><a id="827" href="Cubical.Categories.Constructions.Elements.html#3031" class="Function">ForgetElements</a> <a id="842" class="Symbol">(</a><a id="843" href="Cubical.Categories.Functors.HomFunctor.html#418" class="Function">HomFunctor</a> <a id="854" href="Cubical.Categories.Constructions.TwistedArrow.html#796" class="Bound">C</a><a id="855" class="Symbol">)</a> <a id="857" href="Cubical.Categories.Functor.Base.html#4955" class="Function Operator">^opF</a><a id="861" class="Symbol">)</a>
 
 <a id="TwistedCod"></a><a id="864" href="Cubical.Categories.Constructions.TwistedArrow.html#864" class="Function">TwistedCod</a> <a id="875" class="Symbol">:</a> <a id="877" class="Symbol">(</a><a id="878" href="Cubical.Categories.Constructions.TwistedArrow.html#878" class="Bound">C</a> <a id="880" class="Symbol">:</a> <a id="882" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="891" href="Cubical.Categories.Constructions.TwistedArrow.html#456" class="Generalizable">ℓ</a> <a id="893" href="Cubical.Categories.Constructions.TwistedArrow.html#458" class="Generalizable">ℓ&#39;</a><a id="895" class="Symbol">)</a> <a id="897" class="Symbol">→</a> <a id="899" href="Cubical.Categories.Functor.Base.html#397" class="Record">Functor</a> <a id="907" class="Symbol">(</a><a id="908" href="Cubical.Categories.Constructions.TwistedArrow.html#469" class="Function">TwistedArrowCategory</a> <a id="929" href="Cubical.Categories.Constructions.TwistedArrow.html#878" class="Bound">C</a><a id="930" class="Symbol">)</a> <a id="932" href="Cubical.Categories.Constructions.TwistedArrow.html#878" class="Bound">C</a>
-<a id="934" href="Cubical.Categories.Constructions.TwistedArrow.html#864" class="Function">TwistedCod</a> <a id="945" href="Cubical.Categories.Constructions.TwistedArrow.html#945" class="Bound">C</a> <a id="947" class="Symbol">=</a> <a id="949" class="Symbol">(</a><a id="950" href="Cubical.Categories.Constructions.BinProduct.html#1124" class="Function">Snd</a> <a id="954" class="Symbol">(</a><a id="955" href="Cubical.Categories.Constructions.TwistedArrow.html#945" class="Bound">C</a> <a id="957" href="Cubical.Categories.Category.Base.html#4091" class="Function Operator">^op</a><a id="960" class="Symbol">)</a> <a id="962" href="Cubical.Categories.Constructions.TwistedArrow.html#945" class="Bound">C</a><a id="963" class="Symbol">)</a> <a id="965" href="Cubical.Categories.Functor.Base.html#4428" class="Function">∘F</a> <a id="968" href="Cubical.Categories.Constructions.Elements.html#2948" class="Function">ForgetElements</a> <a id="983" class="Symbol">(</a><a id="984" href="Cubical.Categories.Functors.HomFunctor.html#418" class="Function">HomFunctor</a> <a id="995" href="Cubical.Categories.Constructions.TwistedArrow.html#945" class="Bound">C</a><a id="996" class="Symbol">)</a>
+<a id="934" href="Cubical.Categories.Constructions.TwistedArrow.html#864" class="Function">TwistedCod</a> <a id="945" href="Cubical.Categories.Constructions.TwistedArrow.html#945" class="Bound">C</a> <a id="947" class="Symbol">=</a> <a id="949" class="Symbol">(</a><a id="950" href="Cubical.Categories.Constructions.BinProduct.html#1124" class="Function">Snd</a> <a id="954" class="Symbol">(</a><a id="955" href="Cubical.Categories.Constructions.TwistedArrow.html#945" class="Bound">C</a> <a id="957" href="Cubical.Categories.Category.Base.html#4091" class="Function Operator">^op</a><a id="960" class="Symbol">)</a> <a id="962" href="Cubical.Categories.Constructions.TwistedArrow.html#945" class="Bound">C</a><a id="963" class="Symbol">)</a> <a id="965" href="Cubical.Categories.Functor.Base.html#4428" class="Function">∘F</a> <a id="968" href="Cubical.Categories.Constructions.Elements.html#3031" class="Function">ForgetElements</a> <a id="983" class="Symbol">(</a><a id="984" href="Cubical.Categories.Functors.HomFunctor.html#418" class="Function">HomFunctor</a> <a id="995" href="Cubical.Categories.Constructions.TwistedArrow.html#945" class="Bound">C</a><a id="996" class="Symbol">)</a>
 </pre></body></html>