Questions - Agda

Hi, beginner here working through PLFA. Would anyone be able to help provide an intuition on why function extensionality is not provable from within Agda. I’ve heard that it is possible with cubical agda - but i don’t have a good grasp on what that is yet. I’ve also heard agda’s type system described as intentional whereas others are extensional. Does this have anything to do with function extensionality or are they unrelated?

it's "not true" in a sense - the traditional thing called equality in agda is "it's actually the 'same' thing", while that's not necessarily true for two functions that match pointwise

e.g. one function could have an entirely different algorithm

so they're not really "the same" as "programs"

I'm not familiar with path equality, and don't know what it means there (and why you can use it with cubical)

I'm not sure about this, but if we want to be more precise, I'd wager that for two functions to be "the same" in vanilla agda (e.g. you can write refl : f == g) they need to have the same case/decision tree

Ahh okay that makes sense. I guess for things to be able to be refl they need to have the same normal form - and since you cant pattern match/ deconstruct functions you can't build up any kind of proof to assert this. From a logical point of view I can see that just because two functions give the same result pointwise - to say that they are equal as a result is 'just like an opinion... man'

doing some testing in agda

  _+l_ : ℕ → ℕ → ℕ
  zero +l b = b
  suc a +l b = suc (a +l b)

  _+r_ : ℕ → ℕ → ℕ
  a +r zero = a
  a +r suc b = suc (a +r b)


  same : _+l_ ≡ _+r_
  same =  refl    -- does not type check

  _+l'_ : ℕ → ℕ → ℕ
  zero +l' b = b
  suc a +l' b = suc (a +l' b)

  same2 : _+l_ ≡ _+l'_
  same2 =  refl    --  doesn't type check - but feels like it should

   id : ∀ {A : Set} → A → A
  id = λ x → x

  id2 : ∀ {A : Set} → A → A
  id2 = λ x → x

 -- Both of these type check

  test : ∀ {A : Set} → id {A} ≡ (λ x → x)
  test = refl

  test2 : ∀ {A : Set} → id {A} ≡ id2 {A}
  test2 = refl

I can understand why structurally +l and +r are distinct but it seems odd that test and test2 with id functions type check but the +l' and +l don't.

Also from the book he says:

Postulating extensionality does not lead to difficulties, as it is known to be consistent with the theory that underlies Agda.

It would be interesting to understand why this is true but I'm sure I would need to understand much more type theory before I could handle that :confounded:

Hi not sure if this is the best place to ask but I am using https://github.com/TOTBWF/agda-evil-emacs as my emacs configuration, and recently after updating something I am getting the following error when opening emacs:

Error in post-command-hook (evil-mode-check-buffers): (wrong-number-og-arguments (4 . 4) 5)

Any Emacs experts could help me?

cc @Reed Mullanix

Fixed by nuking my .emacs.d folder and restarting emacs