# Embeddings and their diagonals

A functor is an embedding when its diagonal cone is a pullback. Equivalently,
the first projection of its self-pullback is an equivalence. The chosen diagonal
and the full cone beta make the projection criterion explicit.

```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Embeddings where

open import SCT.VolumeI.Chapter01.Section01.Vocabulary
import SCT.VolumeI.Chapter01.Section01.Terms as Terms
open Operations
open import SCT.VolumeI.Chapter01.Section02.Coherence
  using (id₌; comp-unitˡ; comp-unitʳ; comp-assoc; module Composition)
open Composition
open import SCT.VolumeI.Chapter01.Section02.Specialization using (comp₌-cong)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses
  using (inverse-composite; inverse-inverse; comp₌-unitˡ-One; comp₌-inverseʳ-One)
open import SCT.VolumeI.Chapter01.Section03.Equivalences
import SCT.VolumeI.Chapter01.Section03.Factorizations as Fact
open import SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence using (factor-through-preWhisker)
open import SCT.VolumeI.Chapter01.Section06.Cones
open import SCT.VolumeI.Chapter01.Section06.ConeTransport
open import SCT.VolumeI.Chapter01.Section06.ConeUniversality
open import SCT.VolumeI.Chapter01.Section06.Pullbacks
open import SCT.VolumeI.Chapter01.Section06.PullbackSquares using (IsPullback)
open import SCT.VolumeI.Chapter01.Section06.PullbackConstructions using (pullback₁-isEquiv; pullback-cone-isPullback)
open import SCT.VolumeI.Chapter01.Section06.PullbackArrowChange
open import SCT.VolumeI.Chapter01.Section06.NestedPullbacks


module _ {Γ : Context} where
  diagonal-cone : {C D : CAT Γ} (f : MAP C D) → Cone f f C
  diagonal-cone {C} f = record
    { left = id C; right = id C; match = id₌ (f ∘ id C) }

  diagonal : {C D : CAT Γ} (f : MAP C D) → MAP C (Pullback f f)
  diagonal f = pullback-factor (diagonal-cone f)

  IsEmbedding : {C D : CAT Γ} → MAP C D → Set m
  IsEmbedding f = IsPullback (diagonal-cone f)

  embedding-projection-isEquiv : {C D : CAT Γ} (f : MAP C D)
    → IsEmbedding f → IsEquiv (pullback₁ {f = f} {g = f})
  embedding-projection-isEquiv f ef = equiv-cancel-right (diagonal f) pullback₁ ef
    (equiv-transport ((pullback-factor-β₁ (diagonal-cone f)) ⁻¹) (id-isEquiv _))

  embedding-from-projection-isEquiv : {C D : CAT Γ} (f : MAP C D)
    → IsEquiv (pullback₁ {f = f} {g = f}) → IsEmbedding f
  embedding-from-projection-isEquiv f ep = equiv-cancel-left (diagonal f) pullback₁ ep
    (equiv-transport ((pullback-factor-β₁ (diagonal-cone f)) ⁻¹) (id-isEquiv _))
```

## Reflecting identifications

The two projections agree after restriction to the diagonal. Since the
diagonal is an equivalence, this agreement extends to the whole self-pullback.
Factoring a supplied identification through that pullback then identifies its
two source terms. This proves existence of the reflected identification;
it does not prescribe its postwhiskering image.

```agda
  embedding-projections-equal : {C D : CAT Γ} (f : MAP C D) → IsEmbedding f
    → (pullback₁ {f = f} {g = f}) =₁ pullback₂
  embedding-projections-equal f ef = Fact.factor
    (factor-through-preWhisker (diagonal f) ef
      ((pullback-factor-β₂ (diagonal-cone f)) ⁻¹ ∙ pullback-factor-β₁ (diagonal-cone f)))

  module _ {T C D : CAT Γ} where
    open Terms.InContext T using (Term)

    embedding-reflect : (f : MAP C D) → IsEmbedding f
      → (x y : Term C) → (f ∘ x) =₁ (f ∘ y) → x =₁ y
    embedding-reflect f ef x y α = pullback-factor-β₂ s ∙
      ((embedding-projections-equal f ef ▷ pullback-factor s) ∙ (pullback-factor-β₁ s) ⁻¹)
      where
      s : Cone f f T
      s = record { left = x; right = y; match = α }
```

## An embedding with a section

A supplied section gives one inverse law. Reflection gives the other by
applying the functor and using that supplied section law.

```agda
  embedding-with-section : {C D : CAT Γ} (f : MAP C D)
    → IsEmbedding f → Section f → IsEquiv f
  embedding-with-section f ef σ = record
    { inverse = Section.section σ
    ; left-inverse-law = embedding-reflect f ef _ _
        (comp-assoc f (Section.section σ) f ∙
          ((Section.section-law σ ▷ f) ∙ ((comp-unitˡ f) ⁻¹ ∙ comp-unitʳ f)))
    ; right-inverse-law = Section.section-law σ }
```

## Changing the functor

Change both arrows of the diagonal cospan along the supplied identification.
The resulting matching is an identification followed by its inverse, with
an intervening identity. Its normalization supplies a complete comparison
with the new diagonal cone. This proves invariance directly, without a
general change-of-cospan equivalence.

```agda
  embedding-cong : {C D : CAT Γ} {f g : MAP C D}
    → f =₁ g → IsEmbedding f → IsEmbedding g
  embedding-cong {C} {f = f} {g} α ef =
    isPullback-cone-identification comparison
      (RightArrowChange.isPullback α (cone-change-left α (diagonal-cone f))
        (isPullback-change-left α (diagonal-cone f) ef))
    where
    δ = α ▷ id C
    identity = id₌ (f ∘ id C)
    changed = cone-change-right α (cone-change-left α (diagonal-cone f))
    normalization : Cone.match changed =₂ id₌ (g ∘ id C)
    normalization = comp₌-inverseʳ-One δ ∙
      comp₌-cong (id₌ δ)
        (comp₌-unitˡ-One (δ ⁻¹) ∙
          (comp₌-cong (inverse-inverse identity) (id₌ (δ ⁻¹)) ∙
            inverse-composite δ (identity ⁻¹)))
    comparison : ConeIdentification₁ changed (diagonal-cone g)
    comparison = cone-retarget-match-identification changed (id₌ (g ∘ id C)) normalization
```

## Equivalences are embeddings

Base change of an equivalence makes the first self-pullback projection an
equivalence, so the projection criterion applies.

```agda
  equivalence-isEmbedding : {C D : CAT Γ} (f : MAP C D)
    → IsEquiv f → IsEmbedding f
  equivalence-isEmbedding f ef = embedding-from-projection-isEquiv f (pullback₁-isEquiv f f ef)
```

## Composition and base change

The nesting equivalence compares the relevant first projections. Its
projection consequence applies without an embedding hypothesis; the
embedding results then use the self-pullback criterion.

```agda
  composition-cone : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → Cone (g ∘ f) g C
  composition-cone {C} f g = record { left = id C ; right = f ; match = comp-unitʳ (g ∘ f) }

  composition-cone-isPullback : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) →
    IsEmbedding g → IsPullback (composition-cone f g)
  composition-cone-isPullback f g eg = equiv-cancel-left (pullback-factor (composition-cone f g)) pullback₁
    (nested-projection-isEquiv f g g (embedding-projection-isEquiv g eg))
    (equiv-transport ((pullback-factor-β₁ (composition-cone f g)) ⁻¹) (id-isEquiv _))

  module LeftCancellation {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) (eg : IsEmbedding g) where

    t : Cone g (g ∘ f) C
    t = cone-swap (composition-cone f g)
    et : IsPullback t
    et = SwappedCone.isPullback (composition-cone f g) (composition-cone-isPullback f g eg)
    module N = Nested f g (g ∘ f) t et

    compose : IsEmbedding f → IsEmbedding (g ∘ f)
    compose ef = embedding-from-projection-isEquiv (g ∘ f)
      (equiv-cancel-right N.flatten pullback₁ N.flatten-isEquiv
        (equiv-transport ((pullback-factor-β₁ N.flat-cone) ⁻¹) (embedding-projection-isEquiv f ef)))

    cancel : IsEmbedding (g ∘ f) → IsEmbedding f
    cancel egf = embedding-from-projection-isEquiv f
      (equiv-transport (pullback-factor-β₁ N.flat-cone)
        (equiv-compose N.flatten pullback₁ N.flatten-isEquiv (embedding-projection-isEquiv (g ∘ f) egf)))

```

## Base change

```agda
module _ {Γ : Context} where
  chosen-base-change-embedding : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) →
    IsEmbedding g → IsEmbedding (pullback₁ {f = f} {g})
  chosen-base-change-embedding {C = C} {D = D} f g eg = embedding-from-projection-isEquiv p
    (equiv-transport (pullback-factor-β₁ N.flat-cone)
      (equiv-compose N.flatten pullback₁ N.flatten-isEquiv outerProjection))
    where
    p : MAP (Pullback f g) C
    p = pullback₁ {f = f} {g}
    q : MAP (Pullback f g) D
    q = pullback₂ {f = f} {g}
    module N = ChosenNested p f g
    module Change = ChangeLeftArrow (pullback-match {f = f} {g}) g
    otherProjection : IsEquiv (pullback₁ {f = g ∘ q} {g})
    otherProjection = nested-projection-isEquiv q g g (embedding-projection-isEquiv g eg)
    outerProjection : IsEquiv (pullback₁ {f = f ∘ p} {g})
    outerProjection = equiv-transport (pullback-factor-β₁ (cone-change-left (pullback-match {f = f} {g}) (pullback-cone (f ∘ p) g)))
      (equiv-compose Change.forward pullback₁ Change.forward-isEquiv otherProjection)

  base-change-embedding : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
    (s : Cone f g T) → IsPullback s → IsEmbedding g → IsEmbedding (Cone.left s)
  base-change-embedding {f = f} {g} s es eg = embedding-cong (pullback-factor-β₁ s)
    (LeftCancellation.compose (pullback-factor s) pullback₁ (chosen-base-change-embedding f g eg)
      (equivalence-isEmbedding (pullback-factor s) es))

  chosen-base-change-embeddingʳ : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) →
    IsEmbedding f → IsEmbedding (pullback₂ {f = f} {g})
  chosen-base-change-embeddingʳ f g ef = base-change-embedding (cone-swap (pullback-cone f g))
    (SwappedCone.isPullback (pullback-cone f g) (pullback-cone-isPullback f g)) ef

```

## Relative criterion

```agda
module _ {Γ : Context} where
  module RelativeEmbedding {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
    (s : Cone f g T) (ef : IsEmbedding f) where

    projection : IsEmbedding (pullback₂ {f = f} {g})
    projection = chosen-base-change-embeddingʳ f g ef

    factor-isEmbedding : IsEmbedding (Cone.right s) → IsEmbedding (pullback-factor s)
    factor-isEmbedding eu = LeftCancellation.cancel (pullback-factor s) pullback₂ projection
      (embedding-cong ((pullback-factor-β₂ s) ⁻¹) eu)

    right-isEmbedding : IsEmbedding (pullback-factor s) → IsEmbedding (Cone.right s)
    right-isEmbedding eh = embedding-cong (pullback-factor-β₂ s)
      (LeftCancellation.compose (pullback-factor s) pullback₂ projection eh)
```