{-# OPTIONS --without-K #-}
open import elementary-number-theory.natural-numbers
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.commuting-triangles-of-maps
open import foundation.constant-type-families
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equality-cartesian-product-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.postcomposition-functions
open import foundation.propositional-maps
open import foundation.propositions
open import foundation.slice
open import foundation.subtypes
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)
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-function-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.unique-existence
open import foundation.univalence
open import foundation.universal-property-dependent-pair-types
open import foundation.universal-property-equivalences
open import foundation.universe-levels
open import e-structure.core
open import notation
module e-structure.property.exponentiation
{i j} (((M , _∈_) , p) : ∈-structure i j)
(ordered-pairs : (M × M) ↪ M) where
open ordered-pairing-structure.notation M ordered-pairs
Operation : M → M → M → UU (i ⊔ j)
Operation a b f =
(((x : M) → (x ∈ a) ≃ Σ M (λ y → ⟨ x , y ⟩ ∈ f)) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → y ∈ b)) ×
((u : M) → u ∈ f → Σ M (λ x → Σ M (λ y → ⟨ x , y ⟩ == u)))
Exponentiation : UU (i ⊔ j)
Exponentiation = (a b : M) → Σ M λ a⇒b → (f : M) → (f ∈ a⇒b) ≃ Operation a b f
open elements (M , _∈_)
Operation' : M → M → M → UU (i ⊔ j)
Operation' a b f =
Σ (El a → El b) (λ ϕ →
(u : M) → (u ∈ f) ≃ Σ (El a) (λ (x , p) → ⟨ x , pr1 (ϕ (x , p)) ⟩ == u))
Exponentiation' : UU (i ⊔ j)
Exponentiation' = (a b : M) → Σ M λ a⇒b → (f : M) → (f ∈ a⇒b) ≃ Operation' a b f
Operation≃Operation' : (a b f : M)
→ Operation a b f ≃ Operation' a b f
Operation≃Operation' a b f =
equivalence-reasoning
Operation a b f
≃ ((u : M) → u ∈ f → Σ M (λ x → Σ M (λ y → ⟨ x , y ⟩ == u))) ×
(((x : M) → (x ∈ a) ≃ Σ M (λ y → ⟨ x , y ⟩ ∈ f)) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → y ∈ b)) by commutative-prod
≃ ((u : M) → u ∈ f → Σ (M × M) (λ (x , y) → ⟨ x , y ⟩ == u)) ×
(((x : M) → fiber {A = El a} pr1 x ≃ fiber {A = pairs-∈-f} (pr1 ∘ pr1) x) ×
((y : M) → fiber {A = pairs-∈-f} (pr2 ∘ pr1) y → fiber {A = El b} pr1 y)) by equiv-prod
(equiv-Π-equiv-family (λ u → equiv-Π-equiv-family (λ _ → inv-associative-Σ _ _ _)))
(equiv-prod
(equiv-Π-equiv-family (λ x →
equiv-postcomp-equiv
(inv-compute-fiber-comp pr1 pr1 x ∘e
equiv-Σ _
(inv-equiv-fiber-pr1 (λ _ → M) x)
(λ y → inv-equiv-fiber-pr1 (λ (x' , y') → ⟨ x' , y' ⟩ ∈ f) (x , y)))
(fiber pr1 x) ∘e
equiv-precomp-equiv (equiv-fiber-pr1 (_∈ a) x ) (Σ M (λ y → ⟨ x , y ⟩ ∈ f))))
(equiv-Π-equiv-family (λ y →
equiv-postcomp (fiber (pr2 ∘ pr1) y) (inv-equiv-fiber-pr1 (_∈ b) y) ∘e
equiv-precomp
(equiv-Σ _
(equiv-fiber-pr1 (λ _ → M) y ∘e
equiv-Σ-equiv-base (λ (y' , x') → y' == y) commutative-prod)
(λ t → equiv-eq (ap-binary
(λ x y' → ⟨ x , y' ⟩ ∈ f)
(inv (tr-constant-type-family (pr2 t) (pr1 (pr1 t))))
(pr2 t)) ∘e
equiv-fiber-pr1 (λ (x , y') → ⟨ x , y' ⟩ ∈ f) (pr1 t)) ∘e
compute-fiber-comp pr2 pr1 y)
(y ∈ b)) ∘e
(equiv-Π-equiv-family (λ y → inv-equiv equiv-ev-pair) ∘e
equiv-swap-Π)))
≃ ((s : El f) → Σ (M × M) (λ (x , y) → ⟨ x , y ⟩ == pr1 s)) ×
(Σ (El a ≃ pairs-∈-f) (λ α → pr1 ~ (pr1 ∘ (pr1 ∘ map-equiv α))) ×
Σ (pairs-∈-f → El b) (λ β → (pr2 ∘ pr1) ~ (pr1 ∘ β))) by equiv-prod
(inv-equiv equiv-ev-pair)
(equiv-prod
(inv-equiv (equiv-fam-equiv-equiv-slice pr1 (pr1 ∘ pr1)))
(equiv-hom-slice-fiberwise-hom (pr2 ∘ pr1) pr1))
≃ Σ ((s : El f) → Σ (M × M) (λ (x , y) → ⟨ x , y ⟩ == pr1 s)) (λ γ →
Σ (El a ≃ El f) (λ α → pr1 ~ (pr1 ∘ (pr1 ∘ (γ ∘ map-equiv α)))) ×
Σ (El f → El b) (λ β →
(pr2 ∘ pr1) ~
(pr1 ∘ (β ∘ (λ ((x , y) , ⟨x,y⟩∈f) → (⟨ x , y ⟩ , ⟨x,y⟩∈f)))))) by inv-equiv (equiv-tot (λ γ →
equiv-prod
(equiv-Σ-equiv-base
(λ α → pr1 ~ (pr1 ∘ (pr1 ∘ map-equiv α)))
(equiv-postcomp-equiv
(inv-equiv (equiv-Σ-emb-base ordered-pairs γ))
(El a)))
(equiv-Σ-equiv-base
(λ β → (pr2 ∘ pr1) ~ (pr1 ∘ β))
(equiv-precomp (equiv-Σ-emb-base ordered-pairs γ) (El b)))))
≃ Σ ((s : El f) → Σ (M × M) (λ (x , y) → ⟨ x , y ⟩ == pr1 s)) (λ γ →
Σ (El a ≃ El f) (λ α → (pr1 ∘ map-inv-equiv α) ~ (pr1 ∘ (pr1 ∘ γ))) ×
Σ (El f → El b) (λ β → (pr1 ∘ β) ~ (pr2 ∘ (pr1 ∘ γ)))) by equiv-tot (λ γ → equiv-prod
(equiv-tot (λ α →
equiv-inv-htpy _ _ ∘e
equiv-coherence-triangle-maps-inv-top
pr1
(pr1 ∘ (pr1 ∘ γ))
α))
(equiv-tot (λ β →
equiv-coherence-triangle-maps-inv-top
(pr2 ∘ pr1)
(pr1 ∘ β)
(equiv-Σ-emb-base ordered-pairs γ))))
≃ Σ (El a ≃ El f) (λ α →
Σ (El f → El b) (λ β →
Σ ((s : El f) → Σ (M × M) (λ (x , y) → ⟨ x , y ⟩ == pr1 s)) (λ γ →
((pr1 ∘ map-inv-equiv α) ~ (pr1 ∘ (pr1 ∘ γ))) ×
((pr1 ∘ β) ~ (pr2 ∘ (pr1 ∘ γ)))))) by ((((equiv-tot (λ α → equiv-tot (λ β → associative-Σ _ _ _)) ∘e
equiv-tot (λ α → equiv-left-swap-Σ)) ∘e
associative-Σ _ _ _) ∘e
equiv-Σ-equiv-base
(λ (α , (γ , p)) → Σ (El f → El b) (λ β → (pr1 ∘ β) ~ (pr2 ∘ (pr1 ∘ γ))))
equiv-left-swap-Σ) ∘e
inv-associative-Σ _ _ _)
≃ Σ (El a ≃ El f) (λ α →
Σ (El f → El b) (λ β →
(s : El f) →
Σ (Σ (M × M) (λ (x , y) → ⟨ x , y ⟩ == pr1 s))
(λ t → (pr1 (map-inv-equiv α s) == pr1 (pr1 t)) ×
(pr1 (β s) == pr2 (pr1 t))))) by equiv-tot (λ α → equiv-tot λ β →
inv-distributive-Π-Σ ∘e
equiv-tot (λ γ → inv-distributive-Π-Σ))
≃ Σ (El a ≃ El f) (λ α →
Σ (El f → El b) (λ β →
(s : El f) → ⟨ pr1 (map-inv-equiv α s) , pr1 (β s) ⟩ == pr1 s)) by equiv-tot (λ α → equiv-tot (λ β → equiv-Π-equiv-family (λ s →
left-unit-law-Σ-is-contr
(is-torsorial-path (pr1 (map-inv-equiv α s) , pr1 (β s)))
((pr1 (map-inv-equiv α s) , pr1 (β s)) , refl) ∘e
(equiv-right-swap-Σ ∘e
equiv-tot (λ t → equiv-eq-pair _ _)))))
≃ Σ (El a → El b) (λ β →
Σ (El f ≃ El a) (λ α →
(s : El f) →
pr1 s == ⟨ pr1 (map-equiv α s) , pr1 (β (map-equiv α s)) ⟩)) by (equiv-left-swap-Σ ∘e
equiv-Σ _
equiv-inv-equiv
(λ α → equiv-Σ _
(equiv-precomp α (El b))
(λ β → equiv-Π-equiv-family (λ s →
equiv-concat' (pr1 s)
(ap (λ x → ⟨ pr1 (map-inv-equiv α s) , pr1 (β x) ⟩)
(inv (is-section-map-inv-equiv α s))) ∘e
equiv-inv _ _))))
≃ Σ (El a → El b) (λ ϕ →
(u : M) →
fiber {A = El f} pr1 u ≃
fiber {A = El a} (λ t → ⟨ pr1 t , pr1 (ϕ t) ⟩) u) by equiv-tot (λ β →
equiv-fam-equiv-equiv-slice
(pr1)
(λ t → ⟨ pr1 t , pr1 (β t) ⟩))
≃ Operation' a b f by equiv-tot (λ ϕ → equiv-Π-equiv-family (λ u →
equiv-precomp-equiv
(inv-equiv-fiber-pr1 (_∈ f) u)
(fiber (λ t → ⟨ pr1 t , pr1 (ϕ t) ⟩) u)))
where
pairs-∈-f : UU (i ⊔ j)
pairs-∈-f = Σ (M × M) λ (x , y) → ⟨ x , y ⟩ ∈ f
Exponentiation≃Exponentiation' : Exponentiation ≃ Exponentiation'
Exponentiation≃Exponentiation' =
equiv-Π-equiv-family (λ a →
equiv-Π-equiv-family (λ b →
equiv-tot (λ a⇒b →
equiv-Π-equiv-family (λ f →
equiv-postcomp-equiv
(Operation≃Operation' a b f)
(f ∈ a⇒b)))))
open mere-sets ((M , _∈_) , p)
Operation-mere-sets : M → M → M → UU (i ⊔ j)
Operation-mere-sets a b f =
(((x : M) → (x ∈ a) → ∃! M (λ y → ⟨ x , y ⟩ ∈ f)) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → (x ∈ a) × (y ∈ b))) ×
((u : M) → u ∈ f → Σ M (λ x → Σ M (λ y → ⟨ x , y ⟩ == u)))
is-prop-Operation-mere-sets : (a b f : M)
→ mere-set a
→ mere-set b
→ is-prop (Operation-mere-sets a b f)
is-prop-Operation-mere-sets a b f mere-set-a mere-set-b =
is-prop-prod
(is-prop-prod
(is-prop-Π (λ x → is-prop-function-type is-property-is-contr))
(is-prop-Π (λ x → is-prop-Π (λ y → is-prop-function-type (is-prop-prod (mere-set-a x) (mere-set-b y))))))
(is-prop-Π (λ u → is-prop-function-type (is-prop-equiv (inv-associative-Σ _ _ _) (is-prop-map-emb ordered-pairs u))))
Operation≃Operation-mere-sets : (a b f : M)
→ mere-set a
→ Operation a b f ≃ Operation-mere-sets a b f
Operation≃Operation-mere-sets a b f mere-set-a = equiv-prod α id-equiv
where
α : (((x : M) → (x ∈ a) ≃ Σ M (λ y → ⟨ x , y ⟩ ∈ f)) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → y ∈ b))
≃ (((x : M) → (x ∈ a) → ∃! M (λ y → ⟨ x , y ⟩ ∈ f)) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → (x ∈ a) × (y ∈ b)))
α =
equivalence-reasoning
(((x : M) → (x ∈ a) ≃ Σ M (λ y → ⟨ x , y ⟩ ∈ f)) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → y ∈ b))
≃ ((x : M) →
Σ (Σ M (λ y → ⟨ x , y ⟩ ∈ f) → x ∈ a) (λ ϕ →
(p : x ∈ a) →
∃! (Σ M (λ y → ⟨ x , y ⟩ ∈ f)) (λ s → ϕ s == p))) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → y ∈ b) by equiv-prod
(equiv-Π-equiv-family (λ x →
equiv-tot (λ ϕ → equiv-is-contr-map-is-equiv ϕ) ∘e
equiv-inv-equiv))
id-equiv
≃ ((x : M) →
(Σ M (λ y → ⟨ x , y ⟩ ∈ f) → x ∈ a) ×
(x ∈ a → ∃! M (λ y → ⟨ x , y ⟩ ∈ f))) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → y ∈ b) by equiv-prod
(equiv-Π-equiv-family (λ x →
equiv-tot (λ ϕ →
equiv-Π-equiv-family (λ p →
equiv-is-contr-equiv
(right-unit-law-Σ-is-contr
(λ s → mere-set-a x (ϕ s) p))))))
id-equiv
≃ (((x : M) → (x ∈ a) → ∃! M (λ y → ⟨ x , y ⟩ ∈ f)) ×
((x y : M) → ⟨ x , y ⟩ ∈ f → (x ∈ a) × (y ∈ b))) by (equiv-prod id-equiv
(equiv-Π-equiv-family (λ x →
equiv-Π-equiv-family (λ y → inv-distributive-Π-Σ) ∘e
inv-distributive-Π-Σ) ∘e
(inv-distributive-Π-Σ ∘e
equiv-prod (equiv-Π-equiv-family (λ x → equiv-ev-pair)) id-equiv)) ∘e
(associative-Σ _ _ _ ∘e
equiv-prod (commutative-prod ∘e distributive-Π-Σ) id-equiv))
Exponentiation-mere-sets : UU (i ⊔ j)
Exponentiation-mere-sets = (a b : M) → Σ M λ a⇒b → (f : M) → (f ∈ a⇒b) ≃ Operation-mere-sets a b f
Exponentiation≃Exponentiation-mere-sets : ((x : M) → mere-set x)
→ Exponentiation ≃ Exponentiation-mere-sets
Exponentiation≃Exponentiation-mere-sets p =
equiv-Π-equiv-family (λ a →
equiv-Π-equiv-family (λ b →
equiv-tot (λ a⇒b →
equiv-Π-equiv-family (λ f →
equiv-postcomp-equiv
(Operation≃Operation-mere-sets a b f (p a))
(f ∈ a⇒b)))))
open extensionality ((M , _∈_) , p)
emb-operation'-function : (a b : M)
→ Σ M (Operation' a b) ↪ (El a → El b)
emb-operation'-function a b =
comp-emb
(emb-subtype (λ ϕ →
((Σ M (λ f → (u : M) → (u ∈ f) ≃ Σ (El a) (λ (x , p) → ⟨ x , pr1 (ϕ (x , p)) ⟩ == u))) ,
is-prop-total-space-fixed-∈ (λ u → Σ (El a) (λ (x , p) → ⟨ x , pr1 (ϕ (x , p)) ⟩ == u)))))
(emb-equiv equiv-left-swap-Σ)
open e-structure.core.trunc-sets ((M , _∈_) , p)
open import e-structure.property.replacement ((M , _∈_) , p)
is-equiv-operation'-function-emb : (n : ℕ)
→ ∈-str-has-level n
→ [ n ]-Replacement
→ (a b : M)
→ is-equiv (map-emb (emb-operation'-function a b))
is-equiv-operation'-function-emb n H R a b =
is-equiv-comp
pr1
map-left-swap-Σ
is-equiv-map-left-swap-Σ
(is-equiv-pr1-is-contr (λ ϕ →
is-proof-irrelevant-is-prop
(is-prop-total-space-fixed-∈ (λ u → Σ (El a) (λ x → ⟨ pr1 x , pr1 (ϕ x) ⟩ == u)))
(map-equiv
(equiv-tot (λ f →
equiv-Π-equiv-family (λ u →
equiv-postcomp-equiv
(inv-equiv
(equiv-unit-trunc
(Σ (El a) (λ x → ⟨ pr1 x , pr1 (ϕ x) ⟩ == u) ,
is-trunc-equiv (minus-one n)
(Σ (Σ (El a × El b) (λ (x , y) → ⟨ pr1 x , pr1 y ⟩ == u))
(λ ((x , y) , _) → ϕ x == y))
(α ϕ u)
(is-trunc-Σ
(is-trunc-map-comp (minus-one n)
(map-emb ordered-pairs)
(λ (x , y) → pr1 x , pr1 y)
(is-trunc-map-is-prop-map (minus-two n)
(is-prop-map-emb ordered-pairs))
(is-trunc-map-map-Σ (minus-one n) _
(is-trunc-map-pr1 (minus-one n) (H a))
(λ _ → is-trunc-map-pr1 (minus-one n) (H b)))
u)
λ ((x , y) , _) →
is-trunc-Σ
(is-trunc-∈-str-carrier n H)
(λ z → is-trunc-succ-is-trunc (minus-one n) (H b z))
(ϕ x)
y))))
(u ∈ f))))
(R a (λ (x , p) → ⟨ x , pr1 (ϕ (x , p)) ⟩)))))
where
α : (ϕ : El a → El b) (u : M)
→ Σ (El a) (λ x → ⟨ pr1 x , pr1 (ϕ x) ⟩ == u)
≃ Σ (Σ (El a × El b) (λ (x , y) → ⟨ pr1 x , pr1 y ⟩ == u))
(λ ((x , y) , _) → ϕ x == y)
α ϕ u =
equivalence-reasoning
Σ (El a) (λ x → ⟨ pr1 x , pr1 (ϕ x) ⟩ == u)
≃ Σ (El a) (λ x →
Σ (Σ (El b) (λ y → ϕ x == y))
(λ (y , _) → ⟨ pr1 x , pr1 y ⟩ == u)) by equiv-tot (λ x →
inv-left-unit-law-Σ-is-contr
(is-torsorial-path (ϕ x))
(ϕ x , refl))
≃ Σ (El a) (λ x →
Σ (El b) (λ y →
(ϕ x == y)
× (⟨ pr1 x , pr1 y ⟩ == u))) by equiv-tot (λ x → associative-Σ _ _ _)
≃ Σ (El a) (λ x →
Σ (El b) (λ y →
(⟨ pr1 x , pr1 y ⟩ == u)
× (ϕ x == y))) by equiv-tot (λ x →
equiv-tot (λ y →
commutative-prod))
≃ Σ (El a × El b)
(λ (x , y) →
(⟨ pr1 x , pr1 y ⟩ == u)
× (ϕ x == y)) by inv-associative-Σ _ _ _
≃ Σ (Σ (El a × El b)
(λ (x , y) → ⟨ pr1 x , pr1 y ⟩ == u))
(λ ((x , y) , _) → ϕ x == y) by inv-associative-Σ _ _ _