0

When trying to prove a property over functions using list, I had to prove that the property is preserved by map over a list. Gladly, I found this useful congruence proof in Agda's standard library (here):

map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g
map-cong f≗g []       = refl
map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

I am trying to do my proof with respect to propositional equality ≡ but map-cong proves pointwise equality ≗. I have several questions here:

  1. I noticed that map-cong was previously implemented via ≡ but was generalized (I found this issue). This suggests that ≗ is a generalization of ≡. Is there a way to conclude propositional equality from pointwise equality? Something like a function f ≗ g → f ≡ g?

  2. When looking at the implementation, point-wise equality seems to be defined as propositional equality for functions via the extensionality axiom: Two functions are equal if they yield the same results for all inputs. This is emphasized by the above definition of map-cong which indeed matches not only on the proof f≗g but also on possible input arguments. Is my understanding correct? Is there any documentation or explanation on the implementation of ≗? I found the implementation in the standard library to be undocumented and rather intricate, split across several files and using multiple levels of abstraction.

  3. (Is there any way to conventiently browse the standard library except for browsing the source code (e.g., via grep or clicking in Github)?)

PaulProgrammerNoob
  • 624
  • 6
  • 19

1 Answers1

2

  1. No there isn't.

  2. That's correct. The definition of ≗ is a bit involved because it reuses existing notion but you can ask Agda to normalise it (C-c C-n in emacs) and see that it's just:

λ {A} {B} f g → (x : A) → f x ≡ g x
  1. I typically use http://agda.github.io/agda-stdlib/
gallais
  • 11,823
  • 2
  • 30
  • 63
  • Thank you so much! This is very valuable advice. The normalization command is indeed very helpful. I will keep that in mind! For those interested, assuming extensionality, one can then conclude propositional from pointwise equality: `≗→≡ : ∀ {A B : Set} {f g : A → B} → f ≗ g → f ≡ g` and then `≗→≡ f≗g = extensionality f≗g`. – PaulProgrammerNoob Nov 03 '22 at 14:21