{-

Constant structure: _ ↦ A

-}
{-# OPTIONS --safe #-}
module Cubical.Structures.Constant where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Foundations.SIP

private
  variable
     ℓ' : Level

-- Structured isomorphisms

module _ (A : Type ℓ') where

  ConstantStructure : Type   Type ℓ'
  ConstantStructure _ = A

  ConstantEquivStr : StrEquiv {} ConstantStructure ℓ'
  ConstantEquivStr (_ , a) (_ , a') _ = a  a'

  constantUnivalentStr : UnivalentStr {} ConstantStructure ConstantEquivStr
  constantUnivalentStr e = idEquiv _

  constantEquivAction : EquivAction {} ConstantStructure
  constantEquivAction e = idEquiv _

  constantTransportStr : TransportStr {} constantEquivAction
  constantTransportStr e _ = sym (transportRefl _)