module Identity where

open import Nat

{-
We shall now define the set I A a a' containing proofs that a, a' : A are identical. We call this the identity set. The nature of identity sets is a hot topic (cf "homotopy type theory") but the basic idea in intuitionistic type theory is that there is only one way to construct a proof of an identity: a and a' must be *the same* (modulo simplification). Hence we define the identity sets as a data type with one constructor:
-}

data I (A : Set) (a : A) : A → Set where
  refl : I A a a

{-
We get a more familiar looking notation if we use the infix sign ≡ and make the type A implicit:
-}

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

infix 3 _≡_

1+1=2 : 1 + 1 ≡ 2
1+1=2 = refl

{-
When we case-split (C-c C-c) a proof c : I A a a', Agda replaces c by the only possible constructor refl, and unifies a and a'. We can see how this works by proving that identity is a symmetric relation:
-}

sym : {A : Set} → {a₁ a₂ : A} → a₁ ≡ a₂ → a₂ ≡ a₁
sym refl = refl

{-
Exercise: prove transitivity by doing pattern matching in both arguments:

trans : {A : Set} → {a₁ a₂ a₃ : A} → a₁ ≡ a₂ → a₂ ≡ a₃ → a₁ ≡ a₃
trans p₁ p₂ = {!!}

We can also prove the general rule of identity elimination, the rule that states that we can substitute identical elements for each other. If a property is true for a₂, then it's
also true for any a₁ equal to a₂
-}

subst : {A : Set} -> {P : A → Set} → {a₁ a₂ : A} → a₁ ≡ a₂ -> P a₂ -> P a₁
subst refl q = q

{-
Prove that functions map equal inputs to equal outputs
-}

cong : {A B : Set} → {a₁ a₂ : A} → (f : A → B)
  → a₁ ≡ a₂
  → f a₁ ≡ f a₂
cong f refl = refl

{-
Exercise: prove symmetry and transitivity using subst but without using pattern matching!
-}