ShouldBeApplicationOf.agda

module ShouldBeApplicationOf where

data One : Set where one : One
data Two : Set where two : Two

f : One -> Two
f two = two