16 lines
326 B
Agda
16 lines
326 B
Agda
|
{-# OPTIONS --cubical #-}
|
|||
|
|
|
|||
|
|
module Divergence where
|
|||
|
|
|
|||
|
|
open import Cubical.Core.Everything
|
|||
|
|
open import Cubical.Foundations.Prelude
|
|||
|
|
open import Data.Nat
|
|||
|
|
open import Relation.Binary.Core using (Rel)
|
|||
|
|
open import Relation.Nullary using (¬_)
|
|||
|
|
|
|||
|
|
_≢_ : {ℓ : Level} {A : Set ℓ} → Rel A ℓ
|
|||
|
|
x ≢ y = ¬ x ≡ y
|
|||
|
|
|
|||
|
|
_ : 0 ≢ 1
|
|||
|
|
_ = ?
|