module Cat.Diagram.Subterminal where

Subterminal objects🔗

An object of a category is subterminal if there is at most one map from every other object into that is, if the set is a proposition for all

  is-subterminal : Ob  Type _
  is-subterminal P =  X  is-prop (Hom X P)

This is weaker than being a terminal object whose defining property is that the into are contractible. In particular, every terminal object is subterminal.

  terminal→subterminal :  {T}  is-terminal C T  is-subterminal T
  terminal→subterminal term X = is-contr→is-prop (term X)

Subterminal objects can be thought of as the interpretations of truth values, or propositions, in the internal logic of To make this a bit more precise, note that, in a category with a terminal object an object is subterminal if and only if the unique map is monic (hence if is a subobject of In other words, if has a subobject classifier then subterminal objects are classified by maps

  module _ (top : Terminal C) where
    open Terminal top

    is-sub-terminal : Ob  Type _
    is-sub-terminal P = is-monic (! {x = P})

    subterminal≃sub-terminal :  P  is-subterminal P  is-sub-terminal P
    subterminal≃sub-terminal P = prop-ext!
       h f g _  h _ f g)
       h X x y  h x y (!-unique₂ _ _))

Subterminal objects also have various equivalent characterisations in terms of products. To start with, is subterminal if and only if the following diagram is a product diagram:

  is-subterminal₁ : Ob  Type _
  is-subterminal₁ P = is-product C (id {x = P}) (id {x = P})

Furthermore, is subterminal if and only if there is some product such that the two projections are equal, or equivalently such that the diagonal map is invertible. Intuitively, these conditions all say that “squares to itself 1”, which is something we expect of propositions.

  is-subterminal₂ : Ob  Type _
  is-subterminal₂ P = ∃[ p  Product C P P ] p .π₁  p .π₂

  is-subterminal₃ : Ob  Type _
  is-subterminal₃ P = ∃[ p  Product C P P ] is-invertible (p .⟨_,_⟩ id id)
Proving these equivalences is a succession of elementary exercises, so we leave them hidden in this <details> tag.
  module _ (P : Ob) where
    is-subterminal₀→₁ : is-subterminal P  is-subterminal₁ P
    is-subterminal₀→₁ h .is-product.⟨_,_⟩ f g = f
    is-subterminal₀→₁ h .is-product.π₁∘⟨⟩ = idl _
    is-subterminal₀→₁ h .is-product.π₂∘⟨⟩ = idl _  h _ _ _
    is-subterminal₀→₁ h .is-product.unique a b = sym (idl _)  a

    is-subterminal₁→₀ : is-subterminal₁ P  is-subterminal P
    is-subterminal₁→₀ h X f g = sym (h .is-product.π₁∘⟨⟩)  h .is-product.π₂∘⟨⟩

    is-subterminal₁→₂ : is-subterminal₁ P  is-subterminal₂ P
    is-subterminal₁→₂ h = inc (p , refl)
      where
        p : Product C P P
        p .apex = P
        p .π₁ = id
        p .π₂ = id
        p .has-is-product = h

    is-subterminal₂→₀ : is-subterminal₂ P  is-subterminal P
    is-subterminal₂→₀ = rec! λ p h X f g 
      sym (p .π₁∘⟨⟩) ∙∙ h ⟩∘⟨refl ∙∙ p .π₂∘⟨⟩

    is-subterminal₁→₃ : is-subterminal₁ P  is-subterminal₃ P
    is-subterminal₁→₃ h = inc (p , subst is-invertible eq id-invertible)
      where
        p : Product C P P
        p .apex = P
        p .π₁ = id
        p .π₂ = id
        p .has-is-product = h

        eq : id  h .is-product.⟨_,_⟩ id id
        eq = h .is-product.unique (idl _) (idl _)

    is-subterminal₃→₁ : is-subterminal₃ P  is-subterminal₁ P
    is-subterminal₃→₁ = rec! λ p h 
      is-product-iso-apex h (p .π₁∘⟨⟩) (p .π₂∘⟨⟩) (p .has-is-product)

  1. Another way to say this is that, in a cartesian monoidal category, an object is subterminal if and only if the unique comonoid structure on it is idempotent, but this borders on the ridiculous.↩︎