{-# 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'_168
                    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._._.Associative
d_Associative_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Associative_206 :: T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Associative_206 = 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_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Idempotent_220 :: T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Idempotent_220 = 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_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Identity_226 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Identity_226 = 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_252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_LeftIdentity_252 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_LeftIdentity_252 = 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_282 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_RightIdentity_282 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_RightIdentity_282 = 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_312 ::
  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_312 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
d_'60''8739''62''45'assoc_312 = 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'_324 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'identity'737'_324 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'identity'737'_324 = 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'_328 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'identity'691'_328 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'identity'691'_328 = 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_332 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''8739''62''45'identity_332 :: T_Level_18 -> T_Level_18 -> T_Σ_14
d_'60''8739''62''45'identity_332 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Σ_14
du_'60''8739''62''45'identity_332
du_'60''8739''62''45'identity_332 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''8739''62''45'identity_332 :: T_Σ_14
du_'60''8739''62''45'identity_332
  = (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_334 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'idem_334 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'idem_334 = T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._._.IsMagma
d_IsMagma_392 :: p -> p -> p -> T_Level_18
d_IsMagma_392 p
a0 p
a1 p
a2 = ()
-- Data.Maybe.Properties._._.IsMonoid
d_IsMonoid_398 :: p -> p -> p -> p -> T_Level_18
d_IsMonoid_398 p
a0 p
a1 p
a2 p
a3 = ()
-- Data.Maybe.Properties._._.IsSemigroup
d_IsSemigroup_420 :: p -> p -> p -> T_Level_18
d_IsSemigroup_420 p
a0 p
a1 p
a2 = ()
-- Data.Maybe.Properties._._.IsMagma.isEquivalence
d_isEquivalence_1692 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_1692 :: T_IsMagma_176 -> T_IsEquivalence_26
d_isEquivalence_1692 T_IsMagma_176
v0
  = (T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (T_IsMagma_176 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_176
v0)
-- Data.Maybe.Properties._._.IsMagma.∙-cong
d_'8729''45'cong_1706 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
  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_1706 :: T_IsMagma_176
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'8729''45'cong_1706 = T_IsMagma_176
-> 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_1802 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_identity_1802 :: T_IsMonoid_686 -> T_Σ_14
d_identity_1802 T_IsMonoid_686
v0
  = (T_IsMonoid_686 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_IsMonoid_686 -> T_Σ_14
MAlonzo.Code.Algebra.Structures.d_identity_698 (T_IsMonoid_686 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_686
v0)
-- Data.Maybe.Properties._._.IsMonoid.isSemigroup
d_isSemigroup_1814 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_isSemigroup_1814 :: T_IsMonoid_686 -> T_IsSemigroup_472
d_isSemigroup_1814 T_IsMonoid_686
v0
  = (T_IsMonoid_686 -> T_IsSemigroup_472)
-> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe T_IsMonoid_686 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (T_IsMonoid_686 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_686
v0)
-- Data.Maybe.Properties._._.IsSemigroup.assoc
d_assoc_2546 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_assoc_2546 :: T_IsSemigroup_472
-> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8801'__12
d_assoc_2546 = T_IsSemigroup_472
-> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Properties._._.IsSemigroup.isMagma
d_isMagma_2550 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_isMagma_2550 :: T_IsSemigroup_472 -> T_IsMagma_176
d_isMagma_2550 T_IsSemigroup_472
v0
  = (T_IsSemigroup_472 -> T_IsMagma_176) -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe T_IsSemigroup_472 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_480 (T_IsSemigroup_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
v0)
-- Data.Maybe.Properties._.<∣>-isMagma
d_'60''8739''62''45'isMagma_2860 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'60''8739''62''45'isMagma_2860 :: T_Level_18 -> T_Level_18 -> T_IsMagma_176
d_'60''8739''62''45'isMagma_2860 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsMagma_176
du_'60''8739''62''45'isMagma_2860
du_'60''8739''62''45'isMagma_2860 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'60''8739''62''45'isMagma_2860 :: T_IsMagma_176
du_'60''8739''62''45'isMagma_2860
  = (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
-- Data.Maybe.Properties._.<∣>-isSemigroup
d_'60''8739''62''45'isSemigroup_2862 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'60''8739''62''45'isSemigroup_2862 :: T_Level_18 -> T_Level_18 -> T_IsSemigroup_472
d_'60''8739''62''45'isSemigroup_2862 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsSemigroup_472
du_'60''8739''62''45'isSemigroup_2862
du_'60''8739''62''45'isSemigroup_2862 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'60''8739''62''45'isSemigroup_2862 :: T_IsSemigroup_472
du_'60''8739''62''45'isSemigroup_2862
  = (T_IsMagma_176
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe
      T_IsMagma_176
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
      (T_IsMagma_176 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_176
du_'60''8739''62''45'isMagma_2860) AgdaAny
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-isMonoid
d_'60''8739''62''45'isMonoid_2864 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_'60''8739''62''45'isMonoid_2864 :: T_Level_18 -> T_Level_18 -> T_IsMonoid_686
d_'60''8739''62''45'isMonoid_2864 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsMonoid_686
du_'60''8739''62''45'isMonoid_2864
du_'60''8739''62''45'isMonoid_2864 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
du_'60''8739''62''45'isMonoid_2864 :: T_IsMonoid_686
du_'60''8739''62''45'isMonoid_2864
  = (T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686)
-> AgdaAny -> AgdaAny -> T_IsMonoid_686
forall a b. a -> b
coe
      T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
      (T_IsSemigroup_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
du_'60''8739''62''45'isSemigroup_2862)
      (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'60''8739''62''45'identity_332)
-- Data.Maybe.Properties._.<∣>-semigroup
d_'60''8739''62''45'semigroup_2866 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_'60''8739''62''45'semigroup_2866 :: T_Level_18 -> T_Level_18 -> T_Semigroup_536
d_'60''8739''62''45'semigroup_2866 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Semigroup_536
du_'60''8739''62''45'semigroup_2866
du_'60''8739''62''45'semigroup_2866 ::
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
du_'60''8739''62''45'semigroup_2866 :: T_Semigroup_536
du_'60''8739''62''45'semigroup_2866
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_472 -> T_Semigroup_536)
-> AgdaAny -> AgdaAny -> T_Semigroup_536
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_472 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793
      ((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_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
du_'60''8739''62''45'isSemigroup_2862)
-- Data.Maybe.Properties._.<∣>-monoid
d_'60''8739''62''45'monoid_2868 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_'60''8739''62''45'monoid_2868 :: T_Level_18 -> T_Level_18 -> T_Monoid_882
d_'60''8739''62''45'monoid_2868 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Monoid_882
du_'60''8739''62''45'monoid_2868
du_'60''8739''62''45'monoid_2868 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_'60''8739''62''45'monoid_2868 :: T_Monoid_882
du_'60''8739''62''45'monoid_2868
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_686 -> T_Monoid_882)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_686 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_16157
      ((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_686 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_686
du_'60''8739''62''45'isMonoid_2864)
-- Data.Maybe.Properties.map-id₂
d_map'45'id'8322'_2870 ::
  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'_2870 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
d_map'45'id'8322'_2870 = 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'_2872 ::
  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'_2872 :: 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'_2872 = 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_2874 ::
  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_2874 :: 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_2874 = 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_2876 ::
  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_2876 :: 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_2876 = 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