DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Expose bundles from Unit

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-11 21:20:05 -08:00
parent 5420bb808e
commit b1c6b4c99a
1 changed files with 17 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
Lattice/Unit.agda
View File

@ -89,6 +89,14 @@ isLattice = record
; absorb-⊓-⊔ = absorb-⊓-⊔ ; absorb-⊓-⊔ = absorb-⊓-⊔
} }
lattice : Lattice ⊤
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
private private
@ -104,3 +112,12 @@ isFiniteHeightLattice = record
{ isLattice = isLattice { isLattice = isLattice
; fixedHeight = (((tt , tt) , longestChain) , isLongest) ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
} }
finiteHeightLattice : FiniteHeightLattice ⊤
finiteHeightLattice = record
{ height = 0
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}