Unions of finite subtypes
Content created by Fredrik Bakke and Victor Blanchi.
Created on 2023-03-21.
Last modified on 2024-02-06.
module univalent-combinatorics.unions-subtypes where open import foundation.unions-subtypes public
Imports
open import foundation.decidable-equality open import foundation.propositional-truncations open import foundation.subtypes open import foundation.universe-levels open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.counting open import univalent-combinatorics.counting-decidable-subtypes open import univalent-combinatorics.counting-dependent-pair-types open import univalent-combinatorics.embeddings open import univalent-combinatorics.finite-types
Properties
If A
has decidable equalities, P
and Q
are subtypes of A equipped with a counting, then P ∪ Q
is equipped with a counting
module _ {l1 l2 l3 : Level} {A : UU l1} (P : subtype l2 A) (Q : subtype l3 A) where count-union-subtypes-count-has-decidable-equalities : has-decidable-equality A → count (type-subtype P) → count (type-subtype Q) → count (type-subtype (union-subtype P Q)) count-union-subtypes-count-has-decidable-equalities dec-A count-P count-Q = count-decidable-emb ( decidable-emb-tot-trunc-Prop-count ( count-fiber-count-Σ dec-A (count-Σ-coproduct count-P count-Q))) ( count-Σ-coproduct count-P count-Q)
If A
has decidable equalities and P
and Q
are both finite, then P ∪ Q
is also finite
module _ {l1 l2 l3 : Level} {A : UU l1} (P : subtype l2 A) (Q : subtype l3 A) where finite-union-subtypes-finite-has-decidable-equalities : has-decidable-equality A → is-finite (type-subtype P) → is-finite (type-subtype Q) → is-finite (type-subtype (union-subtype P Q)) finite-union-subtypes-finite-has-decidable-equalities dec-A fin-P fin-Q = apply-twice-universal-property-trunc-Prop ( fin-P) ( fin-Q) ( is-finite-Prop (type-subtype (union-subtype P Q))) ( λ count-P count-Q → unit-trunc-Prop ( count-union-subtypes-count-has-decidable-equalities P Q dec-A count-P count-Q))
Recent changes
- 2024-02-06. Fredrik Bakke. Rename
(co)prod
to(co)product
(#1017). - 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-21. Fredrik Bakke. Formatting fixes (#530).