{-# 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
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- 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.T_Dec_32) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8801''45'dec_24 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T_Dec_32
d_'8801''45'dec_24 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 Maybe AgdaAny
v3 Maybe AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8801''45'dec_24 AgdaAny -> AgdaAny -> T_Dec_32
v2 Maybe AgdaAny
v3 Maybe AgdaAny
v4
du_'8801''45'dec_24 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8801''45'dec_24 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8801''45'dec_24 AgdaAny -> AgdaAny -> T_Dec_32
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) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v3 AgdaAny
v4)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
             Maybe AgdaAny
_ -> T_Dec_32
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_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
             Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
               -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
forall a. a
erased)
             Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
_ -> T_Dec_32
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₂
d_map'45'id'8322'_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'8322'_52 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
d_map'45'id'8322'_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-<∣>-commute
d_map'45''60''8739''62''45'commute_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''45'commute_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''45'commute_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₂
d_map'45'cong'8322'_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'8322'_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'8322'_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-compose
d_map'45'compose_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'compose_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'compose_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_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Associative_202 :: T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Associative_202 = 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_218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Identity_218 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Identity_218 = 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_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_LeftIdentity_232 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_LeftIdentity_232 = 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_244 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny ->
  (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_RightIdentity_244 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_RightIdentity_244 = 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_254 ::
  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_254 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
d_'60''8739''62''45'assoc_254 = 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'_266 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'identity'737'_266 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'identity'737'_266 = 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'_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'identity'691'_270 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'identity'691'_270 = 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_274 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''8739''62''45'identity_274 :: T_Level_18 -> T_Level_18 -> T_Σ_14
d_'60''8739''62''45'identity_274 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Σ_14
du_'60''8739''62''45'identity_274
du_'60''8739''62''45'identity_274 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''8739''62''45'identity_274 :: T_Σ_14
du_'60''8739''62''45'identity_274
  = (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._._.IsMagma
d_IsMagma_316 :: p -> p -> p -> T_Level_18
d_IsMagma_316 p
a0 p
a1 p
a2 = ()
-- Data.Maybe.Properties._._.IsMonoid
d_IsMonoid_318 :: p -> p -> p -> p -> T_Level_18
d_IsMonoid_318 p
a0 p
a1 p
a2 p
a3 = ()
-- Data.Maybe.Properties._._.IsSemigroup
d_IsSemigroup_326 :: p -> p -> p -> T_Level_18
d_IsSemigroup_326 p
a0 p
a1 p
a2 = ()
-- Data.Maybe.Properties._.<∣>-isMagma
d_'60''8739''62''45'isMagma_1708 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'60''8739''62''45'isMagma_1708 :: T_Level_18 -> T_Level_18 -> T_IsMagma_86
d_'60''8739''62''45'isMagma_1708 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsMagma_86
du_'60''8739''62''45'isMagma_1708
du_'60''8739''62''45'isMagma_1708 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'60''8739''62''45'isMagma_1708 :: T_IsMagma_86
du_'60''8739''62''45'isMagma_1708
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      AgdaAny
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-isSemigroup
d_'60''8739''62''45'isSemigroup_1710 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'60''8739''62''45'isSemigroup_1710 :: T_Level_18 -> T_Level_18 -> T_IsSemigroup_194
d_'60''8739''62''45'isSemigroup_1710 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710
du_'60''8739''62''45'isSemigroup_1710 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710 :: T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710
  = (T_IsMagma_86
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
      (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
du_'60''8739''62''45'isMagma_1708) AgdaAny
forall a. a
erased
-- Data.Maybe.Properties._.<∣>-isMonoid
d_'60''8739''62''45'isMonoid_1712 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_'60''8739''62''45'isMonoid_1712 :: T_Level_18 -> T_Level_18 -> T_IsMonoid_358
d_'60''8739''62''45'isMonoid_1712 ~T_Level_18
v0 ~T_Level_18
v1
  = T_IsMonoid_358
du_'60''8739''62''45'isMonoid_1712
du_'60''8739''62''45'isMonoid_1712 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
du_'60''8739''62''45'isMonoid_1712 :: T_IsMonoid_358
du_'60''8739''62''45'isMonoid_1712
  = (T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny -> T_IsMonoid_358
forall a b. a -> b
coe
      T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_7687
      (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710)
      (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'60''8739''62''45'identity_274)
-- Data.Maybe.Properties._.<∣>-semigroup
d_'60''8739''62''45'semigroup_1714 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_'60''8739''62''45'semigroup_1714 :: T_Level_18 -> T_Level_18 -> T_Semigroup_206
d_'60''8739''62''45'semigroup_1714 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Semigroup_206
du_'60''8739''62''45'semigroup_1714
du_'60''8739''62''45'semigroup_1714 ::
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_'60''8739''62''45'semigroup_1714 :: T_Semigroup_206
du_'60''8739''62''45'semigroup_1714
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_194 -> T_Semigroup_206)
-> AgdaAny -> AgdaAny -> T_Semigroup_206
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> T_Semigroup_206
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_3669
      ((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'__84)
      (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710)
-- Data.Maybe.Properties._.<∣>-monoid
d_'60''8739''62''45'monoid_1716 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'60''8739''62''45'monoid_1716 :: T_Level_18 -> T_Level_18 -> T_Monoid_506
d_'60''8739''62''45'monoid_1716 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Monoid_506
du_'60''8739''62''45'monoid_1716
du_'60''8739''62''45'monoid_1716 ::
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'60''8739''62''45'monoid_1716 :: T_Monoid_506
du_'60''8739''62''45'monoid_1716
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_358 -> T_Monoid_506)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_358 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_8851
      ((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'__84)
      (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_358 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_358
du_'60''8739''62''45'isMonoid_1712)