{-# OPTIONS --without-K --rewriting #-}

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.fibers-of-maps
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-truncation
open import foundation.identity-types
open import foundation.locally-small-types
open import foundation.truncated-maps
open import foundation.truncations
open import foundation.truncation-levels
  renaming (truncation-level-minus-one-ℕ to minus-one)
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.univalence
open import foundation.universe-levels

open import functor.n-slice
open import image-factorisation
open import notation as N hiding (sup)

module fixed-point.union {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

-- Construction of ∈-structure on V
open import fixed-point.core m V fixed-point-V

-- Property of having unions
open import e-structure.property.union ∈-structure-V

⋃ : V → V
⋃ x =
  let (A , f) = desup x in
  sup
    (trunc-Image
      {Domain = Σ A (λ a → ¦ desup (f 〈 a 〉) ¦)}
      is-n+1-small-V
      (λ (a , b) → (desup (f 〈 a 〉) ↓) 〈 b 〉) ,
    trunc-image-inclusion-eq-add-ℕ' k (succ-ℕ m) (ap succ-ℕ p) is-n+1-small-V _)


∈-union : (x z : V)
        → (z ∈ ⋃ x)
        ≃ type-trunc (minus-one n) (Σ V λ y → (z ∈ y) × (y ∈ x))
∈-union x z =
  let (A , f) = desup x in
  equivalence-reasoning
    z ∈ ⋃ x
      ≃ fiber (map-trunc-map
              (trunc-image-inclusion-add-ℕ' k
                is-n+1-small-V
                λ (a , b) → (desup (f 〈 a 〉) ↓) 〈 b 〉))
            z                                                   by equiv-eq (∈-sup z)
      ≃ type-trunc (minus-one n)
          (fiber (λ (a , b) → (desup (f 〈 a 〉) ↓) 〈 b 〉) z)         by equiv-fiber-trunc-Image-im is-n+1-small-V _ z
      ≃ type-trunc (minus-one n) (Σ A (λ a → z ∈ f 〈 a 〉))       by equiv-trunc (minus-one n) (associative-Σ _ _ _)
      ≃ type-trunc (minus-one n) (Σ (El x) (λ (y , _) → z ∈ y)) by equiv-trunc (minus-one n)
                                                                     (equiv-Σ-equiv-base
                                                                       (λ (y , _) → z ∈ y)
                                                                       (inv-equiv-total-fiber (map-trunc-map f)))
      ≃ type-trunc (minus-one n) (Σ V λ y → (z ∈ y) × (y ∈ x))  by equiv-trunc (minus-one n)
                                                                     (equiv-tot (λ _ → commutative-prod) ∘e associative-Σ _ _ _)

n-union : [ n ]-Union
n-union x = (⋃ x , ∈-union x)

-- Since V has unordered pairs, it has binary unions
open import fixed-point.unordered-tupling m n k p V fixed-point-V is-n+1-small-V

open binary.from-unordered-pairs n-union unordered-pairs public