refl in agda : explaining congruence property

Question

With the following definition of equality, we have refl as constructor

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

and we can prove that function are congruent on equality

cong : ∀ { a b} { A : Set a }  { B : Set b }
       (f : A → B ) {m  n}  → m ≡ n → f m ≡ f n
cong f  refl  = refl

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 ?)

Is there an intuitive description on what is going on ?

Answer 1

Yes, the arguments in curly braces {} are implicit and they only need to be supplied or matched if agda cannot figure them out. It is necessary to specify them, since dependent types needs to refer to the values they depend on, but dragging them around all the time would make the code rather clunky.

The expression cong f refl = refl matches the explicit arguments (A → B) and (m ≡ n). If you wanted to match the implicit arguments, you'd need to put the matching expression in {}, but here there is no need for that. Then on the right hand side it is indeed the construction of (f m ≡ f n) using refl, and it works "by magic". Agda has a built-in axiom that proves this to be true. That axiom is similar (but stronger than) J-axiom - the induction axiom: if something C : (x y : A) → (x ≡ y) → Set is true for C x x refl, then it is also true for any x y : A and p : x ≡ y.

J : forall {A : Set} {C : (x y : A) → (x ≡ y) → Set} →
                     (c : ∀ x → C x x refl) →
                     (x y : A) → (p : x ≡ y) → C x y p
-- this really is an axiom, but in Agda there is a stronger built-in,
-- which can be used to prove this
J c x .x refl = c x -- this _looks_ to only mean x ≡ x
                    -- but Agda's built-in extends this proof to all cases
                    -- for which x ≡ y can be constructed - that's the point
                    -- of having induction

cong : ∀ { a b} { A : Set a }  { B : Set b }
       (f : A → B ) {m  n}  → m ≡ n → f m ≡ f n
cong f {x} {y} p = J {C = \x y p → f x ≡ f y} -- the type of equality
                                               -- of function results
                     (\_ → refl) -- f x ≡ f x is true indeed
                     x y p

(In this last line we: match explicit arguments f and p, and also the implicit arguments m=x and n=y. Then we pass to J one implicit argument, but it is not the first positional implicit, so we tell agda that it is C in the definition - without doing that, Agda won't see what type is meant by refl in \_ → refl)