Type hierarchy definition in Coq or Agda

Question

I would like to build a kind of type hierarchy:

B is of type A  ( B::A )

C and D are of type of B   (C,D ::B) 

E and F are of type of C     (E,F ::C)

I asked here if this is possible to be directly implemented in Isabelle, but the answer as you see was No. Is it possible to encode this directly in Agda or Coq?

PS: Suppose A..F are all abstract and some functions are defined over each type)

Thanks

Answer 1

If I understood your question correctly, you want something that looks like the identity type. When we declare the type constructor _isOfType_, we mention two Sets (the parameter A and the index B) but the constructor indeed makes sure that the only way to construct an element of such a type is to enforce that they are indeed equal (and that a is of this type):

data _isOfType_ {ℓ} {A : Set ℓ} (a : A) : (B : Set ℓ) → Set where
  indeed : a isOfType A

We can now have functions taking as arguments proofs that things are of the right type. Here I translated your requirements & assumed that I had a function f able to combine two Cs into one. Pattern-matching on the appropriate assumptions reveals that E and F are indeed on type C and can therefore be fed to f to discharge the goal:

example : ∀ (A : Set₃) (B : Set₂) (C D : Set₁) (E F : Set) →
    B isOfType A
  → C isOfType B → D isOfType B
  → E isOfType C → F isOfType C
  → (f : C → C → C) → C
example A B .Set D E F _ _ _ indeed indeed f = f E F

Do you have a particular use case in mind for this sort of patterns or are you coming to Agda with ideas you have encountered in other programming languages? There may be a more idiomatic way to formulate your problem.