{-# 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.Data.Maybe.Properties 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Maybe.Relation.Unary.All
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Data.Maybe.Properties.just-injective
d_just'45'injective_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_just'45'injective_22 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_just'45'injective_22 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.≡-dec
d_'8801''45'dec_24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8801''45'dec_24 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T_Dec_20
d_'8801''45'dec_24 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_20
v2 Maybe AgdaAny
v3 Maybe AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20
du_'8801''45'dec_24 AgdaAny -> AgdaAny -> T_Dec_20
v2 Maybe AgdaAny
v3 Maybe AgdaAny
v4
du_'8801''45'dec_24 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8801''45'dec_24 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20
du_'8801''45'dec_24 AgdaAny -> AgdaAny -> T_Dec_20
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v3 AgdaAny
v4)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             Maybe AgdaAny
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
             Maybe AgdaAny
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Maybe.Properties.map-id
d_map'45'id_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'id_42 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_map'45'id_42 = T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-id-local
d_map'45'id'45'local_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  MAlonzo.Code.Data.Maybe.Relation.Unary.All.T_All_18 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'id'45'local_52 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
d_map'45'id'45'local_52 = T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-<∣>
d_map'45''60''8739''62'_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45''60''8739''62'_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
d_map'45''60''8739''62'_62 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-cong
d_map'45'cong_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'cong_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T__'8801'__12
d_map'45'cong_78 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-cong-local
d_map'45'cong'45'local_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  MAlonzo.Code.Data.Maybe.Relation.Unary.All.T_All_18 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'cong'45'local_94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
d_map'45'cong'45'local_94 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-injective
d_map'45'injective_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'injective_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_map'45'injective_100 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-∘
d_map'45''8728'_118 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45''8728'_118 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_map'45''8728'_118 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-nothing
d_map'45'nothing_126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'nothing_126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_map'45'nothing_126 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-just
d_map'45'just_134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'just_134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_map'45'just_134 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.maybe-map
d_maybe'45'map_148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (Maybe AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_maybe'45'map_148 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_maybe'45'map_148 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.maybe′-map
d_maybe'8242''45'map_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_maybe'8242''45'map_172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_maybe'8242''45'map_172 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.maybe′-∘
d_maybe'8242''45''8728'_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_maybe'8242''45''8728'_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_maybe'8242''45''8728'_180 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._._.Associative
d_Associative_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Associative_194 :: T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Associative_194 = T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
-- Data.Maybe.Properties._._.Idempotent
d_Idempotent_196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Idempotent_196 :: T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Idempotent_196 = T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
-- Data.Maybe.Properties._._.Identity
d_Identity_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Identity_198 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Identity_198 = T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
-- Data.Maybe.Properties._._.LeftIdentity
d_LeftIdentity_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_LeftIdentity_200 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_LeftIdentity_200 = T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
-- Data.Maybe.Properties._._.RightIdentity
d_RightIdentity_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_RightIdentity_202 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_RightIdentity_202 = T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-assoc
d_'60''8739''62''45'assoc_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'assoc_204 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
d_'60''8739''62''45'assoc_204 = T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-identityˡ
d_'60''8739''62''45'identity'737'_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'identity'737'_216 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'identity'737'_216 = T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-identityʳ
d_'60''8739''62''45'identity'691'_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'identity'691'_220 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'identity'691'_220 = T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-identity
d_'60''8739''62''45'identity_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''8739''62''45'identity_224 :: T_Level_18 -> T_Level_18 -> T_Σ_14
d_'60''8739''62''45'identity_224 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Σ_14
du_'60''8739''62''45'identity_224
du_'60''8739''62''45'identity_224 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''8739''62''45'identity_224 :: T_Σ_14
du_'60''8739''62''45'identity_224
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-idem
d_'60''8739''62''45'idem_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'idem_226 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'idem_226 = T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._._.IsMagma
d_IsMagma_240 :: p -> p -> p -> T_Level_18
d_IsMagma_240 p
a0 p
a1 p
a2 = ()
-- Data.Maybe.Properties._._.IsMonoid
d_IsMonoid_244 :: p -> p -> p -> p -> T_Level_18
d_IsMonoid_244 p
a0 p
a1 p
a2 p
a3 = ()
-- Data.Maybe.Properties._._.IsSemigroup
d_IsSemigroup_248 :: p -> p -> p -> T_Level_18
d_IsSemigroup_248 p
a0 p
a1 p
a2 = ()
-- Data.Maybe.Properties._._.IsMagma.isEquivalence
d_isEquivalence_254 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence_254 :: T_IsMagma_178 -> T_IsEquivalence_28
d_isEquivalence_254 T_IsMagma_178
v0
  = (T_IsMagma_178 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v0)
-- Data.Maybe.Properties._._.IsMagma.∙-cong
d_'8729''45'cong_268 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8729''45'cong_268 :: T_IsMagma_178
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'8729''45'cong_268 = T_IsMagma_178
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._._.IsMonoid.identity
d_identity_278 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_identity_278 :: T_IsMonoid_712 -> T_Σ_14
d_identity_278 T_IsMonoid_712
v0
  = (T_IsMonoid_712 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_IsMonoid_712 -> T_Σ_14
MAlonzo.Code.Algebra.Structures.d_identity_724 (T_IsMonoid_712 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_712
v0)
-- Data.Maybe.Properties._._.IsMonoid.isSemigroup
d_isSemigroup_290 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_isSemigroup_290 :: T_IsMonoid_712 -> T_IsSemigroup_488
d_isSemigroup_290 T_IsMonoid_712
v0
  = (T_IsMonoid_712 -> T_IsSemigroup_488)
-> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe T_IsMonoid_712 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_722 (T_IsMonoid_712 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_712
v0)
-- Data.Maybe.Properties._._.IsSemigroup.assoc
d_assoc_312 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488 ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_assoc_312 :: T_IsSemigroup_488
-> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8801'__12
d_assoc_312 = T_IsSemigroup_488
-> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._._.IsSemigroup.isMagma
d_isMagma_316 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_isMagma_316 :: T_IsSemigroup_488 -> T_IsMagma_178
d_isMagma_316 T_IsSemigroup_488
v0
  = (T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v0)
-- Data.Maybe.Properties._.<∣>-isMagma
d_'60''8739''62''45'isMagma_336 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'60''8739''62''45'isMagma_336 :: T_Level_18 -> T_Level_18 -> T_IsMagma_178
d_'60''8739''62''45'isMagma_336 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsMagma_178
du_'60''8739''62''45'isMagma_336
du_'60''8739''62''45'isMagma_336 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'60''8739''62''45'isMagma_336 :: T_IsMagma_178
du_'60''8739''62''45'isMagma_336
  = (T_IsEquivalence_28
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178)
-> AgdaAny -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.C_constructor_210
      (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
      AgdaAny
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-isSemigroup
d_'60''8739''62''45'isSemigroup_338 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'60''8739''62''45'isSemigroup_338 :: T_Level_18 -> T_Level_18 -> T_IsSemigroup_488
d_'60''8739''62''45'isSemigroup_338 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsSemigroup_488
du_'60''8739''62''45'isSemigroup_338
du_'60''8739''62''45'isSemigroup_338 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'60''8739''62''45'isSemigroup_338 :: T_IsSemigroup_488
du_'60''8739''62''45'isSemigroup_338
  = (T_IsMagma_178
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe
      T_IsMagma_178
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.C_constructor_522
      (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
du_'60''8739''62''45'isMagma_336) AgdaAny
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-isMonoid
d_'60''8739''62''45'isMonoid_340 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
d_'60''8739''62''45'isMonoid_340 :: T_Level_18 -> T_Level_18 -> T_IsMonoid_712
d_'60''8739''62''45'isMonoid_340 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsMonoid_712
du_'60''8739''62''45'isMonoid_340
du_'60''8739''62''45'isMonoid_340 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
du_'60''8739''62''45'isMonoid_340 :: T_IsMonoid_712
du_'60''8739''62''45'isMonoid_340
  = (T_IsSemigroup_488 -> T_Σ_14 -> T_IsMonoid_712)
-> AgdaAny -> AgdaAny -> T_IsMonoid_712
forall a b. a -> b
coe
      T_IsSemigroup_488 -> T_Σ_14 -> T_IsMonoid_712
MAlonzo.Code.Algebra.Structures.C_constructor_758
      (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
du_'60''8739''62''45'isSemigroup_338)
      (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'60''8739''62''45'identity_224)
-- Data.Maybe.Properties._.<∣>-semigroup
d_'60''8739''62''45'semigroup_342 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
d_'60''8739''62''45'semigroup_342 :: T_Level_18 -> T_Level_18 -> T_Semigroup_558
d_'60''8739''62''45'semigroup_342 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Semigroup_558
du_'60''8739''62''45'semigroup_342
du_'60''8739''62''45'semigroup_342 ::
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
du_'60''8739''62''45'semigroup_342 :: T_Semigroup_558
du_'60''8739''62''45'semigroup_342
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_488 -> T_Semigroup_558)
-> AgdaAny -> AgdaAny -> T_Semigroup_558
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488 -> T_Semigroup_558
MAlonzo.Code.Algebra.Bundles.C_constructor_614
      ((Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du__'60''8739''62'__80)
      (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
du_'60''8739''62''45'isSemigroup_338)
-- Data.Maybe.Properties._.<∣>-monoid
d_'60''8739''62''45'monoid_344 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_'60''8739''62''45'monoid_344 :: T_Level_18 -> T_Level_18 -> T_Monoid_914
d_'60''8739''62''45'monoid_344 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Monoid_914
du_'60''8739''62''45'monoid_344
du_'60''8739''62''45'monoid_344 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_'60''8739''62''45'monoid_344 :: T_Monoid_914
du_'60''8739''62''45'monoid_344
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_712 -> T_Monoid_914)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_712 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.C_constructor_990
      ((Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du__'60''8739''62'__80)
      (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
      (T_IsMonoid_712 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_712
du_'60''8739''62''45'isMonoid_340)
-- Data.Maybe.Properties.map-id₂
d_map'45'id'8322'_346 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  MAlonzo.Code.Data.Maybe.Relation.Unary.All.T_All_18 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'id'8322'_346 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
d_map'45'id'8322'_346 = T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-cong₂
d_map'45'cong'8322'_348 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  MAlonzo.Code.Data.Maybe.Relation.Unary.All.T_All_18 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'cong'8322'_348 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
d_map'45'cong'8322'_348 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-compose
d_map'45'compose_350 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'compose_350 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_map'45'compose_350 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties.map-<∣>-commute
d_map'45''60''8739''62''45'commute_352 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45''60''8739''62''45'commute_352 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
d_map'45''60''8739''62''45'commute_352 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased