replacement.agda

open import 1Lab.Prelude

module wip.replacement where

module
  Replacement
    {ℓₐ ℓₜ ℓᵢ} {A : Type ℓₐ} {T : Type ℓₜ}
    {R : T → T → Type ℓᵢ} {rr : ∀ x → R x x}
    (locally-small : is-identity-system R rr)
    (f : A → T)
  where

  data Image : Type (ℓₐ ⊔ ℓᵢ)
  Im-decode : Image → T

  data Image where
    inc : A → Image
    quo : ∀ r r′ → R (Im-decode r) (Im-decode r′) → r ≡ r′
    quo-id : ∀ r → quo r r (rr (Im-decode r)) ≡ refl

  Im-decode (inc a) = f a
  Im-decode (quo r r' p i) = locally-small .to-path p i
  Im-decode (quo-id r i j) = to-path-refl {a = Im-decode r} locally-small i j

  Image-elim-prop
    : ∀ {ℓ′} {P : Image → Type ℓ′}
    → (∀ x → is-prop (P x))
    → (∀ x → P (inc x))
    → ∀ x → P x
  Image-elim-prop pprop pinc (inc x) = pinc x
  Image-elim-prop pprop pinc (quo r r′ p i) =
    is-prop→pathp (λ i → pprop (quo r r′ p i)) (Image-elim-prop pprop pinc r) (Image-elim-prop pprop pinc r′) i
  Image-elim-prop pprop pinc (quo-id r i j) =
    is-prop→squarep (λ i j → pprop (quo-id r i j))
      (λ _ → Image-elim-prop pprop pinc r)
      (is-prop→pathp (λ i → pprop _) _ _)
      (λ _ → Image-elim-prop pprop pinc r)
      (λ _ → Image-elim-prop pprop pinc r) i j

  inc-is-surjective : ∀ a → ∥ fibre inc a ∥
  inc-is-surjective = Image-elim-prop (λ _ → squash) (λ x → inc (x , refl))

  Im-decode-is-embedding : is-embedding Im-decode
  Im-decode-is-embedding = cancellable→embedding λ {x y} →
    Iso→Equiv (from , iso (ap Im-decode) invr (invl {x} {y}))
    where
      private module ls {x} {y} = Equiv (identity-system-gives-path locally-small {x} {y})
      from : ∀ {x y} → Im-decode x ≡ Im-decode y → x ≡ y
      from path = quo _ _ (ls.from path)

      invr : ∀ {x y} → is-right-inverse (ap Im-decode {x} {y}) from
      invr = J (λ y p → from (ap Im-decode p) ≡ p) (ap (quo _ _) (transport-refl _) ∙ quo-id _)

      invl : ∀ {x y} → is-left-inverse (ap Im-decode {x} {y}) from
      invl p = ls.ε _

module
  Type-replacement
    {ℓₐ ℓₜ} {A : Type ℓₐ} (f : A → Type ℓₜ)
  = Replacement univalence-identity-system f