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! -}