Finite coverings in locales

Content created by Fredrik Bakke, fernabnor and louismntnu.

Created on 2023-06-24.

module order-theory.finite-coverings-locales where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import order-theory.coverings-locales
open import order-theory.locales

open import univalent-combinatorics.finite-types


Idea

A finite covering of an object u in a locale is a finite family of objects whose join is u.

Definition

module _
{l1 l2 : Level} (L : Locale l1 l2) (u : type-Locale L)
where

is-finite-covering-Locale : (v : covering-Locale L u) → UU l2
is-finite-covering-Locale v = is-finite (indexing-type-covering-Locale L v)

finite-covering-Locale : UU (l1 ⊔ lsuc l2)
finite-covering-Locale =
Σ ( 𝔽 l2)
( λ I →
Σ ( type-𝔽 I → type-Locale L)
( is-covering-Locale L u))

module _
{l1 l2 : Level} (L : Locale l1 l2)
{u : type-Locale L} (v : finite-covering-Locale L u)
where

indexing-type-finite-covering-Locale : UU l2
indexing-type-finite-covering-Locale = type-𝔽 (pr1 v)

covering-family-finite-covering-Locale :
indexing-type-finite-covering-Locale → type-Locale L
covering-family-finite-covering-Locale = pr1 (pr2 v)

is-covering-finite-covering-Locale :
is-covering-Locale L u covering-family-finite-covering-Locale
is-covering-finite-covering-Locale = pr2 (pr2 v)

covering-finite-covering-Locale : covering-Locale L u
pr1 covering-finite-covering-Locale = indexing-type-finite-covering-Locale
pr1 (pr2 covering-finite-covering-Locale) =
covering-family-finite-covering-Locale
pr2 (pr2 covering-finite-covering-Locale) = is-covering-finite-covering-Locale

is-finite-covering-covering-Locale :
is-finite-covering-Locale L u covering-finite-covering-Locale
is-finite-covering-covering-Locale = is-finite-type-𝔽 (pr1 v)