How can I prove a type is valid in Agda?

3
votes

I'm trying to do proofs over dependent functions, and I'm running into a snag.

So let's say we have a theorem f-equal

f-equal : ∀ {A B} {f : A → B} {x y : A} → x ≡ y → f x ≡ f y
f-equal refl = refl

I'm trying to prove a more general notion of equality preservation over dependent functions, and running into a snag. Namely, the type

Π-equal : ∀ {A} {B : A → Set} {f : {a : A} → B a} {x y : A} →
            x ≡ y → f x ≡ f y

is making the compiler unhappy, because it can't figure out that f x and f y are of the same type. This seems like it oughta be a fixable issue. Is it?

note; the equivalence relation used is defined like this:

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x
2
proofagdatheorem-provingdependent-typetype-theory

2 Answers

7
votes

You can explicitly change the type of f x:

Π-equal : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
        -> (p : x ≡ y) -> P.subst B p (f x) ≡ f y
Π-equal refl = refl

Or

Π-equal'T : ∀ {α β} {A : Set α} {B : A -> Set β} -> ((x : A) -> B x) -> (x y : A) -> x ≡ y -> Set β
Π-equal'T f x y p with f x | f y
...| fx | fy rewrite p = fx ≡ fy

Π-equal' : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
        -> (p : x ≡ y) -> Π-equal'T f x y p
Π-equal' refl = refl

Or you can use heterogeneous equality:

Π-equal'' : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
          -> x ≡ y -> f x ≅ f y
Π-equal'' refl = refl

The subst function also can be useful, here is it's type (C-c C-d P.subst in Emacs):

{a p : .Agda.Primitive.Level} {A : Set a} (P : A → Set p)
      {x y : A} →
      x ≡ y → P x → P y

Imports used:

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.HeterogeneousEquality as H

BTW, your f-equal is cong in the standard library.

2
votes

It can be handled by heterogeneous equality, which can be imported from Relation.Binary.HeterogeneousEquality: 

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
   refl : x ≅ x

Intuitively, het. equality carries evidence about the equality of the types involved as well as the equality of values.

You can find analogues for functions for standard equality (subst, trans, cong, etc.) in the module. Also, you can convert back and forth standard and het. equality using ≅-to-≡ and ≡-to-≅, but only when the types on the sides are demonstrably equal.

Note that the "rewrite" syntax can't be used with het. equality.

Alternatively, we can use standard equality with one of the sides coerced to the appropriate type:

Π-equal : 
  ∀ {A : Set} {B : A → Set}{f : ∀ a → B a}{x y : A} → (p : x ≡ y) → subst B p (f x) ≡ f y
Π-equal refl = refl

This approach is actually equivalent to het. equality, but I find het. equality much easier to work with.