{-# OPTIONS --safe #-}
module Cubical.Foundations.Structure where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Syntax.Syntax

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

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.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 ℓ'
-- 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