Deploying to gh-pages from @ 944a487 🚀

Categories.Category.Construction.LT-Models.html

@@ -11,7 +11,7 @@
 
 <a id="271" class="Keyword">open</a> <a id="276" class="Keyword">import</a> <a id="283" href="Categories.Category.Core.html" class="Module">Categories.Category.Core</a> <a id="308" class="Keyword">using</a> <a id="314" class="Symbol">(</a><a id="315" href="Categories.Category.Core.html#442" class="Record">Category</a><a id="323" class="Symbol">)</a>
 <a id="325" class="Keyword">open</a> <a id="330" class="Keyword">import</a> <a id="337" href="Categories.Category.Cartesian.Bundle.html" class="Module">Categories.Category.Cartesian.Bundle</a> <a id="374" class="Keyword">using</a> <a id="380" class="Symbol">(</a><a id="381" href="Categories.Category.Cartesian.Bundle.html#422" class="Record">CartesianCategory</a><a id="398" class="Symbol">)</a>
-<a id="400" class="Keyword">open</a> <a id="405" class="Keyword">import</a> <a id="412" href="Categories.Category.Monoidal.Instance.Setoids.html" class="Module">Categories.Category.Monoidal.Instance.Setoids</a> <a id="458" class="Keyword">using</a> <a id="464" class="Symbol">(</a><a id="465" href="Categories.Category.Monoidal.Instance.Setoids.html#2839" class="Function">Setoids-CartesianCategory</a><a id="490" class="Symbol">)</a>
+<a id="400" class="Keyword">open</a> <a id="405" class="Keyword">import</a> <a id="412" href="Categories.Category.Monoidal.Instance.Setoids.html" class="Module">Categories.Category.Monoidal.Instance.Setoids</a> <a id="458" class="Keyword">using</a> <a id="464" class="Symbol">(</a><a id="465" href="Categories.Category.Monoidal.Instance.Setoids.html#2500" class="Function">Setoids-CartesianCategory</a><a id="490" class="Symbol">)</a>
 <a id="492" class="Keyword">open</a> <a id="497" class="Keyword">import</a> <a id="504" href="Categories.NaturalTransformation.html" class="Module">Categories.NaturalTransformation</a>
   <a id="539" class="Keyword">using</a> <a id="545" class="Symbol">(</a><a id="546" href="Categories.NaturalTransformation.Core.html#466" class="Record">NaturalTransformation</a><a id="567" class="Symbol">;</a> <a id="569" href="Categories.NaturalTransformation.Core.html#2439" class="Function Operator">_∘ᵥ_</a><a id="573" class="Symbol">)</a> <a id="575" class="Keyword">renaming</a> <a id="584" class="Symbol">(</a><a id="585" href="Categories.NaturalTransformation.Core.html#2132" class="Function">id</a> <a id="588" class="Symbol">to</a> <a id="591" class="Function">idN</a><a id="594" class="Symbol">)</a>
 <a id="596" class="Keyword">open</a> <a id="601" class="Keyword">import</a> <a id="608" href="Categories.NaturalTransformation.Equivalence.html" class="Module">Categories.NaturalTransformation.Equivalence</a> <a id="653" class="Keyword">using</a> <a id="659" class="Symbol">(</a><a id="660" href="Categories.NaturalTransformation.Equivalence.html#630" class="Function Operator">_≃_</a><a id="663" class="Symbol">;</a> <a id="665" href="Categories.NaturalTransformation.Equivalence.html#785" class="Function">≃-isEquivalence</a><a id="680" class="Symbol">)</a>
@@ -43,5 +43,5 @@
     <a id="1530" class="Keyword">open</a> <a id="1535" href="Categories.Category.Core.html#442" class="Module">Category</a> <a id="1544" href="Categories.Category.Cartesian.Bundle.html#488" class="Field">C.U</a>
 
 <a id="LT-SetoidsModels"></a><a id="1549" href="Categories.Category.Construction.LT-Models.html#1549" class="Function">LT-SetoidsModels</a> <a id="1566" class="Symbol">:</a> <a id="1568" class="Symbol">{</a><a id="1569" href="Categories.Category.Construction.LT-Models.html#1569" class="Bound">ℓ′</a> <a id="1572" href="Categories.Category.Construction.LT-Models.html#1572" class="Bound">e′</a> <a id="1575" class="Symbol">:</a> <a id="1577" href="Agda.Primitive.html#742" class="Postulate">Level</a><a id="1582" class="Symbol">}</a> <a id="1584" class="Symbol">→</a> <a id="1586" href="Categories.Theory.Lawvere.html#1221" class="Record">LawvereTheory</a> <a id="1600" href="Categories.Category.Construction.LT-Models.html#782" class="Generalizable">ℓ</a> <a id="1602" href="Categories.Category.Construction.LT-Models.html#784" class="Generalizable">e</a> <a id="1604" class="Symbol">→</a> <a id="1606" href="Categories.Category.Core.html#442" class="Record">Category</a> <a id="1615" class="Symbol">(</a><a id="1616" href="Categories.Category.Construction.LT-Models.html#782" class="Generalizable">ℓ</a> <a id="1618" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1620" href="Categories.Category.Construction.LT-Models.html#784" class="Generalizable">e</a> <a id="1622" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1624" href="Agda.Primitive.html#931" class="Primitive">suc</a> <a id="1628" class="Symbol">(</a><a id="1629" href="Categories.Category.Construction.LT-Models.html#1569" class="Bound">ℓ′</a> <a id="1632" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1634" href="Categories.Category.Construction.LT-Models.html#1572" class="Bound">e′</a><a id="1636" class="Symbol">))</a> <a id="1639" class="Symbol">(</a><a id="1640" href="Categories.Category.Construction.LT-Models.html#782" class="Generalizable">ℓ</a> <a id="1642" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1644" href="Categories.Category.Construction.LT-Models.html#1569" class="Bound">ℓ′</a> <a id="1647" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1649" href="Categories.Category.Construction.LT-Models.html#1572" class="Bound">e′</a><a id="1651" class="Symbol">)</a> <a id="1653" class="Symbol">(</a><a id="1654" href="Categories.Category.Construction.LT-Models.html#1569" class="Bound">ℓ′</a> <a id="1657" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1659" href="Categories.Category.Construction.LT-Models.html#1572" class="Bound">e′</a><a id="1661" class="Symbol">)</a>
-<a id="1663" href="Categories.Category.Construction.LT-Models.html#1549" class="Function">LT-SetoidsModels</a> <a id="1680" class="Symbol">{</a><a id="1681" class="Argument">ℓ′</a> <a id="1684" class="Symbol">=</a> <a id="1686" href="Categories.Category.Construction.LT-Models.html#1686" class="Bound">ℓ′</a><a id="1688" class="Symbol">}</a> <a id="1690" class="Symbol">{</a><a id="1691" href="Categories.Category.Construction.LT-Models.html#1691" class="Bound">e′</a><a id="1693" class="Symbol">}</a> <a id="1695" href="Categories.Category.Construction.LT-Models.html#1695" class="Bound">LT</a> <a id="1698" class="Symbol">=</a> <a id="1700" href="Categories.Category.Construction.LT-Models.html#948" class="Function">LT-Models</a> <a id="1710" href="Categories.Category.Construction.LT-Models.html#1695" class="Bound">LT</a> <a id="1713" class="Symbol">(</a><a id="1714" href="Categories.Category.Monoidal.Instance.Setoids.html#2839" class="Function">Setoids-CartesianCategory</a> <a id="1740" href="Categories.Category.Construction.LT-Models.html#1686" class="Bound">ℓ′</a> <a id="1743" href="Categories.Category.Construction.LT-Models.html#1691" class="Bound">e′</a><a id="1745" class="Symbol">)</a>
+<a id="1663" href="Categories.Category.Construction.LT-Models.html#1549" class="Function">LT-SetoidsModels</a> <a id="1680" class="Symbol">{</a><a id="1681" class="Argument">ℓ′</a> <a id="1684" class="Symbol">=</a> <a id="1686" href="Categories.Category.Construction.LT-Models.html#1686" class="Bound">ℓ′</a><a id="1688" class="Symbol">}</a> <a id="1690" class="Symbol">{</a><a id="1691" href="Categories.Category.Construction.LT-Models.html#1691" class="Bound">e′</a><a id="1693" class="Symbol">}</a> <a id="1695" href="Categories.Category.Construction.LT-Models.html#1695" class="Bound">LT</a> <a id="1698" class="Symbol">=</a> <a id="1700" href="Categories.Category.Construction.LT-Models.html#948" class="Function">LT-Models</a> <a id="1710" href="Categories.Category.Construction.LT-Models.html#1695" class="Bound">LT</a> <a id="1713" class="Symbol">(</a><a id="1714" href="Categories.Category.Monoidal.Instance.Setoids.html#2500" class="Function">Setoids-CartesianCategory</a> <a id="1740" href="Categories.Category.Construction.LT-Models.html#1686" class="Bound">ℓ′</a> <a id="1743" href="Categories.Category.Construction.LT-Models.html#1691" class="Bound">e′</a><a id="1745" class="Symbol">)</a>
 </pre></body></html>

Categories.Category.Instance.Properties.Setoids.CCC.html

@@ -13,7 +13,7 @@
 <a id="362" class="Keyword">open</a> <a id="367" class="Keyword">import</a> <a id="374" href="Categories.Category.BinaryProducts.html" class="Module">Categories.Category.BinaryProducts</a> <a id="409" class="Keyword">using</a> <a id="415" class="Symbol">(</a><a id="416" href="Categories.Category.BinaryProducts.html#848" class="Record">BinaryProducts</a><a id="430" class="Symbol">)</a>
 <a id="432" class="Keyword">open</a> <a id="437" class="Keyword">import</a> <a id="444" href="Categories.Category.CartesianClosed.html" class="Module">Categories.Category.CartesianClosed</a> <a id="480" class="Keyword">using</a> <a id="486" class="Symbol">(</a><a id="487" href="Categories.Category.CartesianClosed.html#1233" class="Record">CartesianClosed</a><a id="502" class="Symbol">)</a>
 <a id="504" class="Keyword">open</a> <a id="509" class="Keyword">import</a> <a id="516" href="Categories.Category.CartesianClosed.Canonical.html" class="Module">Categories.Category.CartesianClosed.Canonical</a> <a id="562" class="Keyword">renaming</a> <a id="571" class="Symbol">(</a><a id="572" href="Categories.Category.CartesianClosed.Canonical.html#1539" class="Record">CartesianClosed</a> <a id="588" class="Symbol">to</a> <a id="591" class="Record">CCartesianClosed</a><a id="607" class="Symbol">)</a>
-<a id="609" class="Keyword">open</a> <a id="614" class="Keyword">import</a> <a id="621" href="Categories.Category.Monoidal.Instance.Setoids.html" class="Module">Categories.Category.Monoidal.Instance.Setoids</a> <a id="667" class="Keyword">using</a> <a id="673" class="Symbol">(</a><a id="674" href="Categories.Category.Monoidal.Instance.Setoids.html#1080" class="Function">Setoids-Cartesian</a><a id="691" class="Symbol">)</a>
+<a id="609" class="Keyword">open</a> <a id="614" class="Keyword">import</a> <a id="621" href="Categories.Category.Monoidal.Instance.Setoids.html" class="Module">Categories.Category.Monoidal.Instance.Setoids</a> <a id="667" class="Keyword">using</a> <a id="673" class="Symbol">(</a><a id="674" href="Categories.Category.Monoidal.Instance.Setoids.html#1204" class="Function">Setoids-Cartesian</a><a id="691" class="Symbol">)</a>
 <a id="693" class="Keyword">open</a> <a id="698" class="Keyword">import</a> <a id="705" href="Categories.Category.Instance.Setoids.html" class="Module">Categories.Category.Instance.Setoids</a> <a id="742" class="Keyword">using</a> <a id="748" class="Symbol">(</a><a id="749" href="Categories.Category.Instance.Setoids.html#555" class="Function">Setoids</a><a id="756" class="Symbol">)</a>
 <a id="758" class="Keyword">open</a> <a id="763" class="Keyword">import</a> <a id="770" href="Categories.Object.Terminal.html" class="Module">Categories.Object.Terminal</a> <a id="797" class="Keyword">using</a> <a id="803" class="Symbol">(</a><a id="804" href="Categories.Object.Terminal.html#860" class="Record">Terminal</a><a id="812" class="Symbol">)</a>
 
@@ -52,7 +52,7 @@
     <a id="1900" class="Symbol">;</a> <a id="1902" href="Categories.Category.CartesianClosed.Canonical.html#2734" class="Field">curry-unique</a> <a id="1915" class="Symbol">=</a> <a id="1917" class="Symbol">λ</a> <a id="1919" href="Categories.Category.Instance.Properties.Setoids.CCC.html#1919" class="Bound">eq</a> <a id="1922" class="Symbol">→</a> <a id="1924" href="Categories.Category.Instance.Properties.Setoids.CCC.html#1919" class="Bound">eq</a>
     <a id="1931" class="Symbol">}</a>
     <a id="1937" class="Keyword">where</a>
-      <a id="1949" class="Keyword">open</a> <a id="1954" href="Categories.Category.Monoidal.Instance.Setoids.html#1895" class="Module">Setoids-Cartesian</a>
+      <a id="1949" class="Keyword">open</a> <a id="1954" href="Categories.Category.Monoidal.Instance.Setoids.html#1732" class="Module">Setoids-Cartesian</a>
       <a id="1978" class="Keyword">open</a> <a id="1983" href="Categories.Category.BinaryProducts.html#848" class="Module">BinaryProducts</a> <a id="1998" href="Categories.Category.Cartesian.html#801" class="Function">products</a> <a id="2007" class="Keyword">using</a> <a id="2013" class="Symbol">(</a><a id="2014" href="Categories.Category.BinaryProducts.html#1053" class="Function Operator">_×_</a><a id="2017" class="Symbol">;</a> <a id="2019" href="Categories.Object.Product.Core.html#526" class="Function">π₁</a><a id="2021" class="Symbol">;</a> <a id="2023" href="Categories.Object.Product.Core.html#546" class="Function">π₂</a><a id="2025" class="Symbol">;</a> <a id="2027" href="Categories.Category.BinaryProducts.html#1396" class="Function Operator">⟨_,_⟩</a><a id="2032" class="Symbol">;</a> <a id="2034" href="Categories.Object.Product.Core.html#603" class="Function">project₁</a><a id="2042" class="Symbol">;</a> <a id="2044" href="Categories.Object.Product.Core.html#637" class="Function">project₂</a><a id="2052" class="Symbol">;</a> <a id="2054" href="Categories.Object.Product.Core.html#671" class="Function">unique</a><a id="2060" class="Symbol">)</a>
       <a id="2068" class="Keyword">open</a> <a id="2073" href="Categories.Object.Terminal.html#860" class="Module">Terminal</a> <a id="2082" href="Categories.Category.Cartesian.html#777" class="Function">terminal</a> <a id="2091" class="Keyword">using</a> <a id="2097" class="Symbol">(</a><a id="2098" href="Categories.Object.Terminal.html#905" class="Field">⊤</a><a id="2099" class="Symbol">;</a> <a id="2101" href="Categories.Object.Terminal.html#577" class="Function">!</a><a id="2102" class="Symbol">;</a> <a id="2104" href="Categories.Object.Terminal.html#605" class="Function">!-unique</a><a id="2112" class="Symbol">)</a>