Projections for the principal fields of records

[WhatisRT]

As @Soupstraw pointed out, it's sometimes confusing to read something like proj₁, since it's not always clear if we're projecting out from something we think of as a pair, or if we're projecting away a proof. Related to this is the issue that we sometimes have records that have a 'principal' field, like the Carrier field in many algebraic structures for example. It would be nice to have a consistent way of projecting away less relevant parts of a record, for example with the following typeclass:

record HasDowncast {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  field _↓ : A → B