broken.agda

{-# OPTIONS --cubical --safe --exact-split #-}

module broken where

open import Level public
  using    ( Level )
  renaming ( zero to ℓ-zero
           ; suc  to ℓ-suc
           ; _⊔_  to ℓ-max
           )

Type : (ℓ : Level) → Set (ℓ-suc ℓ)
Type ℓ = Set ℓ

private
  variable
    ℓD ℓ< : Level

record LinearOrderStr (D : Type ℓD) (ℓ< : Level) : Type (ℓ-max (ℓ-suc ℓ<) ℓD) where
  no-eta-equality
  field
    _<_ : D -> D -> Type ℓ<

module _ {D : Type ℓD} {{S : LinearOrderStr D ℓ<}} where
  open LinearOrderStr S public


module _ {D : Type ℓD} {O : LinearOrderStr D ℓ<}
          where
  private
    module O = LinearOrderStr O
    instance
      IO = O

  abstract
    broken : {b c : D} -> (b < c) -> b < c
    broken {b} {c} b<c = b<c
      where
      b<c2 : b < c
      b<c2 = b<c