search

ualib / agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)
https://ualib.github.io/agda-algebras/
Creative Commons Attribution Share Alike 4.0 International
29 stars 7 forks source link

fix definition of closure systems #74

Closed williamdemeo closed 3 years ago

JacquesCarette commented 3 years ago

I don't. You can make things slightly more general with

IntersectClosed : {χ ℓ ρ : Level}{X : Type χ} → Pred (Pred X ℓ) ρ → Type _
IntersectClosed {ℓ = ℓ} {X = X} C = ∀ {I : Type ℓ}{c : I → Pred X ℓ} → (∀ i → (c i) ∈ C) → (⋂ I c) ∈ C

(I was doing things outside a module just in case forcing the same level on both definitions made a difference - it didn't).

If you truly want "very large" intersections, where the indexing type might be larger that the thing itself, you won't be able to avoid Lift. But perhaps intersections at the same size might be good enough?

williamdemeo commented 3 years ago

Nice observations and explanation. Now that you put it that way, yes, I agree. Here, and probably as a general principle, it should be okay to assume indexing types live at a level no higher than the things being indexed.