# Unions of finite subtypes

Content created by Fredrik Bakke and Victor Blanchi.

Created on 2023-03-21.

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))