{-# OPTIONS --cubical --no-import-sorts --safe #-} module Cubical.Foundations.Structure where open import Cubical.Core.Everything open import Cubical.Foundations.Prelude private variable ℓ ℓ' ℓ'' : Level S : Type ℓ → Type ℓ' -- A structure is a type-family S : Type ℓ → Type ℓ', i.e. for X : Type ℓ and s : S X, -- the pair (X , s) : TypeWithStr ℓ S means that X is equipped with a S-structure, witnessed by s. TypeWithStr : (ℓ : Level) (S : Type ℓ → Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ') TypeWithStr ℓ S = Σ[ X ∈ Type ℓ ] S X typ : TypeWithStr ℓ S → Type ℓ typ = fst str : (A : TypeWithStr ℓ S) → S (typ A) str = snd -- Alternative notation for typ ⟨_⟩ : TypeWithStr ℓ S → Type ℓ ⟨_⟩ = typ -- An S-structure should have a notion of S-homomorphism, or rather S-isomorphism. -- This will be implemented by a function ι : StrEquiv S ℓ' -- that gives us for any two types with S-structure (X , s) and (Y , t) a family: -- ι (X , s) (Y , t) : (X ≃ Y) → Type ℓ'' StrEquiv : (S : Type ℓ → Type ℓ'') (ℓ' : Level) → Type (ℓ-max (ℓ-suc (ℓ-max ℓ ℓ')) ℓ'') StrEquiv {ℓ} S ℓ' = (A B : TypeWithStr ℓ S) → typ A ≃ typ B → Type ℓ' -- An S-structure may instead be equipped with an action on equivalences, which will -- induce a notion of S-homomorphism EquivAction : (S : Type ℓ → Type ℓ'') → Type (ℓ-max (ℓ-suc ℓ) ℓ'') EquivAction {ℓ} S = {X Y : Type ℓ} → X ≃ Y → S X ≃ S Y EquivAction→StrEquiv : {S : Type ℓ → Type ℓ''} → EquivAction S → StrEquiv S ℓ'' EquivAction→StrEquiv α (X , s) (Y , t) e = equivFun (α e) s ≡ t