From a67592907605104fbd67a1cf93966d0297b801bd Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Sun, 15 Aug 2021 21:08:10 -0400
Subject: [PATCH] Add syntax typeclass for types with carriers.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This allows types not using TypeWithStr to reuse the nice ⟨_⟩ syntax.
---
 Cubical/Foundations/Structure.agda             | 11 ++++++++---
 Cubical/README.agda                            |  3 +++
 "Cubical/Syntax/\342\237\250\342\237\251.agda" | 12 ++++++++++++
 3 files changed, 23 insertions(+), 3 deletions(-)
 create mode 100644 "Cubical/Syntax/\342\237\250\342\237\251.agda"

diff --git a/Cubical/Foundations/Structure.agda b/Cubical/Foundations/Structure.agda
index 5f0b31c08b..6de3bf9e1b 100644
--- a/Cubical/Foundations/Structure.agda
+++ b/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 ℓ'
diff --git a/Cubical/README.agda b/Cubical/README.agda
index d8e97aea8b..c35afe47a3 100644
--- a/Cubical/README.agda
+++ b/Cubical/README.agda
@@ -68,3 +68,6 @@ import Cubical.Reflection.Everything
 
 -- Displayed univalent graphs
 import Cubical.Displayed.Everything
+
+-- Syntax typeclasses
+import Cubical.Syntax.Everything
diff --git "a/Cubical/Syntax/\342\237\250\342\237\251.agda" "b/Cubical/Syntax/\342\237\250\342\237\251.agda"
new file mode 100644
index 0000000000..03496011b7
--- /dev/null
+++ "b/Cubical/Syntax/\342\237\250\342\237\251.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