Deploying to gh-pages from @ 8180116 🚀

Author: JacquesCarette

Agda.Builtin.Reflection.html

@@ -19,6 +19,7 @@
 .Agda .Datatype               { color: #0000CD }
 .Agda .Field                  { color: #EE1289 }
 .Agda .Function               { color: #0000CD }
+.Agda .Macro                  { color: #0000CD }
 .Agda .Module                 { color: #A020F0 }
 .Agda .Postulate              { color: #0000CD }
 .Agda .Primitive              { color: #0000CD }

Agda.css

@@ -23,7 +23,7 @@
 
 <a id="829" class="Keyword">open</a> <a id="834" class="Keyword">import</a> <a id="841" href="Algebra.Core.html" class="Module">Algebra.Core</a>
 <a id="854" class="Keyword">open</a> <a id="859" class="Keyword">import</a> <a id="866" href="Algebra.Definitions.html" class="Module">Algebra.Definitions</a> <a id="886" class="Symbol">{</a><a id="887" class="Argument">A</a> <a id="889" class="Symbol">=</a> <a id="891" href="Algebra.Consequences.Propositional.html#403" class="Bound">A</a><a id="892" class="Symbol">}</a> <a id="894" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">_≡_</a>
-<a id="898" class="Keyword">import</a> <a id="905" href="Algebra.Consequences.Setoid.html" class="Module">Algebra.Consequences.Setoid</a> <a id="933" class="Symbol">(</a><a id="934" href="Relation.Binary.PropositionalEquality.Properties.html#5687" class="Function">setoid</a> <a id="941" href="Algebra.Consequences.Propositional.html#403" class="Bound">A</a><a id="942" class="Symbol">)</a> as <a id="Base"></a><a id="947" href="Algebra.Consequences.Propositional.html#947" class="Module">Base</a>
+<a id="898" class="Keyword">import</a> <a id="905" href="Algebra.Consequences.Setoid.html" class="Module">Algebra.Consequences.Setoid</a> <a id="933" class="Symbol">(</a><a id="934" href="Relation.Binary.PropositionalEquality.Properties.html#5687" class="Function">setoid</a> <a id="941" href="Algebra.Consequences.Propositional.html#403" class="Bound">A</a><a id="942" class="Symbol">)</a> <a id="944" class="Symbol">as</a> <a id="Base"></a><a id="947" href="Algebra.Consequences.Propositional.html#947" class="Module">Base</a>
 
 <a id="953" class="Comment">------------------------------------------------------------------------</a>
 <a id="1026" class="Comment">-- Re-export all proofs that don&#39;t require congruence or substitutivity</a>

Algebra.Consequences.Propositional.html

@@ -19,7 +19,7 @@
 
 <a id="597" class="Keyword">open</a> <a id="602" class="Keyword">import</a> <a id="609" href="Relation.Binary.Reasoning.Setoid.html" class="Module">Relation.Binary.Reasoning.Setoid</a> <a id="642" href="Algebra.Structures.html#1873" class="Function">setoid</a>
 <a id="649" class="Keyword">import</a> <a id="656" href="Relation.Binary.Construct.NaturalOrder.Left.html" class="Module">Relation.Binary.Construct.NaturalOrder.Left</a> <a id="700" href="Algebra.Lattice.Bundles.html#1333" class="Field Operator">_≈_</a> <a id="704" href="Algebra.Lattice.Properties.Semilattice.html#591" class="Field Operator">_∧_</a>
-  as <a id="LeftNaturalOrder"></a><a id="713" href="Algebra.Lattice.Properties.Semilattice.html#713" class="Module">LeftNaturalOrder</a>
+  <a id="710" class="Symbol">as</a> <a id="LeftNaturalOrder"></a><a id="713" href="Algebra.Lattice.Properties.Semilattice.html#713" class="Module">LeftNaturalOrder</a>
 
 <a id="731" class="Comment">------------------------------------------------------------------------</a>
 <a id="804" class="Comment">-- Every semilattice can be turned into a poset via the left natural</a>

Algebra.Lattice.Properties.Semilattice.html

@@ -19,7 +19,7 @@
 <a id="619" class="Keyword">open</a> <a id="624" class="Keyword">import</a> <a id="631" href="Categories.Enriched.Category.Underlying.html" class="Module">Categories.Enriched.Category.Underlying</a> <a id="671" href="Categories.Bicategory.Instance.EnrichedCats.html#284" class="Bound">M</a>
 <a id="673" class="Keyword">open</a> <a id="678" class="Keyword">import</a> <a id="685" href="Categories.Enriched.Functor.html" class="Module">Categories.Enriched.Functor</a> <a id="713" href="Categories.Bicategory.Instance.EnrichedCats.html#284" class="Bound">M</a> <a id="715" class="Keyword">renaming</a> <a id="724" class="Symbol">(</a><a id="725" href="Categories.Enriched.Functor.html#1794" class="Function">id</a> <a id="728" class="Symbol">to</a> <a id="731" class="Function">idF</a><a id="734" class="Symbol">)</a>
 <a id="736" class="Keyword">open</a> <a id="741" class="Keyword">import</a> <a id="748" href="Categories.Enriched.NaturalTransformation.html" class="Module">Categories.Enriched.NaturalTransformation</a> <a id="790" href="Categories.Bicategory.Instance.EnrichedCats.html#284" class="Bound">M</a> <a id="792" class="Keyword">hiding</a> <a id="799" class="Symbol">(</a><a id="800" href="Categories.Enriched.NaturalTransformation.html#2210" class="Function">id</a><a id="802" class="Symbol">)</a>
-<a id="804" class="Keyword">import</a> <a id="811" href="Categories.Enriched.NaturalTransformation.NaturalIsomorphism.html" class="Module">Categories.Enriched.NaturalTransformation.NaturalIsomorphism</a> <a id="872" href="Categories.Bicategory.Instance.EnrichedCats.html#284" class="Bound">M</a> as <a id="NI"></a><a id="877" href="Categories.Bicategory.Instance.EnrichedCats.html#877" class="Module">NI</a>
+<a id="804" class="Keyword">import</a> <a id="811" href="Categories.Enriched.NaturalTransformation.NaturalIsomorphism.html" class="Module">Categories.Enriched.NaturalTransformation.NaturalIsomorphism</a> <a id="872" href="Categories.Bicategory.Instance.EnrichedCats.html#284" class="Bound">M</a> <a id="874" class="Symbol">as</a> <a id="NI"></a><a id="877" href="Categories.Bicategory.Instance.EnrichedCats.html#877" class="Module">NI</a>
 <a id="880" class="Keyword">open</a> <a id="885" class="Keyword">import</a> <a id="892" href="Categories.Functor.Bifunctor.html" class="Module">Categories.Functor.Bifunctor</a> <a id="921" class="Keyword">using</a> <a id="927" class="Symbol">(</a><a id="928" href="Categories.Functor.Bifunctor.html#442" class="Function">Bifunctor</a><a id="937" class="Symbol">)</a>
 <a id="939" class="Keyword">open</a> <a id="944" class="Keyword">import</a> <a id="951" href="Categories.Functor.Construction.Constant.html" class="Module">Categories.Functor.Construction.Constant</a> <a id="992" class="Keyword">using</a> <a id="998" class="Symbol">(</a><a id="999" href="Categories.Functor.Construction.Constant.html#461" class="Function">const</a><a id="1004" class="Symbol">)</a>
 <a id="1006" class="Keyword">open</a> <a id="1011" class="Keyword">import</a> <a id="1018" href="Categories.NaturalTransformation.NaturalIsomorphism.html" class="Module">Categories.NaturalTransformation.NaturalIsomorphism</a> <a id="1070" class="Keyword">using</a> <a id="1076" class="Symbol">(</a><a id="1077" href="Categories.NaturalTransformation.NaturalIsomorphism.html#2810" class="Function">niHelper</a><a id="1085" class="Symbol">)</a>

Categories.Bicategory.Instance.EnrichedCats.html

@@ -22,7 +22,7 @@
 
 <a id="853" class="Keyword">open</a> <a id="858" class="Keyword">import</a> <a id="865" href="Categories.Category.BinaryProducts.html" class="Module">Categories.Category.BinaryProducts</a> <a id="900" href="Categories.Category.CartesianClosed.Canonical.html#753" class="Bound">𝒞</a>
 <a id="902" class="Keyword">open</a> <a id="907" class="Keyword">import</a> <a id="914" href="Categories.Category.Cartesian.html" class="Module">Categories.Category.Cartesian</a> <a id="944" href="Categories.Category.CartesianClosed.Canonical.html#753" class="Bound">𝒞</a> <a id="946" class="Keyword">using</a> <a id="952" class="Symbol">(</a><a id="953" href="Categories.Category.Cartesian.html#727" class="Record">Cartesian</a><a id="962" class="Symbol">)</a>
-<a id="964" class="Keyword">import</a> <a id="971" href="Categories.Category.CartesianClosed.html" class="Module">Categories.Category.CartesianClosed</a> <a id="1007" href="Categories.Category.CartesianClosed.Canonical.html#753" class="Bound">𝒞</a> as <a id="𝒞-CC"></a><a id="1012" href="Categories.Category.CartesianClosed.Canonical.html#1012" class="Module">𝒞-CC</a>
+<a id="964" class="Keyword">import</a> <a id="971" href="Categories.Category.CartesianClosed.html" class="Module">Categories.Category.CartesianClosed</a> <a id="1007" href="Categories.Category.CartesianClosed.Canonical.html#753" class="Bound">𝒞</a> <a id="1009" class="Symbol">as</a> <a id="𝒞-CC"></a><a id="1012" href="Categories.Category.CartesianClosed.Canonical.html#1012" class="Module">𝒞-CC</a>
 <a id="1017" class="Keyword">open</a> <a id="1022" class="Keyword">import</a> <a id="1029" href="Categories.Object.Exponential.html" class="Module">Categories.Object.Exponential</a> <a id="1059" href="Categories.Category.CartesianClosed.Canonical.html#753" class="Bound">𝒞</a> <a id="1061" class="Keyword">using</a> <a id="1067" class="Symbol">(</a><a id="1068" href="Categories.Object.Exponential.html#583" class="Record">Exponential</a><a id="1079" class="Symbol">)</a>
 <a id="1081" class="Keyword">open</a> <a id="1086" class="Keyword">import</a> <a id="1093" href="Categories.Object.Product.html" class="Module">Categories.Object.Product</a> <a id="1119" href="Categories.Category.CartesianClosed.Canonical.html#753" class="Bound">𝒞</a>
 <a id="1121" class="Keyword">open</a> <a id="1126" class="Keyword">import</a> <a id="1133" href="Categories.Object.Terminal.html" class="Module">Categories.Object.Terminal</a> <a id="1160" href="Categories.Category.CartesianClosed.Canonical.html#753" class="Bound">𝒞</a> <a id="1162" class="Keyword">using</a> <a id="1168" class="Symbol">(</a><a id="1169" href="Categories.Object.Terminal.html#860" class="Record">Terminal</a><a id="1177" class="Symbol">)</a>

Categories.Category.CartesianClosed.Canonical.html

@@ -19,7 +19,7 @@
 <a id="615" class="Keyword">open</a> <a id="620" class="Keyword">import</a> <a id="627" href="Categories.Object.Exponential.html" class="Module">Categories.Object.Exponential</a>
 <a id="657" class="Keyword">open</a> <a id="662" class="Keyword">import</a> <a id="669" href="Categories.Object.Terminal.html" class="Module">Categories.Object.Terminal</a>
 <a id="696" class="Keyword">import</a> <a id="703" href="Categories.Diagram.Pullback.html" class="Module">Categories.Diagram.Pullback</a> <a id="731" class="Symbol">as</a> <a id="734" class="Module">P</a>
-<a id="736" class="Keyword">import</a> <a id="743" href="Categories.Diagram.Pullback.Properties.html" class="Module">Categories.Diagram.Pullback.Properties</a> <a id="782" href="Categories.Category.CartesianClosed.Locally.html#152" class="Bound">C</a> as <a id="Pₚ"></a><a id="787" href="Categories.Category.CartesianClosed.Locally.html#787" class="Module">Pₚ</a>
+<a id="736" class="Keyword">import</a> <a id="743" href="Categories.Diagram.Pullback.Properties.html" class="Module">Categories.Diagram.Pullback.Properties</a> <a id="782" href="Categories.Category.CartesianClosed.Locally.html#152" class="Bound">C</a> <a id="784" class="Symbol">as</a> <a id="Pₚ"></a><a id="787" href="Categories.Category.CartesianClosed.Locally.html#787" class="Module">Pₚ</a>
 <a id="790" class="Keyword">import</a> <a id="797" href="Categories.Morphism.Reasoning.html" class="Module">Categories.Morphism.Reasoning</a> <a id="827" class="Symbol">as</a> <a id="830" class="Module">MR</a>
 
 <a id="834" class="Keyword">open</a> <a id="839" href="Categories.Category.Core.html#442" class="Module">Category</a> <a id="848" href="Categories.Category.CartesianClosed.Locally.html#152" class="Bound">C</a>

Categories.Category.CartesianClosed.Locally.html

@@ -12,8 +12,8 @@
 <a id="251" class="Keyword">open</a> <a id="256" class="Keyword">import</a> <a id="263" href="Function.html" class="Module">Function</a> <a id="272" class="Keyword">using</a> <a id="278" class="Symbol">(</a><a id="279" href="Function.Base.html#1638" class="Function">flip</a><a id="283" class="Symbol">)</a>
 
 <a id="286" class="Keyword">open</a> <a id="291" class="Keyword">import</a> <a id="298" href="Categories.Category.Groupoid.html" class="Module">Categories.Category.Groupoid</a> <a id="327" class="Keyword">using</a> <a id="333" class="Symbol">(</a><a id="334" href="Categories.Category.Groupoid.html#807" class="Record">Groupoid</a><a id="342" class="Symbol">;</a> <a id="344" href="Categories.Category.Groupoid.html#189" class="Record">IsGroupoid</a><a id="354" class="Symbol">)</a>
-<a id="356" class="Keyword">open</a> <a id="361" class="Keyword">import</a> <a id="368" href="Categories.Morphism.html" class="Module">Categories.Morphism</a> <a id="388" href="Categories.Category.Construction.Core.html#194" class="Bound">𝒞</a> as <a id="Morphism"></a><a id="393" href="Categories.Category.Construction.Core.html#393" class="Module">Morphism</a>
-<a id="402" class="Keyword">open</a> <a id="407" class="Keyword">import</a> <a id="414" href="Categories.Morphism.IsoEquiv.html" class="Module">Categories.Morphism.IsoEquiv</a> <a id="443" href="Categories.Category.Construction.Core.html#194" class="Bound">𝒞</a> as <a id="IsoEquiv"></a><a id="448" href="Categories.Category.Construction.Core.html#448" class="Module">IsoEquiv</a>
+<a id="356" class="Keyword">open</a> <a id="361" class="Keyword">import</a> <a id="368" href="Categories.Morphism.html" class="Module">Categories.Morphism</a> <a id="388" href="Categories.Category.Construction.Core.html#194" class="Bound">𝒞</a> <a id="390" class="Symbol">as</a> <a id="Morphism"></a><a id="393" href="Categories.Category.Construction.Core.html#393" class="Module">Morphism</a>
+<a id="402" class="Keyword">open</a> <a id="407" class="Keyword">import</a> <a id="414" href="Categories.Morphism.IsoEquiv.html" class="Module">Categories.Morphism.IsoEquiv</a> <a id="443" href="Categories.Category.Construction.Core.html#194" class="Bound">𝒞</a> <a id="445" class="Symbol">as</a> <a id="IsoEquiv"></a><a id="448" href="Categories.Category.Construction.Core.html#448" class="Module">IsoEquiv</a>
 
 <a id="458" class="Keyword">open</a> <a id="463" href="Categories.Category.Core.html#442" class="Module">Category</a> <a id="472" href="Categories.Category.Construction.Core.html#194" class="Bound">𝒞</a>
 <a id="474" class="Keyword">open</a> <a id="479" href="Categories.Morphism.IsoEquiv.html#1761" class="Module Operator">_≃_</a>

Categories.Category.Construction.Core.html

@@ -10,10 +10,10 @@
 
 <a id="340" class="Keyword">open</a> <a id="345" class="Keyword">import</a> <a id="352" href="Data.Product.html" class="Module">Data.Product</a> <a id="365" class="Keyword">using</a> <a id="371" class="Symbol">(</a><a id="372" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="375" class="Symbol">)</a>
 
-<a id="378" class="Keyword">import</a> <a id="385" href="Categories.Category.Construction.Core.html" class="Module">Categories.Category.Construction.Core</a> <a id="423" href="Categories.Category.Monoidal.Braided.Properties.html#279" class="Bound">C</a> as <a id="Core"></a><a id="428" href="Categories.Category.Monoidal.Braided.Properties.html#428" class="Module">Core</a>
+<a id="378" class="Keyword">import</a> <a id="385" href="Categories.Category.Construction.Core.html" class="Module">Categories.Category.Construction.Core</a> <a id="423" href="Categories.Category.Monoidal.Braided.Properties.html#279" class="Bound">C</a> <a id="425" class="Symbol">as</a> <a id="Core"></a><a id="428" href="Categories.Category.Monoidal.Braided.Properties.html#428" class="Module">Core</a>
 <a id="433" class="Keyword">open</a> <a id="438" class="Keyword">import</a> <a id="445" href="Categories.Category.Monoidal.Properties.html" class="Module">Categories.Category.Monoidal.Properties</a> <a id="485" href="Categories.Category.Monoidal.Braided.Properties.html#300" class="Bound">M</a>
 <a id="487" class="Keyword">open</a> <a id="492" class="Keyword">import</a> <a id="499" href="Categories.Category.Monoidal.Reasoning.html" class="Module">Categories.Category.Monoidal.Reasoning</a> <a id="538" href="Categories.Category.Monoidal.Braided.Properties.html#300" class="Bound">M</a>
-<a id="540" class="Keyword">import</a> <a id="547" href="Categories.Category.Monoidal.Utilities.html" class="Module">Categories.Category.Monoidal.Utilities</a> <a id="586" href="Categories.Category.Monoidal.Braided.Properties.html#300" class="Bound">M</a> as <a id="MonoidalUtilities"></a><a id="591" href="Categories.Category.Monoidal.Braided.Properties.html#591" class="Module">MonoidalUtilities</a>
+<a id="540" class="Keyword">import</a> <a id="547" href="Categories.Category.Monoidal.Utilities.html" class="Module">Categories.Category.Monoidal.Utilities</a> <a id="586" href="Categories.Category.Monoidal.Braided.Properties.html#300" class="Bound">M</a> <a id="588" class="Symbol">as</a> <a id="MonoidalUtilities"></a><a id="591" href="Categories.Category.Monoidal.Braided.Properties.html#591" class="Module">MonoidalUtilities</a>
 <a id="609" class="Keyword">open</a> <a id="614" class="Keyword">import</a> <a id="621" href="Categories.Functor.html" class="Module">Categories.Functor</a> <a id="640" class="Keyword">using</a> <a id="646" class="Symbol">(</a><a id="647" href="Categories.Functor.Core.html#248" class="Record">Functor</a><a id="654" class="Symbol">)</a>
 <a id="656" class="Keyword">open</a> <a id="661" class="Keyword">import</a> <a id="668" href="Categories.Morphism.Reasoning.html" class="Module">Categories.Morphism.Reasoning</a> <a id="698" href="Categories.Category.Monoidal.Braided.Properties.html#279" class="Bound">C</a> <a id="700" class="Keyword">hiding</a> <a id="707" class="Symbol">(</a><a id="708" href="Categories.Morphism.Reasoning.Iso.html#4018" class="Function">push-eq</a><a id="715" class="Symbol">)</a>
 <a id="717" class="Keyword">open</a> <a id="722" class="Keyword">import</a> <a id="729" href="Categories.NaturalTransformation.NaturalIsomorphism.html" class="Module">Categories.NaturalTransformation.NaturalIsomorphism</a> <a id="781" class="Keyword">using</a> <a id="787" class="Symbol">(</a><a id="788" href="Categories.NaturalTransformation.NaturalIsomorphism.html#2810" class="Function">niHelper</a><a id="796" class="Symbol">)</a>

Categories.Category.Monoidal.Braided.Properties.html

@@ -13,7 +13,7 @@
 <a id="432" class="Keyword">open</a> <a id="437" class="Keyword">import</a> <a id="444" href="Level.html" class="Module">Level</a> <a id="450" class="Keyword">using</a> <a id="456" class="Symbol">(</a><a id="457" href="Agda.Primitive.html#961" class="Primitive Operator">_⊔_</a><a id="460" class="Symbol">)</a>
 <a id="462" class="Keyword">open</a> <a id="467" class="Keyword">import</a> <a id="474" href="Data.Product.html" class="Module">Data.Product</a> <a id="487" class="Keyword">using</a> <a id="493" class="Symbol">(</a><a id="494" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="497" class="Symbol">)</a>
 
-<a id="500" class="Keyword">import</a> <a id="507" href="Categories.Category.Construction.Core.html" class="Module">Categories.Category.Construction.Core</a> <a id="545" href="Categories.Category.Monoidal.Interchange.Braided.html#372" class="Bound">C</a> as <a id="Core"></a><a id="550" href="Categories.Category.Monoidal.Interchange.Braided.html#550" class="Module">Core</a>
+<a id="500" class="Keyword">import</a> <a id="507" href="Categories.Category.Construction.Core.html" class="Module">Categories.Category.Construction.Core</a> <a id="545" href="Categories.Category.Monoidal.Interchange.Braided.html#372" class="Bound">C</a> <a id="547" class="Symbol">as</a> <a id="Core"></a><a id="550" href="Categories.Category.Monoidal.Interchange.Braided.html#550" class="Module">Core</a>
 <a id="555" class="Keyword">import</a> <a id="562" href="Categories.Category.Monoidal.Construction.Product.html" class="Module">Categories.Category.Monoidal.Construction.Product</a> <a id="612" class="Symbol">as</a> <a id="615" class="Module">MonoidalProduct</a>
 <a id="631" class="Keyword">open</a> <a id="636" class="Keyword">import</a> <a id="643" href="Categories.Category.Monoidal.Braided.Properties.html" class="Module">Categories.Category.Monoidal.Braided.Properties</a> <a id="691" class="Symbol">as</a> <a id="694" class="Module">BraidedProps</a>
   <a id="709" class="Keyword">using</a> <a id="715" class="Symbol">(</a><a id="716" href="Categories.Category.Monoidal.Braided.Properties.html#3839" class="Function">braiding-coherence</a><a id="734" class="Symbol">;</a> <a id="736" href="Categories.Category.Monoidal.Braided.Properties.html#5168" class="Function">inv-Braided</a><a id="747" class="Symbol">;</a> <a id="749" href="Categories.Category.Monoidal.Braided.Properties.html#5617" class="Function">inv-braiding-coherence</a><a id="771" class="Symbol">)</a>