content: {-# LANGUAGE BangPatterns              #-}
  {-# LANGUAGE EmptyCase                 #-}
  {-# LANGUAGE EmptyDataDecls            #-}
  {-# LANGUAGE ExistentialQuantification #-}
  {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE OverloadedStrings         #-}
  {-# LANGUAGE PatternSynonyms           #-}
  {-# LANGUAGE RankNTypes                #-}
  {-# LANGUAGE ScopedTypeVariables       #-}
  
  {-# OPTIONS_GHC -Wno-overlapping-patterns #-}
  
  module MAlonzo.Code.Relation.Binary.PropositionalEquality.Algebra where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Algebra.Bundles qualified
  import MAlonzo.Code.Algebra.Structures qualified
  import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Relation.Binary.PropositionalEquality.Algebra.isMagma
  d_isMagma_14 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_14 ~v0 ~v1 ~v2 = du_isMagma_14
  du_isMagma_14 :: MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  du_isMagma_14
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
        erased
  -- Relation.Binary.PropositionalEquality.Algebra.magma
  d_magma_20 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Bundles.T_Magma_68
  d_magma_20 ~v0 ~v1 v2 = du_magma_20 v2
  du_magma_20 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Bundles.T_Magma_68
  du_magma_20 v0
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279 v0
        (coe du_isMagma_14)
  