Víctor López Juan vlopezj

This is an explanation of the changes introduced in pull request agda/agda#5234

Twin context infrastructure

When checking whether two well-typed terms t and u are convertible, they might not be typed in the same context.

From the example above, we have a constraint

WrapMonad tells us that a Monad implies Functor, Applicative

instance Monad m => Functor     (WrappedMonad m)
instance Monad m => Applicative (WrappedMonad m)
instance Monad m => Monad       (WrappedMonad m)

module FunImplicits where

open import Data.Bool

data Nat : Set where
  zero : Nat

	data EitherDup a = MyLeft a
	\| MyRight a

	class HasEndo t where
	-- \| prop> endo . endo == id
	endo :: t -> t

	instance HasEndo (EitherDup a) where
	endo (MyLeft a) = MyRight a
	endo (MyRight a) = MyLeft a