Add syntax typeclass for types with carriers.

This allows types not using TypeWithStr to reuse the nice ⟨_⟩ syntax.

Cubical/Foundations/Structure.agda

@@ -3,6 +3,7 @@ module Cubical.Foundations.Structure where
 
 open import Cubical.Core.Everything
 open import Cubical.Foundations.Prelude
+open import Cubical.Syntax.⟨⟩
 
 private
   variable
@@ -21,9 +22,13 @@ typ = fst
 str : (A : TypeWithStr ℓ S) → S (typ A)
 str = snd
 
--- Alternative notation for typ
-⟨_⟩ : TypeWithStr ℓ S → Type ℓ
-⟨_⟩ = typ
+instance
+  TypeWithStr-has-⟨⟩ : ∀ {ℓ S} → has-⟨⟩ (TypeWithStr {ℓ' = ℓ'} ℓ S)
+  ⟨_⟩ ⦃ TypeWithStr-has-⟨⟩ ⦄ = typ
+
+-- Allow users to avoid importing the syntax module directly for
+-- backwards compatibility.
+open import Cubical.Syntax.⟨⟩ using (⟨_⟩) public
 
 -- An S-structure should have a notion of S-homomorphism, or rather S-isomorphism.
 -- This will be implemented by a function ι : StrEquiv S ℓ'

Cubical/README.agda

@@ -68,3 +68,6 @@ import Cubical.Reflection.Everything
 
 -- Displayed univalent graphs
 import Cubical.Displayed.Everything
+
+-- Syntax typeclasses
+import Cubical.Syntax.Everything

Cubical/Syntax/⟨⟩.agda

@@ -0,0 +1,12 @@
+{-# OPTIONS --safe #-}
+module Cubical.Syntax.⟨⟩ where
+
+open import Cubical.Core.Primitives
+
+-- A syntax typeclass for types which contain a "carrier" type in the
+-- sence of an algebraic structure.
+record has-⟨⟩ {ℓᵢ ℓc} (Instance : Type ℓᵢ) : Type (ℓ-max ℓᵢ (ℓ-suc ℓc)) where
+  field
+    ⟨_⟩ : Instance → Type ℓc
+
+open has-⟨⟩ ⦃ … ⦄ public