Source code on Github
{-# OPTIONS --v equivariance:100 #-}
open import Prelude.Init
open L.Mem
open import Prelude.DecEq
open import Prelude.Functor
open import Prelude.Monad
open import Prelude.Semigroup
open import Prelude.Show
open import Prelude.Setoid
open import Prelude.Lists
open import Prelude.ToN
open import Prelude.Tactics.PostulateIt

open import Prelude.Generics
open Meta
open Debug ("equivariance" , 100)

module Nominal.Swap.Equivariance (Atom : Set) โฆƒ _ : DecEq Atom โฆ„ where

open import Nominal.Swap.Base Atom

-- ** generically postulate the axiom scheme expressing distributivity of swapping:
{- โˆ€ (๐•’ ๐•“ : Atom).
     โˆ™[n = 0]
       โˆ€ (x : A).
         swap ๐•’ ๐•“ x โ‰ˆ swap ๐•’ ๐•“ x
     โˆ™[n = 1]
       โˆ€ (f : A โ†’ B) (x : A).
         swap ๐•’ ๐•“ (f x) โ‰ˆ (swap ๐•’ ๐•“ f) (swap ๐•’ ๐•“ x)
     โˆ™[n = 2]
       โˆ€ (f : A โ†’ B โ†’ C) (x : A) (y : B).
         swap ๐•’ ๐•“ (f x y) โ†’ (swap ๐•’ ๐•“ f) (swap ๐•’ ๐•“ x) (swap ๐•’ ๐•“ y)
     โ‹ฎ
-}
deriveSwapDistributiveType : Bool โ†’ Term โ†’ TC Type
deriveSwapDistributiveType equiv? t = do
  ty โ† inferType t
  print $ show t โ—‡ " : " โ—‡ show ty
  printCurrentContext
  ctx โ† getContext
  let
    asโ‚€ = argTys ty
    as  = map (fmap $ mapVars (_+ 2)) asโ‚€
    n = length as

    mkSwaps : Args Term โ†’ Term
    mkSwaps as = def (quote swap) $ map vArg ({-๐•’-} โ™ฏ (suc n) โˆท {-๐•“-} โ™ฏ n โˆท []) ++ as

    mkSwap : Opโ‚ Term
    mkSwap t = mkSwaps [ vArg t ]

    mkHead : Args Term โ†’ Term
    mkHead as = case t of ฮป where
      (def f asโ‚€) โ†’ def f (asโ‚€ ++ as)
      (con c asโ‚€) โ†’ con c (asโ‚€ ++ as)
      (var i asโ‚€) โ†’ var (i + 2 + n) (asโ‚€ ++ as)
      _           โ†’ unknown

    mkSwapHead : Args Term โ†’ Term
    mkSwapHead as =
      let
        a = case t of ฮป where
          (def f asโ‚€) โ†’ def f asโ‚€
          (con c asโ‚€) โ†’ con c asโ‚€
          (var i asโ‚€) โ†’ var (i + 2 + n) asโ‚€
          _           โ†’ unknown
      in mkSwaps (vArg a โˆท as)

    mkTerm : Opโ‚ Term โ†’ Args Term
    mkTerm mk = flip map (enumerate as) ฮป where
      (i , arg v _) โ†’ arg v $ mk (โ™ฏ (n โˆธ suc (toโ„• i)))

    lhs = mkSwap $ mkHead (mkTerm id)
    rhs = (if equiv? then mkHead else mkSwapHead) (mkTerm mkSwap)

    equivTy = vฮ [ "๐•’" โˆถ โ™ฏ (length ctx โˆธ 1) ]
              vฮ [ "๐•“" โˆถ โ™ฏ (length ctx) ]
              โˆ€args as (quote _โ‰ˆ_ โˆ™โŸฆ lhs โˆฃ rhs โŸง)
  print $ "Equivariant " โ—‡ show t โ—‡ " := " โ—‡ show equivTy
  print "-------------------------------------------------"
  return equivTy
  where
    โˆ€args : Args Type โ†’ (Type โ†’ Type)
    โˆ€args [] = id
    โˆ€args (a โˆท as) t = hฮ [ "_" โˆถ unArg a ] โˆ€args as t

deriveSwapโ†”       = deriveSwapDistributiveType false

macro
  Swapโ†” : Term โ†’ Hole โ†’ TC โŠค
  Swapโ†” t hole = deriveSwapโ†” t >>= unify hole

  swapโ†” : Term โ†’ Hole โ†’ TC โŠค
  swapโ†” t hole = do
    n โ† genPostulate =<< deriveSwapโ†” t
    unify hole (n โˆ™)

postulateSwapโ†” : Name โ†’ Term โ†’ TC โŠค
postulateSwapโ†” f t = declarePostulate (vArg f) =<< deriveSwapโ†” t

-- ** derive the statement of equivariance for given term of arbitrary arity,
-- be it a definition, constructor, or local variable
{- โˆ€ (๐•’ ๐•“ : Atom).
     โˆ™[n = 0]
       โˆ€ (x : A).
         swap ๐•’ ๐•“ x โ‰ˆ x
     โˆ™[n = 1]
       โˆ€ (f : A โ†’ B) (x : A).
         swap ๐•’ ๐•“ (f x) โ‰ˆ f (swap ๐•’ ๐•“ x)
     โˆ™[n = 2]
       โˆ€ (f : A โ†’ B โ†’ C) (x : A) (y : B).
         swap ๐•’ ๐•“ (f x y) โ†’ f (swap ๐•’ ๐•“ x) (swap ๐•’ ๐•“ y)
     โ‹ฎ
-}
macro
  Equivariant : Term โ†’ Hole โ†’ TC โŠค
  Equivariant t hole = deriveSwapDistributiveType true t >>= unify hole

private
  data X : Set where
    mkX : โ„• โ†’ โ„• โ†’ X

  variable
    ๐•’ ๐•“ ๐•” ๐•• : Atom
  postulate
    n m : โ„•
    f : โ„• โ†’ โ„•
    g : โ„• โ†’ โ„• โ†’ โ„•

    instance
      _ : ISetoid โ„•
      _ : ISetoid X
      _ : Swap X
      _ : Swap (โ„• โ†’ โ„•)
      _ : Swap (โ„• โ†’ โ„• โ†’ โ„•)
      _ : Swap (โ„• โ†’ โ„• โ†’ X)

  module _ ๐•’ ๐•“ where postulate
    distr-f : โˆ€ {n} โ†’
      swap ๐•’ ๐•“ (f n) โ‰ˆ (swap ๐•’ ๐•“ f) (swap ๐•’ ๐•“ n)
    equiv-f : โˆ€ {n} โ†’
      swap ๐•’ ๐•“ (f n) โ‰ˆ f (swap ๐•’ ๐•“ n)
    distr-g : โˆ€ {n m} โ†’
      swap ๐•’ ๐•“ (g n m) โ‰ˆ (swap ๐•’ ๐•“ g) (swap ๐•’ ๐•“ n) (swap ๐•’ ๐•“ m)
    equiv-g : โˆ€ {n m} โ†’
      swap ๐•’ ๐•“ (g n m) โ‰ˆ g (swap ๐•’ ๐•“ n) (swap ๐•’ ๐•“ m)
    distr-mkX : โˆ€ {n m} โ†’
      swap ๐•’ ๐•“ (mkX n m) โ‰ˆ (swap ๐•’ ๐•“ mkX) (swap ๐•’ ๐•“ n) (swap ๐•’ ๐•“ m)
    equiv-mkX : โˆ€ {n m} โ†’
      swap ๐•’ ๐•“ (mkX n m) โ‰ˆ mkX (swap ๐•’ ๐•“ n) (swap ๐•’ ๐•“ m)
  module _ {f : โ„• โ†’ โ„•} ๐•’ ๐•“ where postulate
    distr-โˆ€f : โˆ€ {n} โ†’ swap ๐•’ ๐•“ (f n) โ‰ˆ (swap ๐•’ ๐•“ f) (swap ๐•’ ๐•“ n)
    equiv-โˆ€f : โˆ€ {n} โ†’ swap ๐•’ ๐•“ (f n) โ‰ˆ f (swap ๐•’ ๐•“ n)

  _ = Swapโ†” f โˆ‹ distr-f
  _ = Swapโ†” f โˆ‹ swapโ†” f
  _ = Equivariant f โˆ‹ equiv-f
  _ = Swapโ†” g โˆ‹ distr-g
  _ = Swapโ†” g โˆ‹ swapโ†” g
  _ = Equivariant g โˆ‹ equiv-g
  _ = Swapโ†” mkX โˆ‹ distr-mkX
  _ = Swapโ†” mkX โˆ‹ swapโ†” mkX
  _ = Equivariant mkX โˆ‹ equiv-mkX
  module _ {f : โ„• โ†’ โ„•} where
    _ = Swapโ†” f โˆ‹ swapโ†” f
    _ = Swapโ†” f โˆ‹ distr-โˆ€f
    _ = Equivariant f โˆ‹ equiv-โˆ€f

  unquoteDecl distr-fโ€ฒ = postulateSwapโ†” distr-fโ€ฒ (quoteTerm f)
  unquoteDecl distr-gโ€ฒ = postulateSwapโ†” distr-gโ€ฒ (quoteTerm g)
  unquoteDecl distr-mkXโ€ฒ = postulateSwapโ†” distr-mkXโ€ฒ (quoteTerm mkX)
  module _ {f : โ„• โ†’ โ„•} where
    unquoteDecl distr-โˆ€fโ€ฒ = postulateSwapโ†” distr-โˆ€fโ€ฒ (quoteTerm f)