{-# 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_86
d_isMagma_14 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86
d_isMagma_14 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny -> AgdaAny -> AgdaAny
v2 = T_IsMagma_86
du_isMagma_14
du_isMagma_14 :: MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_isMagma_14 :: T_IsMagma_86
du_isMagma_14
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      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_36
d_magma_20 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_36
d_magma_20 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_36
du_magma_20 AgdaAny -> AgdaAny -> AgdaAny
v2
du_magma_20 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
du_magma_20 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Magma_36
du_magma_20 AgdaAny -> AgdaAny -> AgdaAny
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86 -> T_Magma_36)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Magma_36
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86 -> T_Magma_36
MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_581 AgdaAny -> AgdaAny -> AgdaAny
v0
      (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
du_isMagma_14)