{-# 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 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176
d_isMagma_14 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny -> AgdaAny -> AgdaAny
v2 = T_IsMagma_176
du_isMagma_14
du_isMagma_14 :: MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_isMagma_14 :: T_IsMagma_176
du_isMagma_14
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_176)
-> AgdaAny -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
      AgdaAny
forall a. a
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 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_68
d_magma_20 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_68
du_magma_20 AgdaAny -> AgdaAny -> AgdaAny
v2
du_magma_20 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_68
du_magma_20 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_68
du_magma_20 AgdaAny -> AgdaAny -> AgdaAny
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176 -> T_Magma_68)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Magma_68
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176 -> T_Magma_68
MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279 AgdaAny -> AgdaAny -> AgdaAny
v0
      (T_IsMagma_176 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_176
du_isMagma_14)