← Back

Modules

CategoricalCrypto

  • CategoricalCrypto
  • Channel.Category
  • Channel.Core
  • Channel.Selection
  • Examples.Basic
  • Examples.Commitment
  • Examples.Signatures
  • Machine.Constraints
  • Machine.Core
  • SFunM

Categories

  • Discrete
  • FreeMonoidal
  • FreeStrictMonoidal
  • GradedKleisli
  • MonoidalCoherence
  • NaturalTransformationHelper
  • Properties

Class

  • Monad.Ext
1234567891011
{-# OPTIONS --cubical-compatible #-}
 
module Class.CommutativeMonoid.Instances where
 
open import Class.CommutativeMonoid.Core
 
open import Data.Nat.Properties
 
module NonUniqueInstances where
CommMonoid-ℕ-+ = Conversion.fromBundle +-0-commutativeMonoid
CommMonoid-ℕ-* = Conversion.fromBundle *-1-commutativeMonoid