{-# 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_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)