Mere decidable embeddings

Content created by Fredrik Bakke.

Created on 2026-01-10.
Last modified on 2026-01-10.

module foundation.mere-decidable-embeddings where
Imports 
open import foundation.cantor-schroder-bernstein-decidable-embeddings
open import foundation.decidable-embeddings
open import foundation.functoriality-propositional-truncation
open import foundation.mere-equivalences
open import foundation.propositional-truncations
open import foundation.universe-levels
open import foundation.weak-limited-principle-of-omniscience

open import foundation-core.propositions

open import order-theory.large-preorders

Idea

A type A merely decidably embeds into a type B if there merely exists a decidable embedding of A into B.

Definition

mere-decidable-emb-Prop : {l1 l2 : Level} → UU l1 → UU l2 → Prop (l1 ⊔ l2)
mere-decidable-emb-Prop X Y = trunc-Prop (X ↪ᵈ Y)

mere-decidable-emb : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
mere-decidable-emb X Y = type-Prop (mere-decidable-emb-Prop X Y)

is-prop-mere-decidable-emb :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2) → is-prop (mere-decidable-emb X Y)
is-prop-mere-decidable-emb X Y = is-prop-type-Prop (mere-decidable-emb-Prop X Y)

Properties

Types equipped with mere decidable embeddings form a preordering

refl-mere-decidable-emb : {l1 : Level} (X : UU l1) → mere-decidable-emb X X
refl-mere-decidable-emb X = unit-trunc-Prop id-decidable-emb

transitive-mere-decidable-emb :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3} →
  mere-decidable-emb Y Z → mere-decidable-emb X Y → mere-decidable-emb X Z
transitive-mere-decidable-emb = map-binary-trunc-Prop comp-decidable-emb

mere-decidable-emb-Large-Preorder : Large-Preorder lsuc (_⊔_)
mere-decidable-emb-Large-Preorder =
  λ where
  .type-Large-Preorder l → UU l
  .leq-prop-Large-Preorder → mere-decidable-emb-Prop
  .refl-leq-Large-Preorder → refl-mere-decidable-emb
  .transitive-leq-Large-Preorder X Y Z → transitive-mere-decidable-emb

Assuming WLPO, then types equipped with mere decidable embeddings form a partial ordering

antisymmetric-mere-decidable-emb :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} → level-WLPO (l1 ⊔ l2) →
  mere-decidable-emb X Y → mere-decidable-emb Y X → mere-equiv X Y
antisymmetric-mere-decidable-emb wlpo =
  map-binary-trunc-Prop (Cantor-Schröder-Bernstein-WLPO wlpo)

Recent changes