I'm attempting to axiomatize a proof-irrelevant disjunction proposition with type elimination in Agda using the universe of proof-irrelevant propositions. However, when I attempt to define rewrite rules for the computation rules I get an error about a certain variable not being bound. For instance, taking a minimal example, the following code does not compile:
{-# OPTIONS --rewriting --prop #-}
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
module Disjunction where
private variable
α β : Prop
A : Set
postulate
_∨_ : (α : Prop) (β : Prop) → Prop
inl : α → α ∨ β
inr : β → α ∨ β
∨-rec : (a₁ : α → A) (a₂ : β → A) → ((x : α) (y : β) → a₁ x ≡ a₂ y) → α ∨ β → A
∨-rec-inl : {a₁ : α → A} {a₂ : β → A} {h : (x : α) (y : β) → a₁ x ≡ a₂ y} {x : α} → ∨-rec a₁ a₂ h (inl x) ≡ a₁ x
{-# REWRITE ∨-rec-inl #-}
and gives me the error
∨-rec-inl is not a legal rewrite rule, since the following variables are not bound by the left hand side: x
However, this error no longer occurs when I change α ∨ β to be a type (i.e. a term of Set) instead of a proof-irrelevant proposition. Why is this?
In order to apply the rewrite rule, Agda needs to infer the value of x, i.e. it needs to match the fourth argument to the pattern inl x. However, if this argument is made irrelevant, then it is not allowed for Agda to inspect it (since this would refute the irrelevance) hence Agda rejects the rule.