{-# 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.Comonad 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.Function.Base

-- Category.Comonad.RawComonad
d_RawComonad_22 :: p -> p -> ()
d_RawComonad_22 p
a0 p
a1 = ()
data T_RawComonad_22
  = C_RawComonad'46'constructor_293 (() -> AgdaAny -> AgdaAny)
                                    (() -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-- Category.Comonad.RawComonad.extract
d_extract_30 :: T_RawComonad_22 -> () -> AgdaAny -> AgdaAny
d_extract_30 :: T_RawComonad_22 -> () -> AgdaAny -> AgdaAny
d_extract_30 T_RawComonad_22
v0
  = case T_RawComonad_22 -> T_RawComonad_22
forall a b. a -> b
coe T_RawComonad_22
v0 of
      C_RawComonad'46'constructor_293 () -> AgdaAny -> AgdaAny
v1 () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v2 -> (() -> AgdaAny -> AgdaAny) -> () -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> AgdaAny -> AgdaAny
v1
      T_RawComonad_22
_ -> () -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Category.Comonad.RawComonad.extend
d_extend_32 ::
  T_RawComonad_22 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_extend_32 :: T_RawComonad_22
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_extend_32 T_RawComonad_22
v0
  = case T_RawComonad_22 -> T_RawComonad_22
forall a b. a -> b
coe T_RawComonad_22
v0 of
      C_RawComonad'46'constructor_293 () -> AgdaAny -> AgdaAny
v1 () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v2 -> (() -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v2
      T_RawComonad_22
_ -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Category.Comonad.RawComonad.duplicate
d_duplicate_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) -> T_RawComonad_22 -> () -> AgdaAny -> AgdaAny
d_duplicate_34 :: () -> (() -> ()) -> T_RawComonad_22 -> () -> AgdaAny -> AgdaAny
d_duplicate_34 ~()
v0 ~() -> ()
v1 T_RawComonad_22
v2 ~()
v3 = T_RawComonad_22 -> AgdaAny -> AgdaAny
du_duplicate_34 T_RawComonad_22
v2
du_duplicate_34 :: T_RawComonad_22 -> AgdaAny -> AgdaAny
du_duplicate_34 :: T_RawComonad_22 -> AgdaAny -> AgdaAny
du_duplicate_34 T_RawComonad_22
v0 = (T_RawComonad_22
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawComonad_22
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_RawComonad_22
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_extend_32 T_RawComonad_22
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased (\ AgdaAny
v1 -> AgdaAny
v1)
-- Category.Comonad.RawComonad.liftW
d_liftW_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawComonad_22 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_liftW_36 :: ()
-> (() -> ())
-> T_RawComonad_22
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_liftW_36 ~()
v0 ~() -> ()
v1 T_RawComonad_22
v2 ~()
v3 ~()
v4 AgdaAny -> AgdaAny
v5 = T_RawComonad_22 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_liftW_36 T_RawComonad_22
v2 AgdaAny -> AgdaAny
v5
du_liftW_36 ::
  T_RawComonad_22 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_liftW_36 :: T_RawComonad_22 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_liftW_36 T_RawComonad_22
v0 AgdaAny -> AgdaAny
v1
  = (T_RawComonad_22
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawComonad_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_RawComonad_22
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_extend_32 T_RawComonad_22
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_RawComonad_22 -> () -> AgdaAny -> AgdaAny)
-> T_RawComonad_22 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawComonad_22 -> () -> AgdaAny -> AgdaAny
d_extract_30 T_RawComonad_22
v0 AgdaAny
forall a. a
erased))
-- Category.Comonad.RawComonad._=>>_
d__'61''62''62'__40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawComonad_22 ->
  () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'61''62''62'__40 :: ()
-> (() -> ())
-> T_RawComonad_22
-> ()
-> ()
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
d__'61''62''62'__40 ~()
v0 ~() -> ()
v1 T_RawComonad_22
v2 ~()
v3 ~()
v4 AgdaAny
v5 AgdaAny -> AgdaAny
v6
  = T_RawComonad_22 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'61''62''62'__40 T_RawComonad_22
v2 AgdaAny
v5 AgdaAny -> AgdaAny
v6
du__'61''62''62'__40 ::
  T_RawComonad_22 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'61''62''62'__40 :: T_RawComonad_22 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'61''62''62'__40 T_RawComonad_22
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = (T_RawComonad_22
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawComonad_22
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_RawComonad_22
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_extend_32 T_RawComonad_22
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny -> AgdaAny
v2 AgdaAny
v1
-- Category.Comonad.RawComonad._=>=_
d__'61''62''61'__42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawComonad_22 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'61''62''61'__42 :: ()
-> (() -> ())
-> T_RawComonad_22
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d__'61''62''61'__42 ~()
v0 ~() -> ()
v1 T_RawComonad_22
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny
v8
  = T_RawComonad_22
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du__'61''62''61'__42 T_RawComonad_22
v2 AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny
v8
du__'61''62''61'__42 ::
  T_RawComonad_22 ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du__'61''62''61'__42 :: T_RawComonad_22
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du__'61''62''61'__42 T_RawComonad_22
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      ((T_RawComonad_22
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawComonad_22
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_RawComonad_22
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_extend_32 T_RawComonad_22
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny -> AgdaAny
v1)
-- Category.Comonad.RawComonad._<<=_
d__'60''60''61'__48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawComonad_22 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''60''61'__48 :: ()
-> (() -> ())
-> T_RawComonad_22
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d__'60''60''61'__48 ~()
v0 ~() -> ()
v1 T_RawComonad_22
v2 ~()
v3 ~()
v4 = T_RawComonad_22 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du__'60''60''61'__48 T_RawComonad_22
v2
du__'60''60''61'__48 ::
  T_RawComonad_22 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du__'60''60''61'__48 :: T_RawComonad_22 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du__'60''60''61'__48 T_RawComonad_22
v0 = (T_RawComonad_22
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawComonad_22
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_RawComonad_22
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_extend_32 T_RawComonad_22
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Category.Comonad.RawComonad._=<=_
d__'61''60''61'__50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawComonad_22 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'61''60''61'__50 :: ()
-> (() -> ())
-> T_RawComonad_22
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d__'61''60''61'__50 ~()
v0 ~() -> ()
v1 T_RawComonad_22
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny
v8
  = T_RawComonad_22
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du__'61''60''61'__50 T_RawComonad_22
v2 AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny
v8
du__'61''60''61'__50 ::
  T_RawComonad_22 ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du__'61''60''61'__50 :: T_RawComonad_22
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du__'61''60''61'__50 T_RawComonad_22
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = (T_RawComonad_22
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawComonad_22
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du__'61''62''61'__42 (T_RawComonad_22 -> AgdaAny
forall a b. a -> b
coe T_RawComonad_22
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)