Issue121.agda

module Issue121 where

id : Set → Set
id A = A

data Bool : Set where
  true  : Bool
  false : Bool

F : Bool → Set → Set
F true  = id
F false = id

G : Bool → Set → Set
G true = id
G false = λ A → A

data D : Set where
  nop : (b : Bool) → F b D → D
  bop : (b : Bool) → G b D → D