{-# OPTIONS --without-K --rewriting #-}
open import elementary-number-theory.natural-numbers
open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.function-extensionality
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.propositional-maps
open import foundation.propositions
open import foundation.slice
open import foundation.small-types
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)
open import foundation.type-arithmetic-dependent-function-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
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 e-structure.u-like
open import notation
module e-structure.internalisations
{i j} (((M , _∈_) , p) : ∈-structure i j) where
open elements (M , _∈_)
open extensionality ((M , _∈_) , p)
open trunc-sets ((M , _∈_) , p)
open mere-sets ((M , _∈_) , p)
open import e-structure.property.replacement ((M , _∈_) , p)
InternalisationOfType : {k : Level} → UU k → UU (i ⊔ j ⊔ k)
InternalisationOfType A = Σ M (λ a → El a ≃ A)
Representation : {k : Level} → UU k → UU (i ⊔ k)
Representation A = A → M
InternalisationOfRepr : {k : Level} {A : UU k}
→ Representation A → UU (i ⊔ j ⊔ k)
InternalisationOfRepr f = Σ M (λ a → (z : M) → (z ∈ a) ≃ fiber f z)
equiv-El-repr-domain : {k : Level} {A : UU k}
→ {f : Representation A}
→ (a : InternalisationOfRepr f)
→ El (pr1 a) ≃ A
equiv-El-repr-domain {A = A} {f = f} a =
equivalence-reasoning
El (pr1 a)
≃ Σ M (fiber f) by equiv-tot (pr2 a)
≃ A by equiv-total-fiber f
is-prop-InternalisationOfRepr : {k : Level} {A : UU k}
→ (f : Representation A)
→ is-prop (InternalisationOfRepr f)
is-prop-InternalisationOfRepr f = is-prop-total-space-fixed-∈ (fiber f)
equiv-IntOfRepr-IntOfType : {k : Level} (A : UU k)
→ Σ (Representation A) InternalisationOfRepr
≃ InternalisationOfType A
equiv-IntOfRepr-IntOfType A =
equivalence-reasoning
Σ (Representation A) InternalisationOfRepr
≃ Σ M (λ a →
Σ (Representation A) (λ f →
(z : M) → (z ∈ a) ≃ fiber f z)) by equiv-left-swap-Σ
≃ InternalisationOfType A by equiv-tot α
where
α : (a : M)
→ Σ (Representation A) (λ f → (z : M) → (z ∈ a) ≃ fiber f z)
≃ (El a ≃ A)
α a =
equivalence-reasoning
Σ (Representation A) (λ f →
(z : M) → (z ∈ a) ≃ fiber f z)
≃ Σ (Representation A) (λ f →
(z : M) → fiber {A = El a} pr1 z ≃ fiber f z) by equiv-tot (λ f →
equiv-Π-equiv-family (λ z →
equiv-precomp-equiv (equiv-fiber-pr1 (_∈ a) z) _))
≃ Σ (Representation A) (λ f →
Σ (El a ≃ A) (λ e →
pr1 ~ (f ∘ map-equiv e))) by equiv-tot (λ f →
inv-equiv (equiv-fam-equiv-equiv-slice pr1 f))
≃ Σ (Representation A) (λ f →
Σ (El a ≃ A) (λ e →
(pr1 ∘ map-inv-equiv e) ~ f)) by equiv-tot (λ f →
equiv-tot (λ e →
equiv-Π _ e (λ s →
equiv-concat (ap pr1 (is-retraction-map-inv-equiv e s)) _)))
≃ Σ (Representation A) (λ f →
Σ (El a ≃ A) (λ e →
(pr1 ∘ map-inv-equiv e) == f)) by equiv-tot (λ f →
equiv-tot (λ e →
equiv-eq-htpy))
≃ Σ (El a ≃ A) (λ e →
Σ (Representation A) (λ f →
(pr1 ∘ map-inv-equiv e) == f)) by equiv-left-swap-Σ
≃ (El a ≃ A) by equiv-pr1 (λ e →
is-torsorial-path (pr1 ∘ map-inv-equiv e))
is-faithful-Repr : {k : Level} {A : UU k}
→ Representation A → UU (i ⊔ k)
is-faithful-Repr f = is-prop-map f
equiv-is-[_]-type-trunc-repr : (n : ℕ) {k : Level} {A : UU k}
→ {f : Representation A}
→ (a : InternalisationOfRepr f)
→ is-[ n ]-type (pr1 a) ≃ is-trunc-map (minus-one n) f
equiv-is-[ n ]-type-trunc-repr a =
equiv-Π-equiv-family (λ z →
equiv-is-trunc-equiv (minus-one n) (pr2 a z))
equiv-mere-set-faithful-repr : {k : Level} {A : UU k}
→ {f : Representation A}
→ (a : InternalisationOfRepr f)
→ mere-set (pr1 a) ≃ is-faithful-Repr f
equiv-mere-set-faithful-repr = equiv-is-[ zero-ℕ ]-type-trunc-repr
equiv-u-like-int-repr : (k : Level)
→ ((A : UU (i ⊔ j))
→ InternalisationOfType A
→ is-small k A)
≃ (k -like (M , _∈_))
equiv-u-like-int-repr k =
equivalence-reasoning
((A : UU (i ⊔ j)) → InternalisationOfType A → is-small k A)
≃ ((A : UU (i ⊔ j)) (a : M)
→ El a ≃ A → is-small k A) by equiv-Π-equiv-family (λ A → equiv-ev-pair)
≃ ((a : M) (A : UU (i ⊔ j))
→ El a ≃ A → is-small k A) by equiv-swap-Π
≃ ((a : M) (A : UU (i ⊔ j))
→ El a ≃ A → is-small k (El a)) by equiv-Π-equiv-family (λ a →
equiv-Π-equiv-family (λ A →
equiv-Π-equiv-family (λ e →
equiv-is-small-equiv (inv-equiv e))))
≃ ((a : M)
→ Σ (UU (i ⊔ j)) (λ A → El a ≃ A)
→ is-small k (El a)) by equiv-Π-equiv-family (λ a →
inv-equiv equiv-ev-pair)
≃ (k -like (M , _∈_)) by equiv-Π-equiv-family (λ a →
left-unit-law-function-type (is-small k (El a))
∘e equiv-precomp
(inv-equiv
(equiv-unit-is-contr
(is-torsorial-equiv (El a))))
(is-small k (El a)))
int-repr-given-replacement : (n : ℕ)
→ [ n ]-Replacement
→ {k : Level} {A : UU k}
→ InternalisationOfType A
→ (f : Representation A)
→ is-trunc-map (minus-one n) f
→ InternalisationOfRepr f
pr1 (int-repr-given-replacement n R (a , α) f H) =
pr1 (R a (f ∘ map-equiv α))
pr2 (int-repr-given-replacement n R (a , α) f H) z =
equivalence-reasoning
z ∈ pr1 (R a (f ∘ map-equiv α))
≃ type-trunc (minus-one n) (fiber (f ∘ map-equiv α) z) by pr2 (R a (f ∘ map-equiv α)) z
≃ fiber (f ∘ map-equiv α) z by inv-equiv (equiv-unit-trunc (_ ,
is-trunc-map-comp (minus-one n) f (map-equiv α)
H
(is-trunc-map-is-equiv (minus-one n) (is-equiv-map-equiv α))
z))
≃ fiber f z by equiv-Σ-equiv-base (λ x → f x == z) α