Example:
module Quantity where
open import Data.Nat.Base
open import Data.Product.Base
open import Data.Unit.Base
-- A quantity is a non-empty set of natural numbers
record Quantity : Set₁ where
field
has : ℕ → Set
non-empty : ∃ has
open Quantity
ω : Quantity
ω .has n = ⊤
ω .non-empty = 0 , _
-- A raw modality structure is a set of quantities containing at least ω
record ModalityStructure : Set₁ where
field
Member : Quantity → Set
has-ω : Member ω
-- open ModalityStructure
-- We define the operations pointwise
module _ (M : ModalityStructure) (open ModalityStructure M) where
-- A collection of modalities
record ModalitySet : Set₁ where
field
Elem : Quantity → Set
is-subset : ∀ {p} → Elem p → Member p
open ModalitySet
-- The infimum of a modality set
record IsLowerBound (S : ModalitySet) (p : Quantity) : Set where
field
lb : ∀{q} → (s : S .Elem q) → ∀{n} → q .has n → p .has n
Error:
Set₁ is not less or equal than Set
when checking that the type
{q : Quantity} → S .Elem q → {n : ℕ} → q .has n → p .has n of an
argument to the constructor Quantity.IsLowerBound.constructor fits
in the sort Set of the datatype.
You can’t perform that action at this time.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4