title: refl in agda : explaining congruence property
body: <p>With the following definition of equality, we have refl as constructor</p>
  
  <pre><code>data _≡_ {a} {A : Set a} (x : A) : A → Set a where
      refl : x ≡ x
  </code></pre>
  
  <p>and we can prove that function are congruent on equality</p>
  
  <pre><code>cong : ∀ { a b} { A : Set a }  { B : Set b }
         (f : A → B ) {m  n}  → m ≡ n → f m ≡ f n
  cong f  refl  = refl
  </code></pre>
  
  <p>I am not sure I can parse what is going on exactly here.
  I think we are pattern matching refl on hidden parameters : if we replace the first occurence by refl by another identifier, we get a type error.
  after pattern matching, I imagine that m and n are the same by the definition of refl. then magic occurs (a definition of functionality of a relation is applied ? or is it build in ?)</p>
  
  <p>Is there an intuitive description on what is going on ?</p>