{-# 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.Relation.Binary.Construct.Add.Point.Equality 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.Primitive
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Binary.Construct.Add.Point.Equality._≈∙_
d__'8776''8729'__20 :: p -> p -> p -> p -> p -> p -> ()
d__'8776''8729'__20 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T__'8776''8729'__20
  = C_'8729''8776''8729'_22 | C_'91'_'93'_28 AgdaAny
-- Relation.Binary.Construct.Add.Point.Equality.[≈]-injective
d_'91''8776''93''45'injective_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> T__'8776''8729'__20 -> AgdaAny
d_'91''8776''93''45'injective_34 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'8776''8729'__20
-> AgdaAny
d_'91''8776''93''45'injective_34 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~AgdaAny
v4 ~AgdaAny
v5 T__'8776''8729'__20
v6
  = T__'8776''8729'__20 -> AgdaAny
du_'91''8776''93''45'injective_34 T__'8776''8729'__20
v6
du_'91''8776''93''45'injective_34 :: T__'8776''8729'__20 -> AgdaAny
du_'91''8776''93''45'injective_34 :: T__'8776''8729'__20 -> AgdaAny
du_'91''8776''93''45'injective_34 T__'8776''8729'__20
v0
  = case T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v0 of
      C_'91'_'93'_28 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
      T__'8776''8729'__20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Point.Equality.≈∙-refl
d_'8776''8729''45'refl_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20
d_'8776''8729''45'refl_38 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8776''8729'__20
d_'8776''8729''45'refl_38 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5
  = (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20
du_'8776''8729''45'refl_38 AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5
du_'8776''8729''45'refl_38 ::
  (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20
du_'8776''8729''45'refl_38 :: (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20
du_'8776''8729''45'refl_38 AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v2
        -> (AgdaAny -> T__'8776''8729'__20) -> AgdaAny -> T__'8776''8729'__20
forall a b. a -> b
coe AgdaAny -> T__'8776''8729'__20
C_'91'_'93'_28 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2)
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
C_'8729''8776''8729'_22
      Maybe AgdaAny
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Point.Equality.≈∙-sym
d_'8776''8729''45'sym_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8776''8729'__20
d_'8776''8729''45'sym_46 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_'8776''8729''45'sym_46 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6 T__'8776''8729'__20
v7
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''8729''45'sym_46 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6 T__'8776''8729'__20
v7
du_'8776''8729''45'sym_46 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8776''8729'__20
du_'8776''8729''45'sym_46 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''8729''45'sym_46 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 T__'8776''8729'__20
v3
  = case T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v3 of
      T__'8776''8729'__20
C_'8729''8776''8729'_22 -> T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v3
      C_'91'_'93'_28 AgdaAny
v6
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v7
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v8
                      -> (AgdaAny -> T__'8776''8729'__20) -> AgdaAny -> T__'8776''8729'__20
forall a b. a -> b
coe AgdaAny -> T__'8776''8729'__20
C_'91'_'93'_28 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v7 AgdaAny
v8 AgdaAny
v6)
                    Maybe AgdaAny
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8776''8729'__20
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Point.Equality.≈∙-trans
d_'8776''8729''45'trans_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8776''8729'__20 -> T__'8776''8729'__20 -> T__'8776''8729'__20
d_'8776''8729''45'trans_54 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_'8776''8729''45'trans_54 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6 Maybe AgdaAny
v7 T__'8776''8729'__20
v8 T__'8776''8729'__20
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''8729''45'trans_54 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6 Maybe AgdaAny
v7 T__'8776''8729'__20
v8 T__'8776''8729'__20
v9
du_'8776''8729''45'trans_54 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8776''8729'__20 -> T__'8776''8729'__20 -> T__'8776''8729'__20
du_'8776''8729''45'trans_54 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''8729''45'trans_54 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2 Maybe AgdaAny
v3 T__'8776''8729'__20
v4 T__'8776''8729'__20
v5
  = case T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v4 of
      T__'8776''8729'__20
C_'8729''8776''8729'_22 -> T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v5
      C_'91'_'93'_28 AgdaAny
v8
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v9
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v10
                      -> case T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v5 of
                           C_'91'_'93'_28 AgdaAny
v13
                             -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v3 of
                                  MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v14
                                    -> (AgdaAny -> T__'8776''8729'__20) -> AgdaAny -> T__'8776''8729'__20
forall a b. a -> b
coe AgdaAny -> T__'8776''8729'__20
C_'91'_'93'_28 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v9 AgdaAny
v10 AgdaAny
v14 AgdaAny
v8 AgdaAny
v13)
                                  Maybe AgdaAny
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T__'8776''8729'__20
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    Maybe AgdaAny
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8776''8729'__20
_ -> T__'8776''8729'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Point.Equality.≈∙-dec
d_'8776''8729''45'dec_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8776''8729''45'dec_66 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T_Dec_32
d_'8776''8729''45'dec_66 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
  = (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8776''8729''45'dec_66 AgdaAny -> AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5 Maybe AgdaAny
v6
du_'8776''8729''45'dec_66 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8776''8729''45'dec_66 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8776''8729''45'dec_66 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 -> T__'8776''8729'__20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8776''8729'__20
C_'91'_'93'_28) ((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
                       (T__'8776''8729'__20 -> AgdaAny
forall a b. a -> b
coe T__'8776''8729'__20
C_'8729''8776''8729'_22))
             Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Point.Equality.≈∙-irrelevant
d_'8776''8729''45'irrelevant_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  Maybe AgdaAny ->
  Maybe AgdaAny ->
  T__'8776''8729'__20 ->
  T__'8776''8729'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''8729''45'irrelevant_84 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8801'__12
d_'8776''8729''45'irrelevant_84 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.Construct.Add.Point.Equality.≈∙-substitutive
d_'8776''8729''45'substitutive_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  ((AgdaAny -> ()) ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (Maybe AgdaAny -> ()) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> T__'8776''8729'__20 -> AgdaAny -> AgdaAny
d_'8776''8729''45'substitutive_96 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ((AgdaAny -> ())
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe AgdaAny -> ())
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
d_'8776''8729''45'substitutive_96 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 Maybe AgdaAny -> ()
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8
                                  T__'8776''8729'__20
v9
  = ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe AgdaAny -> ())
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
du_'8776''8729''45'substitutive_96 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 Maybe AgdaAny -> ()
v6 Maybe AgdaAny
v7 Maybe AgdaAny
v8 T__'8776''8729'__20
v9
du_'8776''8729''45'substitutive_96 ::
  ((AgdaAny -> ()) ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (Maybe AgdaAny -> ()) ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> T__'8776''8729'__20 -> AgdaAny -> AgdaAny
du_'8776''8729''45'substitutive_96 :: ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe AgdaAny -> ())
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
du_'8776''8729''45'substitutive_96 (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny -> ()
v1 Maybe AgdaAny
v2 Maybe AgdaAny
v3 T__'8776''8729'__20
v4
  = case T__'8776''8729'__20 -> T__'8776''8729'__20
forall a b. a -> b
coe T__'8776''8729'__20
v4 of
      T__'8776''8729'__20
C_'8729''8776''8729'_22 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 -> AgdaAny
v5)
      C_'91'_'93'_28 AgdaAny
v7
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v8
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v3 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v9
                      -> ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           (AgdaAny -> ())
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0
                           (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226 ((Maybe AgdaAny -> ()) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> ()
v1)
                              ((AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16))
                           AgdaAny
v8 AgdaAny
v9 AgdaAny
v7
                    Maybe AgdaAny
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             Maybe AgdaAny
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8776''8729'__20
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Add.Point.Equality.≈∙-isEquivalence
d_'8776''8729''45'isEquivalence_108 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'8776''8729''45'isEquivalence_108 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsEquivalence_26
-> T_IsEquivalence_26
d_'8776''8729''45'isEquivalence_108 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsEquivalence_26
v4
  = T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8776''8729''45'isEquivalence_108 T_IsEquivalence_26
v4
du_'8776''8729''45'isEquivalence_108 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_'8776''8729''45'isEquivalence_108 :: T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8776''8729''45'isEquivalence_108 T_IsEquivalence_26
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
      (((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20
du_'8776''8729''45'refl_38
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> T__'8776''8729'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''8729''45'sym_46
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> T__'8776''8729'__20
 -> T__'8776''8729'__20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''8729''45'trans_54
         ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)))
-- Relation.Binary.Construct.Add.Point.Equality.≈∙-isDecEquivalence
d_'8776''8729''45'isDecEquivalence_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_'8776''8729''45'isDecEquivalence_128 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
d_'8776''8729''45'isDecEquivalence_128 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_IsDecEquivalence_44
v4
  = T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8776''8729''45'isDecEquivalence_128 T_IsDecEquivalence_44
v4
du_'8776''8729''45'isDecEquivalence_128 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
du_'8776''8729''45'isDecEquivalence_128 :: T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8776''8729''45'isDecEquivalence_128 T_IsDecEquivalence_44
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3075
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8776''8729''45'isEquivalence_108
         ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
            (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8776''8729''45'dec_66
         ((T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (T_IsDecEquivalence_44 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_44
v0)))