-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathAlgebra.Properties.Semilattice.html
91 lines (74 loc) · 13.8 KB
/
Algebra.Properties.Semilattice.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Algebra.Properties.Semilattice</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Some derivable properties</a>
<a id="135" class="Comment">------------------------------------------------------------------------</a>
<a id="209" class="Symbol">{-#</a> <a id="213" class="Keyword">OPTIONS</a> <a id="221" class="Pragma">--without-K</a> <a id="233" class="Pragma">--safe</a> <a id="240" class="Symbol">#-}</a>
<a id="245" class="Keyword">open</a> <a id="250" class="Keyword">import</a> <a id="257" href="Algebra.html" class="Module">Algebra</a>
<a id="266" class="Keyword">module</a> <a id="273" href="Algebra.Properties.Semilattice.html" class="Module">Algebra.Properties.Semilattice</a> <a id="304" class="Symbol">{</a><a id="305" href="Algebra.Properties.Semilattice.html#305" class="Bound">c</a> <a id="307" href="Algebra.Properties.Semilattice.html#307" class="Bound">ℓ</a><a id="308" class="Symbol">}</a> <a id="310" class="Symbol">(</a><a id="311" href="Algebra.Properties.Semilattice.html#311" class="Bound">L</a> <a id="313" class="Symbol">:</a> <a id="315" href="Algebra.Bundles.html#3473" class="Record">Semilattice</a> <a id="327" href="Algebra.Properties.Semilattice.html#305" class="Bound">c</a> <a id="329" href="Algebra.Properties.Semilattice.html#307" class="Bound">ℓ</a><a id="330" class="Symbol">)</a> <a id="332" class="Keyword">where</a>
<a id="339" class="Keyword">open</a> <a id="344" href="Algebra.Bundles.html#3473" class="Module">Semilattice</a> <a id="356" href="Algebra.Properties.Semilattice.html#311" class="Bound">L</a>
<a id="359" class="Keyword">open</a> <a id="364" class="Keyword">import</a> <a id="371" href="Algebra.Structures.html" class="Module">Algebra.Structures</a>
<a id="390" class="Keyword">open</a> <a id="395" class="Keyword">import</a> <a id="402" href="Function.html" class="Module">Function</a>
<a id="411" class="Keyword">open</a> <a id="416" class="Keyword">import</a> <a id="423" href="Data.Product.html" class="Module">Data.Product</a>
<a id="436" class="Keyword">open</a> <a id="441" class="Keyword">import</a> <a id="448" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="464" class="Keyword">open</a> <a id="469" class="Keyword">import</a> <a id="476" href="Relation.Binary.Reasoning.Setoid.html" class="Module">Relation.Binary.Reasoning.Setoid</a> <a id="509" href="Algebra.Structures.html#1285" class="Function">setoid</a>
<a id="516" class="Keyword">import</a> <a id="523" href="Relation.Binary.Construct.NaturalOrder.Left.html" class="Module">Relation.Binary.Construct.NaturalOrder.Left</a> <a id="567" href="Algebra.Bundles.html#3583" class="Field Operator">_≈_</a> <a id="571" href="Algebra.Bundles.html#3617" class="Field Operator">_∧_</a> as <a id="LeftNaturalOrder"></a><a id="578" href="Algebra.Properties.Semilattice.html#578" class="Module">LeftNaturalOrder</a>
<a id="595" class="Keyword">open</a> <a id="600" class="Keyword">import</a> <a id="607" href="Relation.Binary.Lattice.html" class="Module">Relation.Binary.Lattice</a>
<a id="631" class="Keyword">import</a> <a id="638" href="Relation.Binary.Properties.Poset.html" class="Module">Relation.Binary.Properties.Poset</a> <a id="671" class="Symbol">as</a> <a id="674" class="Module">PosetProperties</a>
<a id="690" class="Keyword">open</a> <a id="695" class="Keyword">import</a> <a id="702" href="Relation.Binary.Reasoning.Setoid.html" class="Module">Relation.Binary.Reasoning.Setoid</a> <a id="735" href="Algebra.Structures.html#1285" class="Function">setoid</a>
<a id="743" class="Comment">------------------------------------------------------------------------</a>
<a id="816" class="Comment">-- Every semilattice can be turned into a poset via the left natural</a>
<a id="885" class="Comment">-- order.</a>
<a id="poset"></a><a id="896" href="Algebra.Properties.Semilattice.html#896" class="Function">poset</a> <a id="902" class="Symbol">:</a> <a id="904" href="Relation.Binary.Bundles.html#3028" class="Record">Poset</a> <a id="910" href="Algebra.Properties.Semilattice.html#305" class="Bound">c</a> <a id="912" href="Algebra.Properties.Semilattice.html#307" class="Bound">ℓ</a> <a id="914" href="Algebra.Properties.Semilattice.html#307" class="Bound">ℓ</a>
<a id="916" href="Algebra.Properties.Semilattice.html#896" class="Function">poset</a> <a id="922" class="Symbol">=</a> <a id="924" href="Relation.Binary.Construct.NaturalOrder.Left.html#4896" class="Function">LeftNaturalOrder.poset</a> <a id="947" href="Algebra.Bundles.html#3649" class="Field">isSemilattice</a>
<a id="962" class="Keyword">open</a> <a id="967" href="Relation.Binary.Bundles.html#3028" class="Module">Poset</a> <a id="973" href="Algebra.Properties.Semilattice.html#896" class="Function">poset</a> <a id="979" class="Keyword">using</a> <a id="985" class="Symbol">(</a><a id="986" href="Relation.Binary.Bundles.html#3167" class="Field Operator">_≤_</a><a id="989" class="Symbol">;</a> <a id="991" href="Relation.Binary.Bundles.html#3203" class="Field">isPartialOrder</a><a id="1005" class="Symbol">)</a>
<a id="1007" class="Keyword">open</a> <a id="1012" href="Relation.Binary.Properties.Poset.html" class="Module">PosetProperties</a> <a id="1028" href="Algebra.Properties.Semilattice.html#896" class="Function">poset</a> <a id="1034" class="Keyword">using</a> <a id="1040" class="Symbol">(</a><a id="1041" href="Relation.Binary.Properties.Poset.html#825" class="Function Operator">_≥_</a><a id="1044" class="Symbol">;</a> <a id="1046" href="Relation.Binary.Properties.Poset.html#979" class="Function">≥-isPartialOrder</a><a id="1062" class="Symbol">)</a>
<a id="1065" class="Comment">------------------------------------------------------------------------</a>
<a id="1138" class="Comment">-- Every algebraic semilattice can be turned into an order-theoretic one.</a>
<a id="∧-isOrderTheoreticMeetSemilattice"></a><a id="1213" href="Algebra.Properties.Semilattice.html#1213" class="Function">∧-isOrderTheoreticMeetSemilattice</a> <a id="1247" class="Symbol">:</a> <a id="1249" href="Relation.Binary.Lattice.html#4003" class="Record">IsMeetSemilattice</a> <a id="1267" href="Algebra.Bundles.html#3583" class="Field Operator">_≈_</a> <a id="1271" href="Relation.Binary.Bundles.html#3167" class="Function Operator">_≤_</a> <a id="1275" href="Algebra.Bundles.html#3617" class="Field Operator">_∧_</a>
<a id="1279" href="Algebra.Properties.Semilattice.html#1213" class="Function">∧-isOrderTheoreticMeetSemilattice</a> <a id="1313" class="Symbol">=</a> <a id="1315" class="Keyword">record</a>
<a id="1324" class="Symbol">{</a> <a id="1326" href="Relation.Binary.Lattice.html#4305" class="Field">isPartialOrder</a> <a id="1341" class="Symbol">=</a> <a id="1343" href="Relation.Binary.Bundles.html#3203" class="Function">isPartialOrder</a>
<a id="1360" class="Symbol">;</a> <a id="1362" href="Relation.Binary.Lattice.html#4349" class="Field">infimum</a> <a id="1377" class="Symbol">=</a> <a id="1379" href="Relation.Binary.Construct.NaturalOrder.Left.html#3347" class="Function">LeftNaturalOrder.infimum</a> <a id="1404" href="Algebra.Bundles.html#3649" class="Field">isSemilattice</a>
<a id="1420" class="Symbol">}</a>
<a id="∧-isOrderTheoreticJoinSemilattice"></a><a id="1423" href="Algebra.Properties.Semilattice.html#1423" class="Function">∧-isOrderTheoreticJoinSemilattice</a> <a id="1457" class="Symbol">:</a> <a id="1459" href="Relation.Binary.Lattice.html#1172" class="Record">IsJoinSemilattice</a> <a id="1477" href="Algebra.Bundles.html#3583" class="Field Operator">_≈_</a> <a id="1481" href="Relation.Binary.Properties.Poset.html#825" class="Function Operator">_≥_</a> <a id="1485" href="Algebra.Bundles.html#3617" class="Field Operator">_∧_</a>
<a id="1489" href="Algebra.Properties.Semilattice.html#1423" class="Function">∧-isOrderTheoreticJoinSemilattice</a> <a id="1523" class="Symbol">=</a> <a id="1525" class="Keyword">record</a>
<a id="1534" class="Symbol">{</a> <a id="1536" href="Relation.Binary.Lattice.html#1474" class="Field">isPartialOrder</a> <a id="1551" class="Symbol">=</a> <a id="1553" href="Relation.Binary.Properties.Poset.html#979" class="Function">≥-isPartialOrder</a>
<a id="1572" class="Symbol">;</a> <a id="1574" href="Relation.Binary.Lattice.html#1518" class="Field">supremum</a> <a id="1589" class="Symbol">=</a> <a id="1591" href="Relation.Binary.Lattice.html#4349" class="Field">IsMeetSemilattice.infimum</a>
<a id="1640" href="Algebra.Properties.Semilattice.html#1213" class="Function">∧-isOrderTheoreticMeetSemilattice</a>
<a id="1676" class="Symbol">}</a>
<a id="∧-orderTheoreticMeetSemilattice"></a><a id="1679" href="Algebra.Properties.Semilattice.html#1679" class="Function">∧-orderTheoreticMeetSemilattice</a> <a id="1711" class="Symbol">:</a> <a id="1713" href="Relation.Binary.Lattice.html#4715" class="Record">MeetSemilattice</a> <a id="1729" href="Algebra.Properties.Semilattice.html#305" class="Bound">c</a> <a id="1731" href="Algebra.Properties.Semilattice.html#307" class="Bound">ℓ</a> <a id="1733" href="Algebra.Properties.Semilattice.html#307" class="Bound">ℓ</a>
<a id="1735" href="Algebra.Properties.Semilattice.html#1679" class="Function">∧-orderTheoreticMeetSemilattice</a> <a id="1767" class="Symbol">=</a> <a id="1769" class="Keyword">record</a>
<a id="1778" class="Symbol">{</a> <a id="1780" href="Relation.Binary.Lattice.html#5040" class="Field">isMeetSemilattice</a> <a id="1798" class="Symbol">=</a> <a id="1800" href="Algebra.Properties.Semilattice.html#1213" class="Function">∧-isOrderTheoreticMeetSemilattice</a>
<a id="1836" class="Symbol">}</a>
<a id="∧-orderTheoreticJoinSemilattice"></a><a id="1839" href="Algebra.Properties.Semilattice.html#1839" class="Function">∧-orderTheoreticJoinSemilattice</a> <a id="1871" class="Symbol">:</a> <a id="1873" href="Relation.Binary.Lattice.html#1882" class="Record">JoinSemilattice</a> <a id="1889" href="Algebra.Properties.Semilattice.html#305" class="Bound">c</a> <a id="1891" href="Algebra.Properties.Semilattice.html#307" class="Bound">ℓ</a> <a id="1893" href="Algebra.Properties.Semilattice.html#307" class="Bound">ℓ</a>
<a id="1895" href="Algebra.Properties.Semilattice.html#1839" class="Function">∧-orderTheoreticJoinSemilattice</a> <a id="1927" class="Symbol">=</a> <a id="1929" class="Keyword">record</a>
<a id="1938" class="Symbol">{</a> <a id="1940" href="Relation.Binary.Lattice.html#2207" class="Field">isJoinSemilattice</a> <a id="1958" class="Symbol">=</a> <a id="1960" href="Algebra.Properties.Semilattice.html#1423" class="Function">∧-isOrderTheoreticJoinSemilattice</a>
<a id="1996" class="Symbol">}</a>
<a id="2000" class="Comment">------------------------------------------------------------------------</a>
<a id="2073" class="Comment">-- DEPRECATED NAMES</a>
<a id="2093" class="Comment">------------------------------------------------------------------------</a>
<a id="2166" class="Comment">-- Please use the new names as continuing support for the old names is</a>
<a id="2237" class="Comment">-- not guaranteed.</a>
<a id="2257" class="Comment">-- Version 1.1</a>
<a id="isOrderTheoreticMeetSemilattice"></a><a id="2273" href="Algebra.Properties.Semilattice.html#2273" class="Function">isOrderTheoreticMeetSemilattice</a> <a id="2305" class="Symbol">=</a> <a id="2307" href="Algebra.Properties.Semilattice.html#1213" class="Function">∧-isOrderTheoreticMeetSemilattice</a>
<a id="2341" class="Symbol">{-#</a> <a id="2345" class="Keyword">WARNING_ON_USAGE</a> <a id="2362" class="Pragma">isOrderTheoreticMeetSemilattice</a>
<a id="2394" class="String">"Warning: isOrderTheoreticMeetSemilattice was deprecated in v1.1.
Please use ∧-isOrderTheoreticMeetSemilattice instead."</a>
<a id="2515" class="Symbol">#-}</a>
<a id="isOrderTheoreticJoinSemilattice"></a><a id="2519" href="Algebra.Properties.Semilattice.html#2519" class="Function">isOrderTheoreticJoinSemilattice</a> <a id="2551" class="Symbol">=</a> <a id="2553" href="Algebra.Properties.Semilattice.html#1423" class="Function">∧-isOrderTheoreticJoinSemilattice</a>
<a id="2587" class="Symbol">{-#</a> <a id="2591" class="Keyword">WARNING_ON_USAGE</a> <a id="2608" class="Pragma">isOrderTheoreticJoinSemilattice</a>
<a id="2640" class="String">"Warning: isOrderTheoreticJoinSemilattice was deprecated in v1.1.
Please use ∧-isOrderTheoreticJoinSemilattice instead."</a>
<a id="2761" class="Symbol">#-}</a>
<a id="orderTheoreticMeetSemilattice"></a><a id="2765" href="Algebra.Properties.Semilattice.html#2765" class="Function">orderTheoreticMeetSemilattice</a> <a id="2795" class="Symbol">=</a> <a id="2797" href="Algebra.Properties.Semilattice.html#1679" class="Function">∧-orderTheoreticMeetSemilattice</a>
<a id="2829" class="Symbol">{-#</a> <a id="2833" class="Keyword">WARNING_ON_USAGE</a> <a id="2850" class="Pragma">orderTheoreticMeetSemilattice</a>
<a id="2880" class="String">"Warning: orderTheoreticMeetSemilattice was deprecated in v1.1.
Please use ∧-orderTheoreticMeetSemilattice instead."</a>
<a id="2997" class="Symbol">#-}</a>
<a id="orderTheoreticJoinSemilattice"></a><a id="3001" href="Algebra.Properties.Semilattice.html#3001" class="Function">orderTheoreticJoinSemilattice</a> <a id="3031" class="Symbol">=</a> <a id="3033" href="Algebra.Properties.Semilattice.html#1839" class="Function">∧-orderTheoreticJoinSemilattice</a>
<a id="3065" class="Symbol">{-#</a> <a id="3069" class="Keyword">WARNING_ON_USAGE</a> <a id="3086" class="Pragma">orderTheoreticJoinSemilattice</a>
<a id="3116" class="String">"Warning: orderTheoreticJoinSemilattice was deprecated in v1.1.
Please use ∧-orderTheoreticJoinSemilattice instead."</a>
<a id="3233" class="Symbol">#-}</a>
</pre></body></html>