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

-- Relation.Binary.Construct.Add.Extrema.Equality.Inf._≈∙_
d__'8776''8729'__22 :: p -> p -> p -> p -> p -> p -> ()
d__'8776''8729'__22 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.Add.Extrema.Equality.Sup._≈∙_
d__'8776''8729'__54 :: p -> p -> p -> p -> p -> p -> ()
d__'8776''8729'__54 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.Add.Extrema.Equality.[≈]-injective
d_'91''8776''93''45'injective_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  AgdaAny
d_'91''8776''93''45'injective_96 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'8776''8729'__20
-> AgdaAny
d_'91''8776''93''45'injective_96 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~AgdaAny
v4 ~AgdaAny
v5
  = T__'8776''8729'__20 -> AgdaAny
du_'91''8776''93''45'injective_96
du_'91''8776''93''45'injective_96 ::
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  AgdaAny
du_'91''8776''93''45'injective_96 :: T__'8776''8729'__20 -> AgdaAny
du_'91''8776''93''45'injective_96
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8776''8729'__20 -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      ((T__'8776''8729'__20 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         T__'8776''8729'__20 -> AgdaAny
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'91''8776''93''45'injective_34)
      ((T__'8776''8729'__20 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         T__'8776''8729'__20 -> AgdaAny
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'91''8776''93''45'injective_34)
-- Relation.Binary.Construct.Add.Extrema.Equality.≈±-refl
d_'8776''177''45'refl_98 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_'8776''177''45'refl_98 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_'8776''177''45'refl_98 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
  = (AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_'8776''177''45'refl_98
du_'8776''177''45'refl_98 ::
  (AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_'8776''177''45'refl_98 :: (AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_'8776''177''45'refl_98
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      (((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20)
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'refl_38)
      (((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20)
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'refl_38)
-- Relation.Binary.Construct.Add.Extrema.Equality.≈±-sym
d_'8776''177''45'sym_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_'8776''177''45'sym_100 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_'8776''177''45'sym_100 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''177''45'sym_100
du_'8776''177''45'sym_100 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_'8776''177''45'sym_100 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''177''45'sym_100
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> T__'8776''8729'__20)
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'sym_46)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> T__'8776''8729'__20)
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'sym_46)
-- Relation.Binary.Construct.Add.Extrema.Equality.≈±-trans
d_'8776''177''45'trans_102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_'8776''177''45'trans_102 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_'8776''177''45'trans_102 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''177''45'trans_102
du_'8776''177''45'trans_102 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_'8776''177''45'trans_102 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_'8776''177''45'trans_102
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8776''8729'__20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      (((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
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
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.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)
-> 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
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'trans_54)
-- Relation.Binary.Construct.Add.Extrema.Equality.≈±-dec
d_'8776''177''45'dec_104 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8776''177''45'dec_104 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Dec_20
d_'8776''177''45'dec_104 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
  = (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe (Maybe AgdaAny) -> Maybe (Maybe AgdaAny) -> T_Dec_20
du_'8776''177''45'dec_104
du_'8776''177''45'dec_104 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8776''177''45'dec_104 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe (Maybe AgdaAny) -> Maybe (Maybe AgdaAny) -> T_Dec_20
du_'8776''177''45'dec_104
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Dec_20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20)
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'dec_66)
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20)
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'dec_66)
-- Relation.Binary.Construct.Add.Extrema.Equality.≈±-irrelevant
d_'8776''177''45'irrelevant_106 ::
  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 (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''177''45'irrelevant_106 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8801'__12
d_'8776''177''45'irrelevant_106 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.Construct.Add.Extrema.Equality.≈±-substitutive
d_'8776''177''45'substitutive_110 ::
  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 (Maybe AgdaAny) -> ()) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  AgdaAny -> AgdaAny
d_'8776''177''45'substitutive_110 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> ((AgdaAny -> ())
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe (Maybe AgdaAny) -> ())
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
d_'8776''177''45'substitutive_110 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4
  = ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe (Maybe AgdaAny) -> ())
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
du_'8776''177''45'substitutive_110
du_'8776''177''45'substitutive_110 ::
  ((AgdaAny -> ()) ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (Maybe (Maybe AgdaAny) -> ()) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  AgdaAny -> AgdaAny
du_'8776''177''45'substitutive_110 :: ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe (Maybe AgdaAny) -> ())
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
du_'8776''177''45'substitutive_110
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> ((AgdaAny -> ())
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe (Maybe AgdaAny) -> ())
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      ((((AgdaAny -> ())
  -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (Maybe AgdaAny -> ())
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe AgdaAny -> ())
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'substitutive_96)
      ((((AgdaAny -> ())
  -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (Maybe AgdaAny -> ())
 -> Maybe AgdaAny
 -> Maybe AgdaAny
 -> T__'8776''8729'__20
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         ((AgdaAny -> ())
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (Maybe AgdaAny -> ())
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8776''8729'__20
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'substitutive_96)
-- Relation.Binary.Construct.Add.Extrema.Equality.≈±-isEquivalence
d_'8776''177''45'isEquivalence_112 ::
  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''177''45'isEquivalence_112 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsEquivalence_26
-> T_IsEquivalence_26
d_'8776''177''45'isEquivalence_112 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
  = T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8776''177''45'isEquivalence_112
du_'8776''177''45'isEquivalence_112 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_'8776''177''45'isEquivalence_112 :: T_IsEquivalence_26 -> T_IsEquivalence_26
du_'8776''177''45'isEquivalence_112
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'isEquivalence_108)
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'isEquivalence_108)
-- Relation.Binary.Construct.Add.Extrema.Equality.≈±-isDecEquivalence
d_'8776''177''45'isDecEquivalence_114 ::
  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''177''45'isDecEquivalence_114 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
d_'8776''177''45'isDecEquivalence_114 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3
  = T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8776''177''45'isDecEquivalence_114
du_'8776''177''45'isDecEquivalence_114 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
du_'8776''177''45'isDecEquivalence_114 :: T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
du_'8776''177''45'isDecEquivalence_114
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsDecEquivalence_44
-> T_IsDecEquivalence_44
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      ((T_IsDecEquivalence_44 -> T_IsDecEquivalence_44) -> AgdaAny
forall a b. a -> b
coe
         T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'isDecEquivalence_128)
      ((T_IsDecEquivalence_44 -> T_IsDecEquivalence_44) -> AgdaAny
forall a b. a -> b
coe
         T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.du_'8776''8729''45'isDecEquivalence_128)