{-# OPTIONS --without-K --rewriting #-}
open import elementary-number-theory.natural-numbers
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.embeddings
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.homotopies
open import foundation.identity-types
open import foundation.locally-small-types
open import foundation.slice
open import foundation.structure-identity-principle
open import foundation.subtypes
open import foundation.truncated-maps
open import foundation.truncated-types
open import foundation.truncation-levels
renaming (truncation-level-minus-one-ℕ to minus-one;
truncation-level-ℕ to to-𝕋)
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.univalence
open import foundation.universe-levels
open import foundation.whiskering-homotopies
open import functor.slice
open import image-factorisation
open import notation
module functor.n-slice where
T-[_] : (n : ℕ) (i : Level) {j : Level} → UU j → UU (lsuc i ⊔ j)
T-[ n ] i X = Σ (UU i) (λ A → trunc-map (minus-one n) A X)
T⁰ : (i : Level) {j : Level} → UU j → UU (lsuc i ⊔ j)
T⁰ = T-[ 0 ]
T¹ : (i : Level) {j : Level} → UU j → UU (lsuc i ⊔ j)
T¹ = T-[ 1 ]
module _ {i j} {A : UU j} where
Eq-T : (n : ℕ) → T-[ n ] i A → T-[ n ] i A → UU (i ⊔ j)
Eq-T n (X , f) (Y , g) =
Σ (X ≃ Y) (λ e → map-trunc-map f ~ (map-trunc-map g ∘ map-equiv e))
syntax Eq-T n s t = s ==T-[ n ] t
equiv-eq-T-[_] : (n : ℕ) (s t : T-[ n ] i A) → s == t ≃ (s ==T-[ n ] t)
equiv-eq-T-[ n ] (X , f) =
extensionality-Σ
(λ g e → map-trunc-map f ~ (map-trunc-map g ∘ map-equiv e))
(id-equiv)
(refl-htpy)
(λ Y → equiv-univalence)
(λ f' → equiv-funext ∘e extensionality-type-subtype' (is-trunc-map-Prop (minus-one n)) f f')
Eq'-T : (n : ℕ) → T-[ n ] i A → T-[ n ] i A → UU (i ⊔ j)
Eq'-T n (X , f) (Y , g) =
(z : A) → fiber (map-trunc-map f) z ≃ fiber (map-trunc-map g) z
syntax Eq'-T n s t = s ==T-[ n ]' t
equiv-eq-T-[_]' : (n : ℕ) (s t : T-[ n ] i A) → s == t ≃ (s ==T-[ n ]' t)
equiv-eq-T-[ n ]' (X , f) (Y , g) =
equiv-fam-equiv-equiv-slice (map-trunc-map f) (map-trunc-map g)
∘e equiv-eq-T-[ n ] (X , f) (Y , g)
is-trunc-T-[_] : (n : ℕ) → is-trunc (to-𝕋 n) (T-[ n ] i A)
is-trunc-T-[ n ] (X , f) (Y , g) =
is-trunc-equiv (minus-one n) _
(equiv-eq-T-[ n ]' (X , f) (Y , g))
(is-trunc-Π _ (λ z → is-trunc-equiv-is-trunc _ (pr2 f z) (pr2 g z)))
map-T-[_] : (n : ℕ)
→ {i j k : Level}
→ {A : UU j}
→ {B : UU k}
→ is-[ succ-ℕ n ]-small i B
→ (A → B)
→ (T-[ n ] i A → T-[ n ] i B)
pr1 (map-T-[ n ] {i = i} {B = B} p f s) = trunc-Image p (f ∘ map-trunc-map (s ↓))
pr2 (map-T-[ n ] {i = i} {B = B} p f s) = trunc-image-inclusion p (f ∘ map-trunc-map (s ↓))
map-T-[_]-~ : (n : ℕ)
→ {i j j' : Level}
→ {X : UU j}
→ {Y : UU j'}
→ (p : is-[ succ-ℕ n ]-small i Y)
→ (φ ψ : X → Y)
→ (φ ~ ψ)
→ map-T-[ n ] p φ ~ map-T-[ n ] p ψ
map-T-[ n ]-~ p φ ψ σ (A , f) =
ap (λ h → map-T-[ n ] p h (A , f)) (eq-htpy σ)
emb-forget-T-[_]-to-T∞ : (n : ℕ)
→ {i j : Level}
→ (X : UU j)
→ T-[ n ] i X ↪ T∞ i X
emb-forget-T-[ n ]-to-T∞ X =
comp-emb
(emb-subtype (λ s → is-trunc-map-Prop (minus-one n) (pr2 s)))
(emb-equiv (inv-associative-Σ _ _ _))
map-T-[_]-~-refl : (n : ℕ)
→ {i j j' : Level}
→ {X : UU j}
→ {Y : UU j'}
→ (p : is-[ succ-ℕ n ]-small i Y)
→ (φ : X → Y)
→ map-T-[ n ]-~ p φ φ refl-htpy ~ refl-htpy
map-T-[ n ]-~-refl p φ (A , f) =
ap (ap (λ h → map-T-[ n ] p h (A , f))) (eq-htpy-refl-htpy φ)
map-T⁰ : ∀ {i j k}
→ {A : UU j}
→ {B : UU k}
→ is-locally-small i B
→ (A → B)
→ (T⁰ i A → T⁰ i B)
map-T⁰ = map-T-[ 0 ]
map-T¹ : ∀ {i j k}
→ {A : UU j}
→ {B : UU k}
→ is-[ 2 ]-small i B
→ (A → B)
→ (T¹ i A → T¹ i B)
map-T¹ = map-T-[ 1 ]
T-[_]-Coalg : ℕ → (i j : Level) → UU (lsuc i ⊔ lsuc j)
T-[ n ]-Coalg i j = Σ (UU j) (λ X → X → T-[ n ] i X)
T⁰-Coalg : ∀ i j → UU (lsuc i ⊔ lsuc j)
T⁰-Coalg = T-[ 0 ]-Coalg
T¹-Coalg : ∀ i j → UU (lsuc i ⊔ lsuc j)
T¹-Coalg = T-[ 1 ]-Coalg
T-[_]-to-T∞-Coalg : (n : ℕ)
→ {i j : Level}
→ T-[ n ]-Coalg i j
→ T∞-Coalg i j
pr1 (T-[ n ]-to-T∞-Coalg X) = ¦ X ¦
pr2 (T-[ n ]-to-T∞-Coalg X) =
map-emb (emb-forget-T-[ n ]-to-T∞ ¦ X ¦) ∘ (X ↓)
T-[_]-Alg : ℕ → (i j : Level) → UU (lsuc i ⊔ lsuc j)
T-[ n ]-Alg i j = Σ (UU j) (λ X → T-[ n ] i X → X)
T⁰-Alg : ∀ i j → UU (lsuc i ⊔ lsuc j)
T⁰-Alg = T-[ 0 ]-Alg
T¹-Alg : ∀ i j → UU (lsuc i ⊔ lsuc j)
T¹-Alg = T-[ 1 ]-Alg
hom-T-[_]-Alg : (n : ℕ)
→ {i j j' : Level}
→ (X : T-[ n ]-Alg i j) (Y : T-[ n ]-Alg i j')
→ is-[ succ-ℕ n ]-small i ¦ Y ¦
→ UU (lsuc i ⊔ j ⊔ j')
hom-T-[ n ]-Alg {i} X Y p =
Σ (¦ X ¦ → ¦ Y ¦) (λ f →
(f ∘ X ↓) ~ (Y ↓ ∘ map-T-[ n ] p f))
hom-T-[_]-Alg-Eq : (n : ℕ)
→ {i j j' : Level}
→ (X : T-[ n ]-Alg i j) (Y : T-[ n ]-Alg i j')
→ (p : is-[ succ-ℕ n ]-small i ¦ Y ¦)
→ hom-T-[ n ]-Alg X Y p
→ hom-T-[ n ]-Alg X Y p
→ UU (lsuc i ⊔ j ⊔ j')
hom-T-[ n ]-Alg-Eq X Y p (φ , α) (ψ , β) =
Σ (φ ~ ψ) λ σ →
(α ∙h ((Y ↓) ·l map-T-[ n ]-~ p φ ψ σ)) ~
((σ ·r (X ↓)) ∙h β)
equiv-hom-T-[_]-Alg-Eq : (n : ℕ)
→ {i j j' : Level}
→ {X : T-[ n ]-Alg i j} {Y : T-[ n ]-Alg i j'}
→ (p : is-[ succ-ℕ n ]-small i ¦ Y ¦)
→ (φ ψ : hom-T-[ n ]-Alg X Y p)
→ (φ == ψ)
≃ hom-T-[ n ]-Alg-Eq X Y p φ ψ
equiv-hom-T-[ n ]-Alg-Eq {X = X} {Y = Y} p (φ , α) =
extensionality-Σ
(λ {ψ} β σ → (α ∙h ((Y ↓) ·l map-T-[ n ]-~ p φ ψ σ)) ~ ((σ ·r (X ↓)) ∙h β))
(refl-htpy)
(λ (A , f) → H A f)
(λ _ → equiv-funext)
(λ α' →
equiv-Π-equiv-family (λ (A , f) → equiv-concat (H A f) (α' (A , f))) ∘e
equiv-funext)
where
H : ∀ A f
→ (α ∙h ((Y ↓) ·l map-T-[ n ]-~ p φ φ refl-htpy)) (A , f) == α (A , f)
H A f =
ap (λ q → α (A , f) ∙ ap (Y ↓) q) (map-T-[ n ]-~-refl p φ (A , f)) ∙
right-unit
hom-T-[_]-Alg-eq : (n : ℕ)
→ {i j j' : Level}
→ {X : T-[ n ]-Alg i j} {Y : T-[ n ]-Alg i j'}
→ (p : is-[ succ-ℕ n ]-small i ¦ Y ¦)
→ (φ ψ : hom-T-[ n ]-Alg X Y p)
→ hom-T-[ n ]-Alg-Eq X Y p φ ψ
→ φ == ψ
hom-T-[ n ]-Alg-eq p φ ψ = map-inv-equiv (equiv-hom-T-[ n ]-Alg-Eq p φ ψ)