{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Equality.Base where

Definition

In blackboard mathematics, “x = y” is an assertion, a statement. For instance, this assertion might be true, or it might be false. In the Agda community, x ≡ y is a type—the type of witnesses that x and y are equal. For instance, this type could be inhabited, or it could be empty.

If in blackboard mathematics we would prove that x = y, in Agda we exhibit a value of type x ≡ y.

The following three lines set up these types:

infix 4 _≡_
data _≡_ {X : Set} : X → X → Set where
  refl : {a : X} → a ≡ a

The basic equality symbol = is used in Agda only for definitions. For formulating assumptions or results involing equality, we use ≡.