content: {-# 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.Sum.Properties where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Bool qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.Sum.Base qualified
  import MAlonzo.Code.Function.Bundles qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
  import MAlonzo.Code.Relation.Nullary.Reflects qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Data.Sum.Properties.inj₁-injective
  d_inj'8321''45'injective_34 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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_inj'8321''45'injective_34 = erased
  -- Data.Sum.Properties.inj₂-injective
  d_inj'8322''45'injective_40 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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_inj'8322''45'injective_40 = erased
  -- Data.Sum.Properties._.≡-dec
  d_'8801''45'dec_54 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_'8801''45'dec_54 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
    = du_'8801''45'dec_54 v4 v5 v6 v7
  du_'8801''45'dec_54 ::
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_'8801''45'dec_54 v0 v1 v2 v3
    = case coe v2 of
        MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 v4
          -> case coe v3 of
               MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 v5
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                      erased erased (coe v0 v4 v5)
               MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 v5
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 v4
          -> case coe v3 of
               MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 v5
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 v5
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                      erased erased (coe v1 v4 v5)
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.Sum.Properties.swap-involutive
  d_swap'45'involutive_72 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_swap'45'involutive_72 = erased
  -- Data.Sum.Properties.swap-↔
  d_swap'45''8596'_78 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
  d_swap'45''8596'_78 ~v0 ~v1 ~v2 ~v3 = du_swap'45''8596'_78
  du_swap'45''8596'_78 ::
    MAlonzo.Code.Function.Bundles.T_Inverse_1960
  du_swap'45''8596'_78
    = coe
        MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
        (coe MAlonzo.Code.Data.Sum.Base.du_swap_78)
        (coe MAlonzo.Code.Data.Sum.Base.du_swap_78)
  -- Data.Sum.Properties.map-id
  d_map'45'id_80 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'id_80 = erased
  -- Data.Sum.Properties.[,]-∘
  d_'91''44''93''45''8728'_88 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'91''44''93''45''8728'_88 = erased
  -- Data.Sum.Properties.[,]-map
  d_'91''44''93''45'map_98 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'91''44''93''45'map_98 = erased
  -- Data.Sum.Properties.map-map
  d_map'45'map_108 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'map_108 = erased
  -- Data.Sum.Properties.map₁₂-map₂₁
  d_map'8321''8322''45'map'8322''8321'_114 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'8321''8322''45'map'8322''8321'_114 = erased
  -- Data.Sum.Properties.map-assocˡ
  d_map'45'assoc'737'_122 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'assoc'737'_122 = erased
  -- Data.Sum.Properties.map-assocʳ
  d_map'45'assoc'691'_136 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'assoc'691'_136 = erased
  -- Data.Sum.Properties.[,]-cong
  d_'91''44''93''45'cong_152 ::
    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 -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'91''44''93''45'cong_152 = erased
  -- Data.Sum.Properties.[-,]-cong
  d_'91''45''44''93''45'cong_160 ::
    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 -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'91''45''44''93''45'cong_160 = erased
  -- Data.Sum.Properties.[,-]-cong
  d_'91''44''45''93''45'cong_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 -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'91''44''45''93''45'cong_172 = erased
  -- Data.Sum.Properties.map-cong
  d_map'45'cong_186 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'cong_186 = erased
  -- Data.Sum.Properties.map₁-cong
  d_map'8321''45'cong_204 ::
    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 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'8321''45'cong_204 = erased
  -- Data.Sum.Properties.map₂-cong
  d_map'8322''45'cong_212 ::
    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 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'8322''45'cong_212 = erased
  -- Data.Sum.Properties.[,]-∘-distr
  d_'91''44''93''45''8728''45'distr_216 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'91''44''93''45''8728''45'distr_216 = erased
  -- Data.Sum.Properties.[,]-map-commute
  d_'91''44''93''45'map'45'commute_218 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'91''44''93''45'map'45'commute_218 = erased
  -- Data.Sum.Properties.map-commute
  d_map'45'commute_220 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'commute_220 = erased
  -- Data.Sum.Properties.map₁₂-commute
  d_map'8321''8322''45'commute_222 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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) ->
    MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'8321''8322''45'commute_222 = erased
  