{-# 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.Category.Functor 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.Builtin.Equality
import qualified MAlonzo.Code.Agda.Primitive

-- Category.Functor.RawFunctor
d_RawFunctor_24 :: p -> p -> p -> ()
d_RawFunctor_24 p
a0 p
a1 p
a2 = ()
newtype T_RawFunctor_24
  = C_RawFunctor'46'constructor_241 (() ->
                                     () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-- Category.Functor.RawFunctor._<$>_
d__'60''36''62'__30 ::
  T_RawFunctor_24 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''36''62'__30 :: T_RawFunctor_24
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''36''62'__30 T_RawFunctor_24
v0
  = case T_RawFunctor_24 -> T_RawFunctor_24
forall a b. a -> b
coe T_RawFunctor_24
v0 of
      C_RawFunctor'46'constructor_241 () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v1 -> (() -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v1
      T_RawFunctor_24
_ -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Category.Functor.RawFunctor._<$_
d__'60''36'__32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawFunctor_24 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'60''36'__32 :: ()
-> ()
-> (() -> ())
-> T_RawFunctor_24
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'60''36'__32 ~()
v0 ~()
v1 ~() -> ()
v2 T_RawFunctor_24
v3 ~()
v4 ~()
v5 AgdaAny
v6 AgdaAny
v7
  = T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny
du__'60''36'__32 T_RawFunctor_24
v3 AgdaAny
v6 AgdaAny
v7
du__'60''36'__32 ::
  T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny
du__'60''36'__32 :: T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny
du__'60''36'__32 T_RawFunctor_24
v0 AgdaAny
v1 AgdaAny
v2
  = (T_RawFunctor_24
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawFunctor_24
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_RawFunctor_24
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''36''62'__30 T_RawFunctor_24
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased (\ AgdaAny
v3 -> AgdaAny
v1) AgdaAny
v2
-- Category.Functor.RawFunctor._<&>_
d__'60''38''62'__38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawFunctor_24 ->
  () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'60''38''62'__38 :: ()
-> ()
-> (() -> ())
-> T_RawFunctor_24
-> ()
-> ()
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
d__'60''38''62'__38 ~()
v0 ~()
v1 ~() -> ()
v2 T_RawFunctor_24
v3 ~()
v4 ~()
v5 AgdaAny
v6 AgdaAny -> AgdaAny
v7
  = T_RawFunctor_24 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'60''38''62'__38 T_RawFunctor_24
v3 AgdaAny
v6 AgdaAny -> AgdaAny
v7
du__'60''38''62'__38 ::
  T_RawFunctor_24 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'60''38''62'__38 :: T_RawFunctor_24 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'60''38''62'__38 T_RawFunctor_24
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = (T_RawFunctor_24
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawFunctor_24
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_RawFunctor_24
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''36''62'__30 T_RawFunctor_24
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny -> AgdaAny
v2 AgdaAny
v1
-- Category.Functor.Morphism
d_Morphism_54 :: p -> p -> p -> p -> p -> p -> p -> ()
d_Morphism_54 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_Morphism_54
  = C_Morphism'46'constructor_3287 (() -> AgdaAny -> AgdaAny)
-- Category.Functor.Morphism.op
d_op_72 :: T_Morphism_54 -> () -> AgdaAny -> AgdaAny
d_op_72 :: T_Morphism_54 -> () -> AgdaAny -> AgdaAny
d_op_72 T_Morphism_54
v0
  = case T_Morphism_54 -> T_Morphism_54
forall a b. a -> b
coe T_Morphism_54
v0 of
      C_Morphism'46'constructor_3287 () -> AgdaAny -> AgdaAny
v1 -> (() -> AgdaAny -> AgdaAny) -> () -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> AgdaAny -> AgdaAny
v1
      T_Morphism_54
_ -> () -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Category.Functor.Morphism.op-<$>
d_op'45''60''36''62'_78 ::
  T_Morphism_54 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_op'45''60''36''62'_78 :: T_Morphism_54
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> T__'8801'__12
d_op'45''60''36''62'_78 = T_Morphism_54
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> T__'8801'__12
forall a. a
erased