This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Rewriting

{-# OPTIONS --rewriting #-}

module reflection.rewriting where
Imports 
open import foundation-core.identity-types

Idea

Agda's rewriting functionality allows us to add new strict equalities to our type theory. Given an identification β : x ＝ y, then adding a rewrite rule for β with

{-# REWRITE β #-}

will make it so x rewrites to y, i.e., x ≐ y.

Warning. Rewriting is by nature a very unsafe tool so we advice exercising abundant caution when defining such rules.

Definitions

We declare to Agda that the standard identity relation may be used to define rewrite rules.

{-# BUILTIN REWRITE _＝_ #-}

See also