Skip to content

Commit

Permalink
Deploying to gh-pages from @ e5fef74 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@JacquesCarette
JacquesCarette committed Dec 30, 2023
1 parent 188a961 commit 4a5c79d
Show file tree
Hide file tree
Showing 13 changed files with 1,210 additions and 1,171 deletions.
8 changes: 4 additions & 4 deletions Categories.Adjoint.AFT.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@
<a id="1872" class="Keyword">private</a>
<a id="1886" class="Keyword">module</a> <a id="1893" href="Categories.Adjoint.AFT.html#1893" class="Module">_</a> <a id="1895" href="Categories.Adjoint.AFT.html#1895" class="Bound">X</a> <a id="1897" class="Keyword">where</a>
<a id="1911" href="Categories.Adjoint.AFT.html#1911" class="Function">X↙R</a> <a id="1915" class="Symbol">:</a> <a id="1917" href="Categories.Category.Core.html#442" class="Record">Category</a> <a id="1926" class="Symbol">(</a><a id="1927" href="Categories.Category.Core.html#2226" class="Function">C.o-level</a> <a id="1937" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1939" href="Categories.Category.Core.html#2259" class="Function">D.ℓ-level</a><a id="1948" class="Symbol">)</a> <a id="1950" class="Symbol">(</a><a id="1951" href="Categories.Category.Core.html#2259" class="Function">C.ℓ-level</a> <a id="1961" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1963" href="Categories.Category.Core.html#2292" class="Function">D.e-level</a><a id="1972" class="Symbol">)</a> <a id="1974" href="Categories.Category.Core.html#2292" class="Function">C.e-level</a>
<a id="1992" href="Categories.Adjoint.AFT.html#1911" class="Function">X↙R</a> <a id="1996" class="Symbol">=</a> <a id="1998" href="Categories.Adjoint.AFT.html#1895" class="Bound">X</a> <a id="2000" href="Categories.Category.Construction.Comma.html#4286" class="Function Operator">↙</a> <a id="2002" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a>
<a id="1992" href="Categories.Adjoint.AFT.html#1911" class="Function">X↙R</a> <a id="1996" class="Symbol">=</a> <a id="1998" href="Categories.Adjoint.AFT.html#1895" class="Bound">X</a> <a id="2000" href="Categories.Category.Construction.Comma.html#4320" class="Function Operator">↙</a> <a id="2002" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a>
<a id="2012" class="Keyword">module</a> <a id="2019" href="Categories.Adjoint.AFT.html#2019" class="Module">X↙R</a> <a id="2023" class="Symbol">=</a> <a id="2025" href="Categories.Category.Core.html#442" class="Module">Category</a> <a id="2034" href="Categories.Adjoint.AFT.html#1911" class="Function">X↙R</a>

<a id="2047" href="Categories.Adjoint.AFT.html#2047" class="Function">s′</a> <a id="2050" class="Symbol">:</a> <a id="2052" href="Categories.Category.Complete.Properties.SolutionSet.html#738" class="Record">SolutionSet</a> <a id="2064" href="Categories.Adjoint.AFT.html#1911" class="Function">X↙R</a>
Expand All @@ -99,7 +99,7 @@
<a id="2717" class="Keyword">module</a> <a id="2724" href="Categories.Adjoint.AFT.html#2724" class="Module">F</a> <a id="2726" class="Symbol">=</a> <a id="2728" href="Categories.Functor.Core.html#248" class="Module">Functor</a> <a id="2736" href="Categories.Adjoint.AFT.html#2650" class="Bound">F</a>

<a id="2749" href="Categories.Adjoint.AFT.html#2749" class="Function">F′</a> <a id="2752" class="Symbol">:</a> <a id="2754" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="2762" href="Categories.Adjoint.AFT.html#2611" class="Bound">J</a> <a id="2764" href="Categories.Adjoint.AFT.html#941" class="Bound">C</a>
<a id="2776" href="Categories.Adjoint.AFT.html#2749" class="Function">F′</a> <a id="2779" class="Symbol">=</a> <a id="2781" href="Categories.Category.Construction.Comma.html#3914" class="Function">Cod</a> <a id="2785" class="Symbol">_</a> <a id="2787" class="Symbol">_</a> <a id="2789" href="Categories.Functor.html#747" class="Function Operator">∘F</a> <a id="2792" href="Categories.Adjoint.AFT.html#2650" class="Bound">F</a>
<a id="2776" href="Categories.Adjoint.AFT.html#2749" class="Function">F′</a> <a id="2779" class="Symbol">=</a> <a id="2781" href="Categories.Category.Construction.Comma.html#3948" class="Function">Cod</a> <a id="2785" class="Symbol">_</a> <a id="2787" class="Symbol">_</a> <a id="2789" href="Categories.Functor.html#747" class="Function Operator">∘F</a> <a id="2792" href="Categories.Adjoint.AFT.html#2650" class="Bound">F</a>

<a id="2805" href="Categories.Adjoint.AFT.html#2805" class="Function">LimF′</a> <a id="2811" class="Symbol">:</a> <a id="2813" href="Categories.Diagram.Limit.html#934" class="Record">Limit</a> <a id="2819" href="Categories.Adjoint.AFT.html#2749" class="Function">F′</a>
<a id="2832" href="Categories.Adjoint.AFT.html#2805" class="Function">LimF′</a> <a id="2838" class="Symbol">=</a> <a id="2840" href="Categories.Adjoint.AFT.html#1649" class="Bound">Com</a> <a id="2844" href="Categories.Adjoint.AFT.html#2749" class="Function">F′</a>
Expand Down Expand Up @@ -149,7 +149,7 @@
<a id="4198" class="Symbol">}</a>

<a id="4211" href="Categories.Adjoint.AFT.html#4211" class="Function">K-conv</a> <a id="4218" class="Symbol">:</a> <a id="4220" href="Categories.Diagram.Cone.html#526" class="Record">Cone</a> <a id="4225" href="Categories.Adjoint.AFT.html#2650" class="Bound">F</a> <a id="4227" class="Symbol">→</a> <a id="4229" href="Categories.Diagram.Cone.html#526" class="Record">Cone</a> <a id="4234" href="Categories.Adjoint.AFT.html#2749" class="Function">F′</a>
<a id="4247" href="Categories.Adjoint.AFT.html#4211" class="Function">K-conv</a> <a id="4254" class="Symbol">=</a> <a id="4256" href="Categories.Diagram.Cone.Properties.html#633" class="Function">F-map-Coneˡ</a> <a id="4268" class="Symbol">(</a><a id="4269" href="Categories.Category.Construction.Comma.html#3914" class="Function">Cod</a> <a id="4273" class="Symbol">_</a> <a id="4275" class="Symbol">_)</a>
<a id="4247" href="Categories.Adjoint.AFT.html#4211" class="Function">K-conv</a> <a id="4254" class="Symbol">=</a> <a id="4256" href="Categories.Diagram.Cone.Properties.html#633" class="Function">F-map-Coneˡ</a> <a id="4268" class="Symbol">(</a><a id="4269" href="Categories.Category.Construction.Comma.html#3948" class="Function">Cod</a> <a id="4273" class="Symbol">_</a> <a id="4275" class="Symbol">_)</a>

<a id="4289" href="Categories.Adjoint.AFT.html#4289" class="Function">K-conv′</a> <a id="4297" class="Symbol">:</a> <a id="4299" href="Categories.Diagram.Cone.html#526" class="Record">Cone</a> <a id="4304" href="Categories.Adjoint.AFT.html#2650" class="Bound">F</a> <a id="4306" class="Symbol">→</a> <a id="4308" href="Categories.Diagram.Cone.html#526" class="Record">Cone</a> <a id="4313" class="Symbol">(</a><a id="4314" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a> <a id="4316" href="Categories.Functor.html#747" class="Function Operator">∘F</a> <a id="4319" href="Categories.Adjoint.AFT.html#2749" class="Function">F′</a><a id="4321" class="Symbol">)</a>
<a id="4333" href="Categories.Adjoint.AFT.html#4289" class="Function">K-conv′</a> <a id="4341" href="Categories.Adjoint.AFT.html#4341" class="Bound">K</a> <a id="4343" class="Symbol">=</a> <a id="4345" href="Categories.Diagram.Cone.Properties.html#633" class="Function">F-map-Coneˡ</a> <a id="4357" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a> <a id="4359" class="Symbol">(</a><a id="4360" href="Categories.Adjoint.AFT.html#4211" class="Function">K-conv</a> <a id="4367" href="Categories.Adjoint.AFT.html#4341" class="Bound">K</a><a id="4368" class="Symbol">)</a>
Expand Down Expand Up @@ -195,7 +195,7 @@

<a id="5780" href="Categories.Adjoint.AFT.html#5780" class="Function">solutionSet′⇒universalMorphism</a> <a id="5811" class="Symbol">:</a> <a id="5813" href="Categories.Morphism.Universal.html#259" class="Record">UniversalMorphism</a> <a id="5831" href="Categories.Adjoint.AFT.html#1895" class="Bound">X</a> <a id="5833" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a>
<a id="5843" href="Categories.Adjoint.AFT.html#5780" class="Function">solutionSet′⇒universalMorphism</a> <a id="5874" class="Symbol">=</a> <a id="5876" class="Keyword">record</a>
<a id="5893" class="Symbol">{</a> <a id="5895" href="Categories.Morphism.Universal.html#532" class="Field">initial</a> <a id="5903" class="Symbol">=</a> <a id="5905" href="Categories.Category.Complete.Properties.SolutionSet.html#3082" class="Function">SolutionSet⇒Initial</a> <a id="5925" class="Symbol">{</a><a id="5926" class="Argument">o′</a> <a id="5929" class="Symbol">=</a> <a id="5931" href="Level.html#521" class="Function">0ℓ</a><a id="5933" class="Symbol">}</a> <a id="5935" class="Symbol">{</a><a id="5936" href="Level.html#521" class="Function">0ℓ</a><a id="5938" class="Symbol">}</a> <a id="5940" class="Symbol">{</a><a id="5941" href="Level.html#521" class="Function">0ℓ</a><a id="5943" class="Symbol">}</a> <a id="5945" class="Symbol">{</a><a id="5946" class="Argument">C</a> <a id="5948" class="Symbol">=</a> <a id="5950" href="Categories.Adjoint.AFT.html#1895" class="Bound">X</a> <a id="5952" href="Categories.Category.Construction.Comma.html#4286" class="Function Operator">↙</a> <a id="5954" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a><a id="5955" class="Symbol">}</a> <a id="5957" href="Categories.Adjoint.AFT.html#5500" class="Function">complete</a> <a id="5966" href="Categories.Adjoint.AFT.html#2047" class="Function">s′</a>
<a id="5893" class="Symbol">{</a> <a id="5895" href="Categories.Morphism.Universal.html#532" class="Field">initial</a> <a id="5903" class="Symbol">=</a> <a id="5905" href="Categories.Category.Complete.Properties.SolutionSet.html#3082" class="Function">SolutionSet⇒Initial</a> <a id="5925" class="Symbol">{</a><a id="5926" class="Argument">o′</a> <a id="5929" class="Symbol">=</a> <a id="5931" href="Level.html#521" class="Function">0ℓ</a><a id="5933" class="Symbol">}</a> <a id="5935" class="Symbol">{</a><a id="5936" href="Level.html#521" class="Function">0ℓ</a><a id="5938" class="Symbol">}</a> <a id="5940" class="Symbol">{</a><a id="5941" href="Level.html#521" class="Function">0ℓ</a><a id="5943" class="Symbol">}</a> <a id="5945" class="Symbol">{</a><a id="5946" class="Argument">C</a> <a id="5948" class="Symbol">=</a> <a id="5950" href="Categories.Adjoint.AFT.html#1895" class="Bound">X</a> <a id="5952" href="Categories.Category.Construction.Comma.html#4320" class="Function Operator">↙</a> <a id="5954" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a><a id="5955" class="Symbol">}</a> <a id="5957" href="Categories.Adjoint.AFT.html#5500" class="Function">complete</a> <a id="5966" href="Categories.Adjoint.AFT.html#2047" class="Function">s′</a>
<a id="5979" class="Symbol">}</a>

<a id="5986" href="Categories.Adjoint.AFT.html#5986" class="Function">solutionSet⇒adjoint</a> <a id="6006" class="Symbol">:</a> <a id="6008" href="Agda.Builtin.Sigma.html#165" class="Record">Σ</a> <a id="6010" class="Symbol">(</a><a id="6011" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="6019" href="Categories.Adjoint.AFT.html#943" class="Bound">D</a> <a id="6021" href="Categories.Adjoint.AFT.html#941" class="Bound">C</a><a id="6022" class="Symbol">)</a> <a id="6024" class="Symbol">(λ</a> <a id="6027" href="Categories.Adjoint.AFT.html#6027" class="Bound">L</a> <a id="6029" class="Symbol">→</a> <a id="6031" href="Categories.Adjoint.AFT.html#6027" class="Bound">L</a> <a id="6033" href="Categories.Adjoint.html#7818" class="Function Operator">⊣</a> <a id="6035" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a><a id="6036" class="Symbol">)</a>
Expand Down
Loading

0 comments on commit 4a5c79d

Please sign in to comment.