How can I prove dependent function types equal in Agda?

January 6, 2024

When programming in Agda I have defined the following function:

WeirdType : (n : ℕ) → Set
WeirdType n with n + zero ≟ suc n
WeirdType n    | no ¬n+zero≡sucn = ℕ
WeirdType n    | yes n+zero≡sucn = ℕ → ℕ

It’s easy to prove that this always gives ℕ:

lemma : (n : ℕ) → ℕ ≡ WeirdType n
lemma n with n + zero ≟ suc n
lemma n    | no ¬n+zero≡sucn = refl
lemma n    | yes n+zero≡sucn =
    ⊥-elim
        (case
            trans (+-comm zero n) n+zero≡sucn
        of λ())

What I’d like to prove is the following:

theorem : (ℕ → ℕ) ≡ ((n : ℕ) → WeirdType n)

The problem is I can’t figure out how to manipulate types in a proof in the way that I can with non-types. It seems like I should be doing something like the following:

TypeTransform : Set → Set
TypeTransform Type = (n : ℕ) → Type

theorem : (ℕ → ℕ) ≡ ((n : ℕ) → WeirdType n)
theorem = cong TypeTransform lemma

but it results in the following error:

Cannot instantiate the metavariable _182 to solution
WeirdType n₁
| Relation.Nullary.Decidable.Core.map′ (≡ᵇ⇒≡ (n₁ + zero) (suc n₁))
  (≡⇒≡ᵇ (n₁ + zero) (suc n₁))
  (Data.Bool.Properties.T? (n₁ + zero ≡ᵇ suc n₁))
since it contains the variable n₁
which is not in scope of the metavariable
when checking that the inferred type of an application
  TypeTransform ℕ ≡ TypeTransform _y_182
matches the expected type
  (ℕ → ℕ) ≡ ((n₁ : ℕ) → WeirdType n₁)

I guess this is because I haven’t told it that the n in TypeTransform and in lemma are the same, but I don’t know the syntax to do that. After messing around it seems like I can prove similar theorems as long as the function involved is simple enough for Agda to resolve it with refl.

WeirdType' : (n : ℕ) → Set
WeirdType' n with suc n ≟ zero
WeirdType' n    | (no ¬sucn≡zero) = ℕ
WeirdType' n    | (yes sucn≡zero) = ℕ → ℕ

theorem' : (ℕ → ℕ) ≡ ((n : ℕ) → WeirdType' n)
theorem' = refl

This suggests that this sort of theorem is provable in Agda but I can’t find the correct syntax to express the proof. Does anyone have any suggestions?

>Solution :

You need to postulate some form of function extensionality for this:

open import Agda.Primitive
open import Axiom.Extensionality.Propositional

postulate
  ext : Extensionality lzero (lsuc lzero)

theorem : (ℕ → ℕ) ≡ ((n : ℕ) → WeirdType n)
theorem = ∀-extensionality ext _ _ lemma

Alternatively, in Cubical Agda this is provable without any postulates (because function extensionality is built into the theory, and follows from univalence).