Small Composition of species of finite inhabited types
{-# OPTIONS --lossy-unification #-} module species.small-cauchy-composition-species-of-finite-inhabited-types where
Imports
open import foundation.contractible-types open import foundation.decidable-types open import foundation.equivalences open import foundation.functions open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.inhabited-types open import foundation.propositions open import foundation.relaxed-sigma-decompositions open import foundation.sigma-decomposition-subuniverse open import foundation.subuniverses open import foundation.type-arithmetic-cartesian-product-types open import foundation.unit-type open import foundation.universe-levels open import species.small-cauchy-composition-species-of-types-in-subuniverses open import species.species-of-finite-inhabited-types open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.decidable-propositions open import univalent-combinatorics.dependent-function-types open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.finite-types open import univalent-combinatorics.inhabited-finite-types open import univalent-combinatorics.sigma-decompositions open import univalent-combinatorics.small-types
Definition
equiv-Σ-Decomposition-Inhabited-𝔽-Σ-Decomposition-𝔽 : {l : Level} (X : Inhabited-𝔽 l) → Σ-Decomposition-𝔽 l l (finite-type-Inhabited-𝔽 X) ≃ Σ-Decomposition-Subuniverse ( is-finite-and-inhabited-Prop) ( map-compute-Inhabited-𝔽' X) equiv-Σ-Decomposition-Inhabited-𝔽-Σ-Decomposition-𝔽 X = ( inv-equiv ( equiv-total-is-in-subuniverse-Σ-Decomposition ( is-finite-and-inhabited-Prop) ( map-compute-Inhabited-𝔽' X))) ∘e ( ( equiv-tot ( λ D → equiv-prod ( equiv-add-redundant-prop ( is-property-is-inhabited _) ( λ _ → map-is-inhabited ( pr1 ∘ map-matching-correspondence-Relaxed-Σ-Decomposition D) ( is-inhabited-type-Inhabited-𝔽 X))) ( id-equiv))) ∘e ( ( equiv-Relaxed-Σ-Decomposition-Σ-Decomposition-𝔽 (finite-type-Inhabited-𝔽 X)))) is-finite-Σ-Decomposition-Subuniverse-Inhabited-𝔽 : {l : Level} (X : Inhabited-𝔽 l) → is-finite ( Σ-Decomposition-Subuniverse ( is-finite-and-inhabited-Prop {l}) ( map-compute-Inhabited-𝔽' X)) is-finite-Σ-Decomposition-Subuniverse-Inhabited-𝔽 X = is-finite-equiv ( equiv-Σ-Decomposition-Inhabited-𝔽-Σ-Decomposition-𝔽 X) ( is-finite-Σ-Decomposition-𝔽 (finite-type-Inhabited-𝔽 X)) finite-Σ-Decomposition-Subuniverse-Inhabited-𝔽 : {l : Level} (X : Inhabited-𝔽 l) → 𝔽 (lsuc l) pr1 (finite-Σ-Decomposition-Subuniverse-Inhabited-𝔽 {l} X) = Σ-Decomposition-Subuniverse ( is-finite-and-inhabited-Prop {l}) ( map-compute-Inhabited-𝔽' X) pr2 (finite-Σ-Decomposition-Subuniverse-Inhabited-𝔽 X) = is-finite-Σ-Decomposition-Subuniverse-Inhabited-𝔽 X module _ {l1 l2 : Level} where finite-small-cauchy-composition-species-subuniverse : ( S T : species-Inhabited-𝔽 l1 (l1 ⊔ l2)) (X : Inhabited-𝔽 l1) → 𝔽 (lsuc l1 ⊔ l2) finite-small-cauchy-composition-species-subuniverse S T X = Σ-𝔽 ( finite-Σ-Decomposition-Subuniverse-Inhabited-𝔽 X) ( λ D → prod-𝔽 ( S ( subuniverse-indexing-type-Σ-Decomposition-Subuniverse ( is-finite-and-inhabited-Prop) ( map-compute-Inhabited-𝔽' X) ( D))) ( Π-𝔽 ( finite-type-Inhabited-𝔽 ( map-inv-compute-Inhabited-𝔽' ( subuniverse-indexing-type-Σ-Decomposition-Subuniverse ( is-finite-and-inhabited-Prop) ( map-compute-Inhabited-𝔽' X) ( D)))) ( λ x → T ( subuniverse-cotype-Σ-Decomposition-Subuniverse ( is-finite-and-inhabited-Prop) ( map-compute-Inhabited-𝔽' X) ( D) ( x))))) private C1 : ( S T : species-Inhabited-𝔽 l1 (l1 ⊔ l2)) → ( X : type-subuniverse is-finite-and-inhabited-Prop) → is-small (l1 ⊔ l2) ( small-cauchy-composition-species-subuniverse' is-finite-and-inhabited-Prop is-finite-Prop S T X) C1 S T X = is-small-is-finite (l1 ⊔ l2) ( finite-small-cauchy-composition-species-subuniverse S T (map-inv-compute-Inhabited-𝔽' X)) C2 : ( S T : species-Inhabited-𝔽 l1 (l1 ⊔ l2)) → (X : type-subuniverse is-finite-and-inhabited-Prop) → is-finite (type-is-small (C1 S T X)) C2 S T X = is-finite-equiv ( equiv-is-small (C1 S T X)) ( is-finite-type-𝔽 ( finite-small-cauchy-composition-species-subuniverse ( S) ( T) ( map-inv-compute-Inhabited-𝔽' X))) C3 : is-closed-under-Σ-subuniverse (is-finite-and-inhabited-Prop {l1}) C3 X Y = is-finite-Σ ( is-finite-Inhabited-𝔽 (map-inv-compute-Inhabited-𝔽' X)) ( λ x → is-finite-Inhabited-𝔽 (map-inv-compute-Inhabited-𝔽' (Y x))) , is-inhabited-Σ ( is-inhabited-type-Inhabited-𝔽 ( map-inv-compute-Inhabited-𝔽' X)) ( λ x → is-inhabited-type-Inhabited-𝔽 ( map-inv-compute-Inhabited-𝔽' (Y x))) C4 : is-finite-and-inhabited (raise-unit l1) C4 = is-finite-is-contr is-contr-raise-unit , is-inhabited-is-contr is-contr-raise-unit C5 : (X : UU l1) → is-small (l1 ⊔ l2) (is-contr X) C5 X = is-small-lmax l2 (is-contr X) C6 : ( X : type-subuniverse {l1} is-finite-and-inhabited-Prop) → ( is-finite ( type-is-small ( C5 ( inclusion-subuniverse is-finite-and-inhabited-Prop X)))) C6 X = is-finite-is-decidable-Prop ( _ , is-prop-equiv ( inv-equiv ( equiv-is-small ( is-small-lmax l2 ( is-contr ( type-Inhabited-𝔽 ( map-inv-compute-Inhabited-𝔽' X)))))) ( is-property-is-contr)) ( is-decidable-equiv ( inv-equiv ( equiv-is-small ( is-small-lmax ( l2) ( is-contr ( type-Inhabited-𝔽 ( map-inv-compute-Inhabited-𝔽' X)))))) ( is-decidable-is-contr-is-finite ( is-finite-Inhabited-𝔽 (map-inv-compute-Inhabited-𝔽' X)))) small-cauchy-composition-species-Inhabited-𝔽 : species-Inhabited-𝔽 l1 (l1 ⊔ l2) → species-Inhabited-𝔽 l1 (l1 ⊔ l2)→ species-Inhabited-𝔽 l1 (l1 ⊔ l2) small-cauchy-composition-species-Inhabited-𝔽 = small-cauchy-composition-species-subuniverse is-finite-and-inhabited-Prop is-finite-Prop C1 C2 C3 small-cauchy-composition-unit-species-Inhabited-𝔽 : species-Inhabited-𝔽 l1 (l1 ⊔ l2) small-cauchy-composition-unit-species-Inhabited-𝔽 = small-cauchy-composition-unit-species-subuniverse is-finite-and-inhabited-Prop is-finite-Prop C1 C2 C3 C4 C5 C6 left-unit-law-small-cauchy-composition-species-Inhabited-𝔽 : ( S : species-Inhabited-𝔽 l1 (l1 ⊔ l2)) → small-cauchy-composition-species-Inhabited-𝔽 small-cauchy-composition-unit-species-Inhabited-𝔽 S ＝ S left-unit-law-small-cauchy-composition-species-Inhabited-𝔽 = left-unit-law-small-cauchy-composition-species-subuniverse is-finite-and-inhabited-Prop is-finite-Prop C1 C2 C3 C4 C5 C6 right-unit-law-small-cauchy-composition-species-Inhabited-𝔽 : ( S : species-Inhabited-𝔽 l1 (l1 ⊔ l2)) → small-cauchy-composition-species-Inhabited-𝔽 S small-cauchy-composition-unit-species-Inhabited-𝔽 ＝ S right-unit-law-small-cauchy-composition-species-Inhabited-𝔽 = right-unit-law-small-cauchy-composition-species-subuniverse is-finite-and-inhabited-Prop is-finite-Prop C1 C2 C3 C4 C5 C6 associative-small-cauchy-composition-species-Inhabited-𝔽 : (S T U : species-Inhabited-𝔽 l1 (l1 ⊔ l2)) → small-cauchy-composition-species-Inhabited-𝔽 ( S) ( small-cauchy-composition-species-Inhabited-𝔽 T U) ＝ small-cauchy-composition-species-Inhabited-𝔽 ( small-cauchy-composition-species-Inhabited-𝔽 S T) ( U) associative-small-cauchy-composition-species-Inhabited-𝔽 = associative-small-cauchy-composition-species-subuniverse is-finite-and-inhabited-Prop is-finite-Prop C1 C2 C3