Givens in Scala 3 as proofs of existence of types
Note
From the point of view of Type level programming, a given proves the existence of a type - e.g. the compiler can prove the existence of types, and then create new given instances using those types. This can be used for computations at compile time. (e.g. for a type level sum for example)
A given is conceptually constructing an instance of a type with a concrete behaviour where a using claused is used.