[Agda] Defining a module by pattern matching

[Guillaume Brunerie]

On 2013/5/15 Dr. ERDI Gergo <gergo at erdi.hu> wrote:
> On Wed, 15 May 2013, Guillaume Brunerie wrote:
> Is your equality type a valid EQUALITY built-in? Because I was able to get
> this working via 'rewrite', which requires _≡_ (or in your case, _==_) to be
> marked as the EQUALITY:
>
> module Guillaume where
>
> open import Relation.Binary.PropositionalEquality
>
> module FunctionArguments where
>   same-same : {A : Set} {x y : A} {P : A → Set} → x ≡ y → P x → P y
>   same-same refl Px = Px
>
> module ModuleArguments {A : Set} {x y : A} {eq : x ≡ y} where
>   same-same : {P : A → Set} → P x → P y
>   same-same Px rewrite eq = Px

Hmm, interesting. It wasn’t an EQUALITY built-in, but now it is and
your example works.
It’s getting closer, but it’s still not exactly what I want. Here is a
more concrete example (I don’t have the standard library, so maybe it
doesn’t compile as is)


module Guillaume {A : Set} {B : A → Set} where

open import Relation.Binary.PropositionalEquality

-- This is probably called [subst] or something like that
tr : {x y : A} (p : x ≡ y) → B x → B y
tr refl u = u

tr! : {x y : A} (p : x ≡ y) → B y → B x
tr! refl v = v

module FunctionArguments where
  thing : {x y : A} (p : x ≡ y) (u : B x) (v : B y) → tr p u ≡ v → u ≡ tr! p v
  thing refl u v x = x

module ModuleArguments {x y : A} (p : x ≡ y) (u : B x) (v : B y) where
{- Does not compile
  thing' : tr p u ≡ v → u ≡ tr! p v
  thing' rewrite p = {!!}
-}


Guillaume