{-# 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 MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties

-- Relation.Binary.PropositionalEquality.Algebra.isMagma
d_isMagma_14 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_isMagma_14 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178
d_isMagma_14 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny -> AgdaAny -> AgdaAny
v2 = T_IsMagma_178
du_isMagma_14
du_isMagma_14 :: MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_isMagma_14 :: T_IsMagma_178
du_isMagma_14
  = (T_IsEquivalence_28
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178)
-> AgdaAny -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.C_constructor_210
      (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
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_74
d_magma_20 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_74
d_magma_20 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_74
du_magma_20 AgdaAny -> AgdaAny -> AgdaAny
v2
du_magma_20 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
du_magma_20 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_74
du_magma_20 AgdaAny -> AgdaAny -> AgdaAny
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178 -> T_Magma_74)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Magma_74
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178 -> T_Magma_74
MAlonzo.Code.Algebra.Bundles.C_constructor_124 AgdaAny -> AgdaAny -> AgdaAny
v0
      (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
du_isMagma_14)