Render HTML

rahulc29 · Jan 9, 2024 · 04a3069 · 04a3069
1 parent 32beff3
commit 04a3069
Show file tree

Hide file tree

Showing 12 changed files with 906 additions and 1,549 deletions.
diff --git a/docs/Realizability.Tripos.Algebra.Base.html b/docs/Realizability.Tripos.Algebra.Base.html
diff --git a/docs/Realizability.Tripos.Algebra.html b/docs/Realizability.Tripos.Algebra.html
diff --git a/docs/Realizability.Tripos.Everything.html b/docs/Realizability.Tripos.Everything.html
@@ -1,9 +1,7 @@
 <!DOCTYPE HTML>
 <html><head><meta charset="utf-8"><title>Realizability.Tripos.Everything</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">module</a> <a id="8" href="Realizability.Tripos.Everything.html" class="Module">Realizability.Tripos.Everything</a> <a id="40" class="Keyword">where</a>
 <a id="46" class="Keyword">open</a> <a id="51" class="Keyword">import</a> <a id="58" href="Realizability.Tripos.Predicate.html" class="Module">Realizability.Tripos.Predicate</a>
-<a id="89" class="Keyword">open</a> <a id="94" class="Keyword">import</a> <a id="101" href="Realizability.Tripos.PosetReflection.html" class="Module">Realizability.Tripos.PosetReflection</a>
-<a id="138" class="Keyword">open</a> <a id="143" class="Keyword">import</a> <a id="150" href="Realizability.Tripos.HeytingAlgebra.html" class="Module">Realizability.Tripos.HeytingAlgebra</a>
-<a id="186" class="Keyword">open</a> <a id="191" class="Keyword">import</a> <a id="198" href="Realizability.Tripos.Algebra.html" class="Module">Realizability.Tripos.Algebra</a>
-<a id="227" class="Keyword">open</a> <a id="232" class="Keyword">import</a> <a id="239" href="Realizability.Tripos.Algebra.Base.html" class="Module">Realizability.Tripos.Algebra.Base</a>
-<a id="273" class="Keyword">open</a> <a id="278" class="Keyword">import</a> <a id="285" href="Realizability.Tripos.Prealgebra.Everything.html" class="Module">Realizability.Tripos.Prealgebra.Everything</a>
+<a id="89" class="Keyword">open</a> <a id="94" class="Keyword">import</a> <a id="101" href="Realizability.Tripos.Algebra.html" class="Module">Realizability.Tripos.Algebra</a>
+<a id="130" class="Keyword">open</a> <a id="135" class="Keyword">import</a> <a id="142" href="Realizability.Tripos.Algebra.Base.html" class="Module">Realizability.Tripos.Algebra.Base</a>
+<a id="176" class="Keyword">open</a> <a id="181" class="Keyword">import</a> <a id="188" href="Realizability.Tripos.Prealgebra.Everything.html" class="Module">Realizability.Tripos.Prealgebra.Everything</a>
 </pre></body></html>
diff --git a/docs/Realizability.Tripos.Prealgebra.Absorbtion.html b/docs/Realizability.Tripos.Prealgebra.Absorbtion.html
diff --git a/docs/Realizability.Tripos.Prealgebra.Joins.Associativity.html b/docs/Realizability.Tripos.Prealgebra.Joins.Associativity.html
diff --git a/docs/Realizability.Tripos.Prealgebra.Meets.Associativity.html b/docs/Realizability.Tripos.Prealgebra.Meets.Associativity.html
diff --git a/docs/Realizability.Tripos.Prealgebra.Meets.Commutativity.html b/docs/Realizability.Tripos.Prealgebra.Meets.Commutativity.html
diff --git a/docs/Realizability.Tripos.Prealgebra.Meets.Idempotency.html b/docs/Realizability.Tripos.Prealgebra.Meets.Idempotency.html
diff --git a/docs/Realizability.Tripos.Prealgebra.Meets.Identity.html b/docs/Realizability.Tripos.Prealgebra.Meets.Identity.html
diff --git a/docs/Tripoi.HeytingAlgebra.html b/docs/Tripoi.HeytingAlgebra.html
diff --git a/docs/Tripoi.PosetReflection.html b/docs/Tripoi.PosetReflection.html
diff --git a/src/Realizability/Tripos/Algebra.agda b/src/Realizability/Tripos/Algebra.agda