open import 1Lab.Equiv.Fibrewise
open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel.Universe
open import 1Lab.Path.Groupoid
open import 1Lab.Type.Sigma
open import 1Lab.Univalence
open import 1Lab.Type.Pi
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Equiv.Embedding where

private variable
  β„“ ℓ₁ : Level
  A B : Type β„“
  w x : A

EmbeddingsπŸ”—

One of the most important observations leading to the development of categorical set theory is that injective maps into a set SS correspond to maps from SS into a universe of propositions, normally denoted Ω\Omega. Classically, this object is Ω={0,1}\Omega = \{ 0 , 1 \}, but there are other settings in which this idea makes sense (elementary topoi) where the subobject classifier is not a coproduct 1∐11 \coprod 1.

To develop this correspondence, we note that, if a map is injective and its codomain is a set, then all the fibres fβˆ—(x)f^*(x) of ff are propositions.

injective : (A β†’ B) β†’ Type _
injective f = βˆ€ {x y} β†’ f x ≑ f y β†’ x ≑ y

injective→is-embedding
  : is-set B β†’ (f : A β†’ B) β†’ injective f
  β†’ βˆ€ x β†’ is-prop (fibre f x)
injective→is-embedding bset f inj x (f*x , p) (f*x′ , q) =
  Ξ£-prop-path (Ξ» x β†’ bset _ _) (inj (p βˆ™ sym q))

In fact, this condition is not only necessary, it is also sufficient. Thus, we conclude that, for maps between sets, these notions are equivalent, and we could take either as the definition of β€œsubset inclusion”.

has-prop-fibres→injective
  : (f : A β†’ B) β†’ (βˆ€ x β†’ is-prop (fibre f x))
  β†’ injective f
has-prop-fibres→injective _ prop p = ap fst (prop _ (_ , p) (_ , refl))

between-sets-injective≃has-prop-fibres
  : is-set A β†’ is-set B β†’ (f : A β†’ B)
  β†’ injective f ≃ (βˆ€ x β†’ is-prop (fibre f x))
between-sets-injective≃has-prop-fibres aset bset f =
  prop-ext (Ξ» p q i x β†’ aset _ _ (p x) (q x) i)
           (Ξ -is-hlevel 1 Ξ» _ β†’ is-prop-is-prop)
           (injective→is-embedding bset f)
           (has-prop-fibres→injective f)

Since we want β€œis a subtype inclusion” to be a property β€” that is, we really want to not care about how a function is a subtype inclusion, only that it is, we define embeddings as those functions which have propositional fibres:

is-embedding : (A β†’ B) β†’ Type _
is-embedding f = βˆ€ x β†’ is-prop (fibre f x)

_β†ͺ_ : Type β„“ β†’ Type ℓ₁ β†’ Type _
A β†ͺ B = Ξ£[ f ∈ (A β†’ B) ] is-embedding f

Univalence β€” specifically, the existence of classifying objects for maps with PP-fibres β€” tells us that the embeddings into BB correspond to the families of propositional types over BB.

subtype-classifier
  : βˆ€ {β„“} {B : Type β„“}
  β†’ (Ξ£[ A ∈ Type β„“ ] (A β†ͺ B)) ≃ (B β†’ Ξ£[ T ∈ Type β„“ ] (is-prop T))
subtype-classifier {β„“} = Map-classifier {β„“ = β„“} is-prop
module subtype-classifier {β„“} {B : Type β„“} = Equiv (subtype-classifier {B = B})

A canonical source of embedding, then, are the first projections from total spaces of propositional families. This is because, as Fibre-equiv tells us, the fibre of Ο€1\pi_1 over xx is equivalent to β€œthe space of possible second coordinates”, i.e., B(x)B(x). Since B(x)B(x) was assumed to be a prop., then so are the fibres of fst.

Subset-proj-embedding
  : βˆ€ {B : A β†’ Type β„“} β†’ (βˆ€ x β†’ is-prop (B x))
  β†’ is-embedding {A = Ξ£ A B} fst
Subset-proj-embedding {B = B} Bprop x = is-hlevel≃ 1 (Fibre-equiv B x) (Bprop _)

embedding→monic
  : βˆ€ {β„“ β„“β€² β„“β€²β€²} {A : Type β„“} {B : Type β„“β€²} {f : A β†’ B}
  β†’ is-embedding f
  β†’ βˆ€ {C : Type β„“β€²β€²} (g h : C β†’ A) β†’ f ∘ g ≑ f ∘ h β†’ g ≑ h
embedding→monic {f = f} emb g h p =
  funext Ξ» x β†’ ap fst (emb _ (g x , refl) (h x , happly (sym p) x))

monic→is-embedding
  : βˆ€ {β„“ β„“β€² β„“β€²β€²} {A : Type β„“} {B : Type β„“β€²} {f : A β†’ B}
  β†’ is-set B
  β†’ (βˆ€ {C : Set β„“β€²β€²} (g h : ∣ C ∣ β†’ A) β†’ f ∘ g ≑ f ∘ h β†’ g ≑ h)
  β†’ is-embedding f
monic→is-embedding {f = f} bset monic =
  injective→is-embedding bset _ λ {x} {y} p →
    happly (monic {C = el (Lift _ ⊀) (Ξ» _ _ _ _ i j β†’ lift tt)} (Ξ» _ β†’ x) (Ξ» _ β†’ y) (funext (Ξ» _ β†’ p))) _

As ff morphismsπŸ”—

A fully faithful functor is a functor whose action on morphisms is an isomorphism everywhere. By the β€œtypes are higher groupoids” analogy, functors are functions, so we’re left to consider: what is a fully faithful function? The answer turns out to be precisely β€œan embedding”, as long as we interpret β€œfully faithful” to mean β€œaction on morphisms is an equivalence” everywhere.

module _ {β„“ β„“β€²} {A : Type β„“} {B : Type β„“β€²} {f : A β†’ B} where
  embedding-lemma : (βˆ€ x β†’ is-contr (fibre f (f x))) β†’ is-embedding f
  embedding-lemma cffx y (x , p) q =
    is-contr→is-prop (subst is-contr (ap (fibre f) p) (cffx x)) (x , p) q

  cancellableβ†’embedding : (βˆ€ {x y} β†’ (f x ≑ f y) ≃ (x ≑ y)) β†’ is-embedding f
  cancellable→embedding eqv =
    embedding-lemma Ξ» x β†’ is-hlevel≃ 0 (Ξ£-ap-snd (Ξ» _ β†’ eqv)) $
      contr (x , refl) Ξ» (y , p) i β†’ p (~ i) , Ξ» j β†’ p (~ i ∨ j)

  embeddingβ†’cancellable : is-embedding f β†’ βˆ€ {x y} β†’ is-equiv {B = f x ≑ f y} (ap f)
  embedding→cancellable emb = total→equiv {f = λ y p → ap f {y = y} p}
    (is-contr→is-equiv
      (contr (_ , refl) Ξ» (y , p) i β†’ p i , Ξ» j β†’ p (i ∧ j))
      (contr (_ , refl) (is-hlevel≃ 1 (Ξ£-ap-snd Ξ» _ β†’ sym-equiv) (emb _) _)))

  abstract
    embedding→is-hlevel
      : βˆ€ n β†’ is-embedding f
      β†’ is-hlevel B (suc n)
      β†’ is-hlevel A (suc n)
    embeddingβ†’is-hlevel n emb a-hl = is-hlevel≃ (suc n) (Total-equiv f) $
      Σ-is-hlevel (suc n) a-hl λ x → is-prop→is-hlevel-suc (emb x)