{-# OPTIONS --without-K --rewriting #-}
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers
open import foundation.action-on-identifications-functions
open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equality-coproduct-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.functoriality-truncation
open import foundation.identity-types
open import foundation.locally-small-types
open import foundation.propositional-maps
open import foundation.propositional-truncations
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.transport-along-identifications
open import foundation.truncated-maps
open import foundation.truncated-types
open import foundation.truncations
open import foundation.truncation-levels
renaming (truncation-level-minus-one-ℕ to minus-one;
truncation-level-minus-two-ℕ to minus-two;
truncation-level-ℕ to to-𝕋)
open import foundation.type-arithmetic-empty-type
open import foundation.type-arithmetic-unit-type
open import foundation.type-arithmetic-booleans
open import foundation.unit-type
open import foundation.univalence
open import foundation.universe-levels
open import e-structure.core
open import functor.n-slice
open import image-factorisation
open import notation hiding (sup)
module fixed-point.unordered-tupling {i j}
(m n k : ℕ) (p : m == add-ℕ' n k)
(V : UU j) (fixed-point-V : V ≃ T-[ m ] i V)
(is-n+1-small-V : is-[ succ-ℕ n ]-small i V) where
open import fixed-point.core m V fixed-point-V
open import e-structure.property.unordered-tupling ∈-structure-V
unordered-tuple : (I : UU i) → (I → V) → V
unordered-tuple I σ =
sup
(trunc-Image is-n+1-small-V σ ,
trunc-image-inclusion-eq-add-ℕ' k (succ-ℕ m) (ap succ-ℕ p) is-n+1-small-V σ)
∈-unordered-tuple : (I : UU i)
→ (σ : I → V)
→ (z : V)
→ (z ∈ unordered-tuple I σ) ≃ type-trunc (minus-one n) (Σ I λ i → σ i == z)
∈-unordered-tuple I σ z =
equivalence-reasoning
z ∈ unordered-tuple I σ
≃ fiber (map-trunc-map
(trunc-image-inclusion-eq-add-ℕ' _ _
(ap succ-ℕ p) is-n+1-small-V σ)) z by equiv-eq (∈-sup z)
≃ type-trunc (minus-one n) (Σ I λ i → σ i == z) by equiv-fiber-trunc-Image-im is-n+1-small-V σ z
n-unordered-tupling : (I : UU i) → [ n ]-UnorderedTupling I
n-unordered-tupling I σ = (unordered-tuple I σ , ∈-unordered-tuple I σ)
module ∞-unordered-tupling-from-k=0 (q : k == 0) where
∞-unordered-tupling : (l : ℕ) → l <-ℕ n
→ (I : Truncated-Type i (to-𝕋 l))
→ ∞-UnorderedTupling (type-Truncated-Type I)
pr1 (∞-unordered-tupling l l<-ℕn (I , is-trunc-I) σ) = unordered-tuple I σ
pr2 (∞-unordered-tupling l l<-ℕn (I , is-trunc-I) σ) z =
equivalence-reasoning
z ∈ unordered-tuple I σ
≃ type-trunc (minus-one n) (Σ I λ i → σ i == z) by ∈-unordered-tuple I σ z
≃ Σ I (λ i → σ i == z) by inv-equiv
(equiv-unit-trunc
(Σ-Truncated-Type
(I , is-trunc-I')
(λ i → Id-Truncated-Type
(V , tr (λ l → is-trunc (to-𝕋 l) V)
(p ∙ (ap (add-ℕ' n) q ∙ commutative-add-ℕ 0 n))
is-trunc-V)
(σ i)
z)))
where
is-trunc-add-ℕ : (j j' : ℕ)
→ is-trunc (to-𝕋 j) I
→ is-trunc (to-𝕋 (add-ℕ j j')) I
is-trunc-add-ℕ j zero-ℕ = id
is-trunc-add-ℕ j (succ-ℕ j') is-trunc-V =
is-trunc-succ-is-trunc _
(is-trunc-add-ℕ j j' is-trunc-V)
H : Σ ℕ (λ x → succ-ℕ (add-ℕ x l) == n)
H = subtraction-leq-ℕ (succ-ℕ l) n (leq-succ-le-ℕ l n l<-ℕn)
is-trunc-I' : is-trunc (minus-one n) I
is-trunc-I' = tr (λ j → is-trunc (minus-one j) I)
(ap succ-ℕ (commutative-add-ℕ l (pr1 H)) ∙ pr2 H)
(is-trunc-add-ℕ l (pr1 H) is-trunc-I)
singletons : [ n ]-Singletons
pr1 (singletons x) = pr1 (n-unordered-tupling (raise-unit i) (λ _ → x))
pr2 (singletons x) y =
equivalence-reasoning
y ∈ _
≃ type-trunc (minus-one n) ((raise-unit i) × (x == y)) by pr2 (n-unordered-tupling (raise-unit i) (λ _ → x)) y
≃ type-trunc (minus-one n) (unit × (x == y)) by equiv-trunc (minus-one n)
(equiv-Σ-equiv-base
(λ t → x == y)
(inv-equiv (compute-raise-unit i)))
≃ type-trunc (minus-one n) (x == y) by equiv-trunc (minus-one n) left-unit-law-prod
open singletons.notation singletons public
∞-singletons : k == 0
→ ∞-Singletons
pr1 (∞-singletons q x) = pr1 (singletons x)
pr2 (∞-singletons q x) y =
equivalence-reasoning
y ∈ _
≃ type-trunc (minus-one n) (x == y) by pr2 (singletons x) y
≃ x == y by inv-equiv (equiv-unit-trunc
(Id-Truncated-Type
(V ,
tr (λ l → is-trunc (to-𝕋 l) V)
(p ∙ (ap (add-ℕ' n) q ∙ left-unit-law-add-ℕ n))
is-trunc-V)
x y))
∈-unordered-pairs : {n' : ℕ}
→ (tup-bool : [ n' ]-UnorderedTupling (raise-bool i))
→ (x y z : V)
→ (z ∈ pr1 (tup-bool ((if_then x else y) ∘ map-inv-raise)))
≃ type-trunc (minus-one n') ((x == z) + (y == z))
∈-unordered-pairs {n'} tup-bool x y z =
equivalence-reasoning
z ∈ _
≃ type-trunc (minus-one n')
(Σ (raise-bool i) (λ b → (if (map-inv-raise b) then x else y) == z)) by pr2 (tup-bool ((if_then x else y) ∘ map-inv-raise)) z
≃ type-trunc (minus-one n')
(Σ bool (λ b → (if b then x else y) == z)) by equiv-trunc (minus-one n')
(equiv-Σ-equiv-base
(λ b → (if b then x else y) == z)
(inv-equiv (compute-raise i bool)))
≃ type-trunc (minus-one n') ((x == z) + (y == z)) by equiv-trunc (minus-one n')
(equiv-Σ-bool-coprod
(λ b → (if b then x else y) == z))
unordered-pairs : [ n ]-UnorderedPairs
pr1 (unordered-pairs x y) = pr1 (n-unordered-tupling (raise-bool i) ((if_then x else y) ∘ map-inv-raise))
pr2 (unordered-pairs x y) = ∈-unordered-pairs (n-unordered-tupling (raise-bool i)) x y
unordered-pairs' : is-set V
→ 0-UnorderedTupling (raise-bool i)
→ UnorderedPairs'
pr1 (unordered-pairs' is-set-V tup-bool x y) = pr1 (tup-bool ((if_then x else y) ∘ map-inv-raise))
pr2 (unordered-pairs' is-set-V tup-bool x y) x≠y z =
equivalence-reasoning
z ∈ _
≃ type-trunc-Prop ((x == z) + (y == z)) by ∈-unordered-pairs tup-bool x y z
≃ (x == z) + (y == z) by inv-equiv (equiv-unit-trunc
(coprod-Prop
(Id-Prop (V , is-set-V) x z)
(Id-Prop (V , is-set-V) y z)
(λ x=z y=z → x≠y (x=z ∙ inv y=z))))
∞-unordered-pairs : {n' : ℕ}
→ is-trunc (to-𝕋 (succ-ℕ n')) V
→ [ succ-ℕ n' ]-UnorderedTupling (raise-bool i)
→ ∞-UnorderedPairs
pr1 (∞-unordered-pairs is-trunc-V tup-bool x y) = pr1 (tup-bool ((if_then x else y) ∘ map-inv-raise))
pr2 (∞-unordered-pairs {n'} is-trunc-V' tup-bool x y) z =
equivalence-reasoning
z ∈ _
≃ type-trunc (to-𝕋 n') ((x == z) + (y == z)) by ∈-unordered-pairs tup-bool x y z
≃ (x == z) + (y == z) by inv-equiv (equiv-unit-trunc
((x == z) + (y == z) ,
is-trunc-coprod (minus-two n')
(is-trunc-V' x z)
(is-trunc-V' y z)))
open e-structure.core.ordered-pairing-structure V
open e-structure.core.trunc-sets ∈-structure-V
open import fixed-point.empty-set m V fixed-point-V
module ordered-pairs-from-k=0 (q : k == 0) where
ordered-pairs : OrderedPairs
ordered-pairs =
ordered-pairs-from-level
n
(tr ∈-str-has-level (p ∙ ap (add-ℕ' n) q ∙ left-unit-law-add-ℕ n) (λ x y → is-trunc-∈ {x} {y}))
empty-set
singletons
unordered-pairs where
open ordered-pairs
open ordered-pairing-structure.notation V ordered-pairs public