{-# 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.Function.Identity.Categorical 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.Category.Applicative.Indexed
import qualified MAlonzo.Code.Category.Comonad
import qualified MAlonzo.Code.Category.Functor
import qualified MAlonzo.Code.Category.Monad.Indexed
import qualified MAlonzo.Code.Function.Base

-- Function.Identity.Categorical.Identity
d_Identity_8 :: MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_Identity_8 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_Identity_8 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Function.Identity.Categorical.functor
d_functor_12 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Category.Functor.T_RawFunctor_24
d_functor_12 :: T_Level_18 -> T_RawFunctor_24
d_functor_12 ~T_Level_18
v0 = T_RawFunctor_24
du_functor_12
du_functor_12 :: MAlonzo.Code.Category.Functor.T_RawFunctor_24
du_functor_12 :: T_RawFunctor_24
du_functor_12
  = ((T_Level_18 -> T_Level_18 -> (Any -> Any) -> Any -> Any)
 -> T_RawFunctor_24)
-> Any -> T_RawFunctor_24
forall a b. a -> b
coe
      (T_Level_18 -> T_Level_18 -> (Any -> Any) -> Any -> Any)
-> T_RawFunctor_24
MAlonzo.Code.Category.Functor.C_RawFunctor'46'constructor_241
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
-- Function.Identity.Categorical.applicative
d_applicative_14 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38
d_applicative_14 :: T_Level_18 -> T_RawIApplicative_38
d_applicative_14 ~T_Level_18
v0 = T_RawIApplicative_38
du_applicative_14
du_applicative_14 ::
  MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38
du_applicative_14 :: T_RawIApplicative_38
du_applicative_14
  = ((T_Level_18 -> Any -> Any -> Any)
 -> (T_Level_18
     -> T_Level_18 -> Any -> Any -> Any -> Any -> Any -> Any)
 -> T_RawIApplicative_38)
-> Any -> Any -> T_RawIApplicative_38
forall a b. a -> b
coe
      (T_Level_18 -> Any -> Any -> Any)
-> (T_Level_18
    -> T_Level_18 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_RawIApplicative_38
MAlonzo.Code.Category.Applicative.Indexed.C_RawIApplicative'46'constructor_815
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2)) ((Any -> Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 Any
v5 -> Any
v5))
-- Function.Identity.Categorical.monad
d_monad_16 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32
d_monad_16 :: T_Level_18 -> T_RawIMonad_32
d_monad_16 ~T_Level_18
v0 = T_RawIMonad_32
du_monad_16
du_monad_16 :: MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32
du_monad_16 :: T_RawIMonad_32
du_monad_16
  = ((T_Level_18 -> Any -> Any -> Any)
 -> (T_Level_18
     -> T_Level_18 -> Any -> Any -> Any -> Any -> (Any -> Any) -> Any)
 -> T_RawIMonad_32)
-> Any -> Any -> T_RawIMonad_32
forall a b. a -> b
coe
      (T_Level_18 -> Any -> Any -> Any)
-> (T_Level_18
    -> T_Level_18 -> Any -> Any -> Any -> Any -> (Any -> Any) -> Any)
-> T_RawIMonad_32
MAlonzo.Code.Category.Monad.Indexed.C_RawIMonad'46'constructor_711
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
      ((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 ->
            (Any -> (Any -> Any) -> Any) -> Any
forall a b. a -> b
coe Any -> (Any -> Any) -> Any
MAlonzo.Code.Function.Base.du__'124''62''8242'__242))
-- Function.Identity.Categorical.comonad
d_comonad_18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Category.Comonad.T_RawComonad_22
d_comonad_18 :: T_Level_18 -> T_RawComonad_22
d_comonad_18 ~T_Level_18
v0 = T_RawComonad_22
du_comonad_18
du_comonad_18 :: MAlonzo.Code.Category.Comonad.T_RawComonad_22
du_comonad_18 :: T_RawComonad_22
du_comonad_18
  = ((T_Level_18 -> Any -> Any)
 -> (T_Level_18 -> T_Level_18 -> (Any -> Any) -> Any -> Any)
 -> T_RawComonad_22)
-> Any -> Any -> T_RawComonad_22
forall a b. a -> b
coe
      (T_Level_18 -> Any -> Any)
-> (T_Level_18 -> T_Level_18 -> (Any -> Any) -> Any -> Any)
-> T_RawComonad_22
MAlonzo.Code.Category.Comonad.C_RawComonad'46'constructor_293
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> Any
v1)) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))