functor.slice

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

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.slice
open import foundation.structure-identity-principle
open import foundation.univalence
open import foundation.universe-levels

open import notation

module functor.slice where

T∞ : ∀ i {j} → UU j → UU (lsuc i ⊔ j)
T∞ = Slice

module _ {i j} {A : UU j} where

  infix 100 _==T∞_

  _==T∞_ : T∞ i A → T∞ i A → UU (i ⊔ j)
  (X , f) ==T∞ (Y , g)  =
    Σ (X ≃ Y) (λ e → f ~ (g ∘ (map-equiv e)))

  equiv-eq-T∞ : (s t : T∞ i A) → s == t ≃ s ==T∞ t
  equiv-eq-T∞ (X , f) =
    extensionality-Σ
      (λ g e → f ~ (g ∘ (map-equiv e)))
      (id-equiv)
      (refl-htpy)
      (λ Y → equiv-univalence)
      (λ f' → equiv-funext)

  _==T∞'_ : T∞ i A → T∞ i A → UU (i ⊔ j)
  (X , f) ==T∞' (Y , g)  =
    (z : A) → fiber f z ≃ fiber g z

  equiv-eq-T∞' : (s t : T∞ i A) → s == t ≃ s ==T∞' t
  equiv-eq-T∞' (X , f) (Y , g) =
    equiv-fam-equiv-equiv-slice f g
    ∘e equiv-eq-T∞ (X , f) (Y , g)

T∞-Coalg : ∀ i j → UU (lsuc j ⊔ lsuc i)
T∞-Coalg i j = Σ (UU j) (λ X → X → T∞ i X)

map-T∞ : ∀ {i j k}
      → {A : UU j}
      → {B : UU k}
      → (A → B)
      → (T∞ i A → T∞ i B)
pr1 (map-T∞ f U) = ¦ U ¦
pr2 (map-T∞ f U) = f ∘ (U ↓)