Deploying to gh-pages from @ dddf364 🚀

Author: JacquesCarette

Categories.Adjoint.Instance.BaseChange.html

@@ -8,7 +8,7 @@
 <a id="169" class="Keyword">open</a> <a id="174" class="Keyword">import</a> <a id="181" href="Categories.Adjoint.html" class="Module">Categories.Adjoint</a> <a id="200" class="Keyword">using</a> <a id="206" class="Symbol">(</a><a id="207" href="Categories.Adjoint.html#7818" class="Function Operator">_⊣_</a><a id="210" class="Symbol">)</a>
 <a id="212" class="Keyword">open</a> <a id="217" class="Keyword">import</a> <a id="224" href="Categories.Adjoint.Compose.html" class="Module">Categories.Adjoint.Compose</a> <a id="251" class="Keyword">using</a> <a id="257" class="Symbol">(</a><a id="258" href="Categories.Adjoint.Compose.html#1395" class="Function Operator">_∘⊣_</a><a id="262" class="Symbol">)</a>
 <a id="264" class="Keyword">open</a> <a id="269" class="Keyword">import</a> <a id="276" href="Categories.Adjoint.Instance.Slice.html" class="Module">Categories.Adjoint.Instance.Slice</a> <a id="310" class="Keyword">using</a> <a id="316" class="Symbol">(</a><a id="317" href="Categories.Adjoint.Instance.Slice.html#656" class="Function">TotalSpace⊣ConstantFamily</a><a id="342" class="Symbol">)</a>
-<a id="344" class="Keyword">open</a> <a id="349" class="Keyword">import</a> <a id="356" href="Categories.Category.Slice.html" class="Module">Categories.Category.Slice</a> <a id="382" href="Categories.Adjoint.Instance.BaseChange.html#142" class="Bound">C</a> <a id="384" class="Keyword">using</a> <a id="390" class="Symbol">(</a><a id="391" href="Categories.Category.Slice.html#811" class="Function">Slice</a><a id="396" class="Symbol">)</a>
+<a id="344" class="Keyword">open</a> <a id="349" class="Keyword">import</a> <a id="356" href="Categories.Category.Slice.html" class="Module">Categories.Category.Slice</a> <a id="382" href="Categories.Adjoint.Instance.BaseChange.html#142" class="Bound">C</a> <a id="384" class="Keyword">using</a> <a id="390" class="Symbol">(</a><a id="391" href="Categories.Category.Slice.html#773" class="Function">Slice</a><a id="396" class="Symbol">)</a>
 <a id="398" class="Keyword">open</a> <a id="403" class="Keyword">import</a> <a id="410" href="Categories.Category.Slice.Properties.html" class="Module">Categories.Category.Slice.Properties</a> <a id="447" href="Categories.Adjoint.Instance.BaseChange.html#142" class="Bound">C</a> <a id="449" class="Keyword">using</a> <a id="455" class="Symbol">(</a><a id="456" href="Categories.Category.Slice.Properties.html#1840" class="Function">pullback⇒product</a><a id="472" class="Symbol">;</a> <a id="474" href="Categories.Category.Slice.Properties.html#3959" class="Function">slice-slice≃slice</a><a id="491" class="Symbol">)</a>
 <a id="493" class="Keyword">open</a> <a id="498" class="Keyword">import</a> <a id="505" href="Categories.Category.Equivalence.Properties.html" class="Module">Categories.Category.Equivalence.Properties</a> <a id="548" class="Keyword">using</a> <a id="554" class="Symbol">(</a><a id="555" class="Keyword">module</a> <a id="562" href="Categories.Category.Equivalence.Properties.html#5332" class="Module">C≅D</a><a id="565" class="Symbol">)</a>
 <a id="567" class="Keyword">open</a> <a id="572" class="Keyword">import</a> <a id="579" href="Categories.Diagram.Pullback.html" class="Module">Categories.Diagram.Pullback</a> <a id="607" href="Categories.Adjoint.Instance.BaseChange.html#142" class="Bound">C</a> <a id="609" class="Keyword">using</a> <a id="615" class="Symbol">(</a><a id="616" href="Categories.Diagram.Pullback.html#1945" class="Record">Pullback</a><a id="624" class="Symbol">)</a>
@@ -19,5 +19,5 @@
 <a id="727" class="Keyword">module</a> <a id="734" href="Categories.Adjoint.Instance.BaseChange.html#734" class="Module">_</a> <a id="736" class="Symbol">{</a><a id="737" href="Categories.Adjoint.Instance.BaseChange.html#737" class="Bound">A</a> <a id="739" href="Categories.Adjoint.Instance.BaseChange.html#739" class="Bound">B</a> <a id="741" class="Symbol">:</a> <a id="743" href="Categories.Category.Core.html#559" class="Field">Obj</a><a id="746" class="Symbol">}</a> <a id="748" class="Symbol">(</a><a id="749" href="Categories.Adjoint.Instance.BaseChange.html#749" class="Bound">f</a> <a id="751" class="Symbol">:</a> <a id="753" href="Categories.Adjoint.Instance.BaseChange.html#739" class="Bound">B</a> <a id="755" href="Categories.Category.Core.html#575" class="Field Operator">⇒</a> <a id="757" href="Categories.Adjoint.Instance.BaseChange.html#737" class="Bound">A</a><a id="758" class="Symbol">)</a> <a id="760" class="Symbol">(</a><a id="761" href="Categories.Adjoint.Instance.BaseChange.html#761" class="Bound">pullback</a> <a id="770" class="Symbol">:</a> <a id="772" class="Symbol">∀</a> <a id="774" class="Symbol">{</a><a id="775" href="Categories.Adjoint.Instance.BaseChange.html#775" class="Bound">C</a><a id="776" class="Symbol">}</a> <a id="778" class="Symbol">{</a><a id="779" href="Categories.Adjoint.Instance.BaseChange.html#779" class="Bound">h</a> <a id="781" class="Symbol">:</a> <a id="783" href="Categories.Adjoint.Instance.BaseChange.html#775" class="Bound">C</a> <a id="785" href="Categories.Category.Core.html#575" class="Field Operator">⇒</a> <a id="787" href="Categories.Adjoint.Instance.BaseChange.html#737" class="Bound">A</a><a id="788" class="Symbol">}</a> <a id="790" class="Symbol">→</a> <a id="792" href="Categories.Diagram.Pullback.html#1945" class="Record">Pullback</a> <a id="801" href="Categories.Adjoint.Instance.BaseChange.html#749" class="Bound">f</a> <a id="803" href="Categories.Adjoint.Instance.BaseChange.html#779" class="Bound">h</a><a id="804" class="Symbol">)</a> <a id="806" class="Keyword">where</a>
 
   <a id="815" href="Categories.Adjoint.Instance.BaseChange.html#815" class="Function">!⊣*</a> <a id="819" class="Symbol">:</a> <a id="821" href="Categories.Functor.Slice.BaseChange.html#630" class="Function">BaseChange!</a> <a id="833" href="Categories.Adjoint.Instance.BaseChange.html#749" class="Bound">f</a> <a id="835" href="Categories.Adjoint.html#7818" class="Function Operator">⊣</a> <a id="837" href="Categories.Functor.Slice.BaseChange.html#905" class="Function">BaseChange*</a> <a id="849" href="Categories.Adjoint.Instance.BaseChange.html#749" class="Bound">f</a> <a id="851" href="Categories.Adjoint.Instance.BaseChange.html#761" class="Bound">pullback</a>
-  <a id="862" href="Categories.Adjoint.Instance.BaseChange.html#815" class="Function">!⊣*</a> <a id="866" class="Symbol">=</a> <a id="868" href="Categories.Adjoint.TwoSided.html#2636" class="Function">C≅D.L⊣R</a> <a id="876" class="Symbol">(</a><a id="877" href="Categories.Category.Slice.Properties.html#3959" class="Function">slice-slice≃slice</a> <a id="895" href="Categories.Adjoint.Instance.BaseChange.html#749" class="Bound">f</a><a id="896" class="Symbol">)</a> <a id="898" href="Categories.Adjoint.Compose.html#1395" class="Function Operator">∘⊣</a> <a id="901" href="Categories.Adjoint.Instance.Slice.html#656" class="Function">TotalSpace⊣ConstantFamily</a> <a id="927" class="Symbol">(</a><a id="928" href="Categories.Category.Slice.html#811" class="Function">Slice</a> <a id="934" href="Categories.Adjoint.Instance.BaseChange.html#737" class="Bound">A</a><a id="935" class="Symbol">)</a> <a id="937" class="Symbol">(</a><a id="938" href="Categories.Category.Slice.Properties.html#1840" class="Function">pullback⇒product</a> <a id="955" href="Categories.Adjoint.Instance.BaseChange.html#761" class="Bound">pullback</a><a id="963" class="Symbol">)</a>
+  <a id="862" href="Categories.Adjoint.Instance.BaseChange.html#815" class="Function">!⊣*</a> <a id="866" class="Symbol">=</a> <a id="868" href="Categories.Adjoint.TwoSided.html#2636" class="Function">C≅D.L⊣R</a> <a id="876" class="Symbol">(</a><a id="877" href="Categories.Category.Slice.Properties.html#3959" class="Function">slice-slice≃slice</a> <a id="895" href="Categories.Adjoint.Instance.BaseChange.html#749" class="Bound">f</a><a id="896" class="Symbol">)</a> <a id="898" href="Categories.Adjoint.Compose.html#1395" class="Function Operator">∘⊣</a> <a id="901" href="Categories.Adjoint.Instance.Slice.html#656" class="Function">TotalSpace⊣ConstantFamily</a> <a id="927" class="Symbol">(</a><a id="928" href="Categories.Category.Slice.html#773" class="Function">Slice</a> <a id="934" href="Categories.Adjoint.Instance.BaseChange.html#737" class="Bound">A</a><a id="935" class="Symbol">)</a> <a id="937" class="Symbol">(</a><a id="938" href="Categories.Category.Slice.Properties.html#1840" class="Function">pullback⇒product</a> <a id="955" href="Categories.Adjoint.Instance.BaseChange.html#761" class="Bound">pullback</a><a id="963" class="Symbol">)</a>
 </pre></body></html>