{-# OPTIONS --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 an 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

instance
  mkTypeWithStr :  {} {S : Type   Type ℓ'} {X}  {{S X}}  TypeWithStr  S
  mkTypeWithStr {{i}} = _ , i

-- 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