You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
recordHasDowncast {a b} (A :Set a) (B :Set b) :Set (a ⊔ b) wherefield _↓ : A → B
The text was updated successfully, but these errors were encountered:
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 theCarrier
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:The text was updated successfully, but these errors were encountered: