Sequences in strictly preordered sets

Content created by malarbol.

Created on 2025-04-22.
Last modified on 2025-04-22.

module order-theory.sequences-strictly-preordered-sets where
Imports 
open import foundation.sequences
open import foundation.universe-levels

open import order-theory.strictly-preordered-sets

Idea

A sequence in a strictly preordered set is a sequence in its underlying type.

Definition

Sequences in a strictly preordered set

module _
  {l1 l2 : Level} (A : Strictly-Preordered-Set l1 l2)
  where

  type-sequence-Strictly-Preordered-Set : UU l1
  type-sequence-Strictly-Preordered-Set =
    sequence (type-Strictly-Preordered-Set A)

Recent changes