Coinitial maps in posets

Content created by Louis Wasserman.

Created on 2026-02-07.
Last modified on 2026-02-07.

module order-theory.coinitial-maps-posets where
Imports 
open import foundation.existential-quantification
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.posets

Idea

A map between posets f : A → B is coinitial if for any b : B, there exists an a : A such that f a ≤ b.

Definition

module _
  {l1 l2 l3 : Level}
  {A : UU l1}
  (P : Poset l2 l3)
  (f : A → type-Poset P)
  where

  is-coinitial-prop-map-Poset : Prop (l1 ⊔ l2 ⊔ l3)
  is-coinitial-prop-map-Poset =
    Π-Prop
      ( type-Poset P)
      ( λ y → ∃ A (λ x → leq-prop-Poset P (f x) y))

  is-coinitial-map-Poset : UU (l1 ⊔ l2 ⊔ l3)
  is-coinitial-map-Poset = type-Prop is-coinitial-prop-map-Poset

See also

Recent changes