# Congruence Rule with Heterogeneous Equality in Agda

Congruence rule plays an important role in reasoning in Agda, and things become mystery as working under heterogeneous equality. In the standard library of Agda2, the type of Relation.Binary.HeterogeneousEquality.cong is

`∀{a b} (f : a → b) {i : a} {j : a} → i ≅ j → f i ≅ f j`

Since i and j are the same type, the equality between i and j becomes propositional instead of heterogeneous. Continue reading

# View for (mod n)

```data Bound (k : ℕ) : ℕ → Set where below : (n : ℕ) → (l : ℕ) → (l+n=k : l + (suc n) ≡ k) 　　　　→ Bound k n above : (n : ℕ) → (l : ℕ) → (l+k=n : l + k ≡ n) → Bound k n```

```data Z (k : ℕ) : ℕ → Set where 　cl : (m : ℕ){m<k : (suc m) ≤ k} (n : ℕ) → Z k (m + (n * k))```

# Setoids in Agda

Setoid is a record type in Agda, and it appears everywhere from `Relation.Binary.EqReasoning` to `Algebra`. But, why do we need such a type ? After reading “setoids in type theory”, I thought that setoids are used for mathematical constructions like subset, quotients in the intensional type theory and the Calculus of Inductive Construction. Since some of functional data structure could be represented as such constructions, it also may be useful for functional programming, at least for understanding it. Continue reading