module exampleFullLogicalFramework where


B : Set1
B = Set

f : Set -> Set1
f X = X

C : Set1
C = Set0


D : Set2
D = Set1