------------------------------------------------------------------------
-- The Agda standard library
--
-- This module constructs the zero R-module, and similar for weaker
-- module-like structures.
-- The intended universal property is that, given any R-module M, there
-- is a unique map into and a unique map out of the zero R-module
-- from/to M.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Level

module Algebra.Module.Construct.Zero {c  : Level} where

open import Algebra.Bundles
open import Algebra.Module.Bundles
open import Data.Unit.Polymorphic
open import Relation.Binary.Core using (Rel)

private
  variable
    r s ℓr ℓs : Level

------------------------------------------------------------------------
-- gather all the functionality in one place

module ℤero where

  infix  4 _≈ᴹ_
  Carrierᴹ : Set c
  Carrierᴹ = 

  _≈ᴹ_     : Rel Carrierᴹ 
  _ ≈ᴹ _ = 

------------------------------------------------------------------------
-- Raw bundles

rawLeftSemimodule : {R : Set r}  RawLeftSemimodule R c 
rawLeftSemimodule = record { ℤero }

rawLeftModule : {R : Set r}  RawLeftModule R c 
rawLeftModule = record { ℤero }

rawRightSemimodule : {R : Set r}  RawRightSemimodule R c 
rawRightSemimodule = record { ℤero }

rawRightModule : {R : Set r}  RawRightModule R c 
rawRightModule = record { ℤero }

rawBisemimodule : {R : Set r} {S : Set s}  RawBisemimodule R S c 
rawBisemimodule = record { ℤero }

rawBimodule : {R : Set r} {S : Set s}  RawBimodule R S c 
rawBimodule = record { ℤero }

rawSemimodule : {R : Set r}  RawSemimodule R c 
rawSemimodule = record { ℤero }

rawModule : {R : Set r}  RawModule R c 
rawModule = record { ℤero }

------------------------------------------------------------------------
-- Bundles

leftSemimodule : {R : Semiring r ℓr}  LeftSemimodule R c 
leftSemimodule = record { ℤero }

rightSemimodule : {S : Semiring s ℓs}  RightSemimodule S c 
rightSemimodule = record { ℤero }

bisemimodule :
  {R : Semiring r ℓr} {S : Semiring s ℓs}  Bisemimodule R S c 
bisemimodule = record { ℤero }

semimodule : {R : CommutativeSemiring r ℓr}  Semimodule R c 
semimodule = record { ℤero }

leftModule : {R : Ring r ℓr}  LeftModule R c 
leftModule = record { ℤero }

rightModule : {S : Ring s ℓs}  RightModule S c 
rightModule = record { ℤero }

bimodule : {R : Ring r ℓr} {S : Ring s ℓs}  Bimodule R S c 
bimodule = record { ℤero }

⟨module⟩ : {R : CommutativeRing r ℓr}  Module R c 
⟨module⟩ = record { ℤero }