{-# 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.NaturalOrder.Left 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Binary.Construct.NaturalOrder.Left._.Commutative
d_Commutative_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Commutative_48 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Commutative_48 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.NaturalOrder.Left._.Idempotent
d_Idempotent_58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Idempotent_58 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Idempotent_58 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.NaturalOrder.Left._.Selective
d_Selective_130 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Selective_130 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Selective_130 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.NaturalOrder.Left._.IsBand
d_IsBand_160 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsBand_160 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.NaturalOrder.Left._.IsMagma
d_IsMagma_240 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsMagma_240 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.NaturalOrder.Left._.IsSemigroup
d_IsSemigroup_296 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsSemigroup_296 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.NaturalOrder.Left._.IsBand.idem
d_idem_424 ::
  MAlonzo.Code.Algebra.Structures.T_IsBand_526 -> AgdaAny -> AgdaAny
d_idem_424 :: T_IsBand_526 -> AgdaAny -> AgdaAny
d_idem_424 T_IsBand_526
v0
  = (T_IsBand_526 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_526 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_536 (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v0)
-- Relation.Binary.Construct.NaturalOrder.Left._.IsBand.isSemigroup
d_isSemigroup_432 ::
  MAlonzo.Code.Algebra.Structures.T_IsBand_526 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_isSemigroup_432 :: T_IsBand_526 -> T_IsSemigroup_488
d_isSemigroup_432 T_IsBand_526
v0
  = (T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534 (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v0)
-- Relation.Binary.Construct.NaturalOrder.Left._.IsMagma.isEquivalence
d_isEquivalence_1592 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence_1592 :: T_IsMagma_178 -> T_IsEquivalence_28
d_isEquivalence_1592 T_IsMagma_178
v0
  = (T_IsMagma_178 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v0)
-- Relation.Binary.Construct.NaturalOrder.Left._.IsMagma.∙-cong
d_'8729''45'cong_1606 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'cong_1606 :: T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8729''45'cong_1606 T_IsMagma_178
v0
  = (T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v0)
-- Relation.Binary.Construct.NaturalOrder.Left._.IsSemigroup.assoc
d_assoc_2448 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_assoc_2448 :: T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_assoc_2448 T_IsSemigroup_488
v0
  = (T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_498 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v0)
-- Relation.Binary.Construct.NaturalOrder.Left._.IsSemigroup.isMagma
d_isMagma_2452 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_isMagma_2452 :: T_IsSemigroup_488 -> T_IsMagma_178
d_isMagma_2452 T_IsSemigroup_488
v0
  = (T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v0)
-- Relation.Binary.Construct.NaturalOrder.Left._.IsSemilattice
d_IsSemilattice_2796 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_IsSemilattice_2796 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_IsSemilattice_2796 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.NaturalOrder.Left._≤_
d__'8804'__3202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d__'8804'__3202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8804'__3202 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.NaturalOrder.Left.reflexive
d_reflexive_3208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_3208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_3208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_178
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_3208 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_178
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_reflexive_3208 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_3208 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_3208 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsMagma_178
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v8)
      AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
         AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4)
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4)
            (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
               (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                  ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                     ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4))
            ((T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188 T_IsMagma_178
v1 AgdaAny
v3 AgdaAny
v3 AgdaAny
v3 AgdaAny
v4
               ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                  (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> T_IsMagma_178
forall a b. a -> b
coe T_IsMagma_178
v1)) AgdaAny
v3)
               AgdaAny
v5))
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> T_IsMagma_178
forall a b. a -> b
coe T_IsMagma_178
v1))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3) AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)))
-- Relation.Binary.Construct.NaturalOrder.Left.refl
d_refl_3286 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_refl_3286 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_refl_3286 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_refl_3286 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_refl_3286 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_refl_3286 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_refl_3286 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3) AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Construct.NaturalOrder.Left.antisym
d_antisym_3294 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_3294 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antisym_3294 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_28
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antisym_3294 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_28
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_antisym_3294 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_3294 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antisym_3294 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsEquivalence_28
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v9)
      AgdaAny
v3 AgdaAny
v4
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
         AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4) AgdaAny
v4
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v3) AgdaAny
v4
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v3) AgdaAny
v4 AgdaAny
v4
               (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                     ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
               ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38 T_IsEquivalence_28
v1 AgdaAny
v4
                  ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v3) AgdaAny
v6))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4))
         AgdaAny
v5)
-- Relation.Binary.Construct.NaturalOrder.Left.total
d_total_3364 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_total_3364 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_total_3364 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T__'8846'__30
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_total_3364 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T__'8846'__30
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_total_3364 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_total_3364 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_total_3364 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> T__'8846'__30
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v6) AgdaAny
v5)
      (\ AgdaAny
v7 ->
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v6 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v6) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v6 AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v6) AgdaAny
v6 AgdaAny
v7)
           ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6))
      ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v3 AgdaAny
v5 AgdaAny
v6)
-- Relation.Binary.Construct.NaturalOrder.Left.trans
d_trans_3380 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_3380 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_3380 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemigroup_488
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_trans_3380 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemigroup_488
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_trans_3380 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_3380 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_trans_3380 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemigroup_488
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v9)
      AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))))
         AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4)
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                     ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4)
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                     ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                        ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v4)
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4)
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                     ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                        ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                           ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))))
                  ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v4) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4)
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                     (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                        ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                           ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                              ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))))
                     ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4))
                  ((T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188
                     (T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> T_IsSemigroup_488
forall a b. a -> b
coe T_IsSemigroup_488
v1))
                     ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v2 AgdaAny
v4 AgdaAny
v4
                     ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
                        (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                           ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))
                        AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v5)
                     ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                        (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                           ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))
                        AgdaAny
v4)))
               ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
                  (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                     ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))
                  ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v4) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4))
                  ((T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_498 T_IsSemigroup_488
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4)))
            ((T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188
               (T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> T_IsSemigroup_488
forall a b. a -> b
coe T_IsSemigroup_488
v1)) AgdaAny
v2 AgdaAny
v2 AgdaAny
v3
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4)
               ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                  (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                     ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v1)))
                  AgdaAny
v2)
               AgdaAny
v6))
         AgdaAny
v5)
-- Relation.Binary.Construct.NaturalOrder.Left.respʳ
d_resp'691'_3464 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp'691'_3464 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp'691'_3464 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_178
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'691'_3464 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_178
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_resp'691'_3464 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'691'_3464 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'691'_3464 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsMagma_178
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v9)
      AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
         AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4)
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4)
            (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
               (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                  ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                     ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4))
            ((T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188 T_IsMagma_178
v1 AgdaAny
v2 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
               ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                  (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> T_IsMagma_178
forall a b. a -> b
coe T_IsMagma_178
v1)) AgdaAny
v2)
               AgdaAny
v5))
         AgdaAny
v6)
-- Relation.Binary.Construct.NaturalOrder.Left.respˡ
d_resp'737'_3544 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp'737'_3544 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp'737'_3544 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_178
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'737'_3544 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_178
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_resp'737'_3544 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'737'_3544 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'737'_3544 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsMagma_178
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v9)
      AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
         AgdaAny
v4 AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2)
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
            AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2)
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                     ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2)
               (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                     ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                        ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))))
                  ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2))
               ((T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188 T_IsMagma_178
v1 AgdaAny
v3 AgdaAny
v4 AgdaAny
v2 AgdaAny
v2
                  AgdaAny
v5
                  ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                     (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> T_IsMagma_178
forall a b. a -> b
coe T_IsMagma_178
v1))
                     AgdaAny
v2)))
            AgdaAny
v6)
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> T_IsMagma_178
forall a b. a -> b
coe T_IsMagma_178
v1)) AgdaAny
v3
            AgdaAny
v4 AgdaAny
v5))
-- Relation.Binary.Construct.NaturalOrder.Left.resp₂
d_resp'8322'_3624 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_resp'8322'_3624 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> T_Σ_14
d_resp'8322'_3624 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_178
v5 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178 -> T_Σ_14
du_resp'8322'_3624 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_178
v5
du_resp'8322'_3624 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_resp'8322'_3624 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178 -> T_Σ_14
du_resp'8322'_3624 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsMagma_178
v1
  = (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 -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'691'_3464 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'737'_3544 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v1))
-- Relation.Binary.Construct.NaturalOrder.Left.dec
d_dec_3628 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_dec_3628 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
d_dec_3628 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7 = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_dec_3628 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
du_dec_3628 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dec_3628 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_dec_3628 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Construct.NaturalOrder.Left._.x∙y≤x
d_x'8729'y'8804'x_3720 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8729'y'8804'x_3720 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8729'y'8804'x_3720 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'x_3720 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny
v6 AgdaAny
v7
du_x'8729'y'8804'x_3720 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'x_3720 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'x_3720 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny
v2 AgdaAny
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v6)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v2)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                        ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v2) AgdaAny
v3)
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v2)
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                     ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                        ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                           ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v2) AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v2)
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                     ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                        ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                           ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                              ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v2)
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v2)
               (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                     ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                        ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                           ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                              ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                                 ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
                  ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v2))
               ((T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_622 T_IsCommutativeBand_612
v1 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)))
            ((T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_498
               (T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                  ((T_IsCommutativeBand_612 -> T_IsBand_526)
-> AgdaAny -> T_IsBand_526
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))
               AgdaAny
v2 AgdaAny
v2 AgdaAny
v3))
         ((T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188
            (T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
               ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe
                  T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                  ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1))))
            AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v2) AgdaAny
v3 AgdaAny
v3
            ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
               (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                        ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v2) AgdaAny
v2
               ((T_IsBand_526 -> AgdaAny -> AgdaAny)
-> T_IsBand_526 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsBand_526 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_536
                  (T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> T_IsCommutativeBand_612
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)) AgdaAny
v2))
            ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
               (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                        ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))
               AgdaAny
v3)))
-- Relation.Binary.Construct.NaturalOrder.Left._.x∙y≤y
d_x'8729'y'8804'y_3730 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8729'y'8804'y_3730 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8729'y'8804'y_3730 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'y_3730 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny
v6 AgdaAny
v7
du_x'8729'y'8804'y_3730 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'y_3730 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'y_3730 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny
v2 AgdaAny
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v6)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                        ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v3)
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                     ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                        ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                           ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v3)
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v3)
            (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
               (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                  ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                     ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                        ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                           ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                              ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v3))
            ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
               (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                        ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3))
               ((T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_498
                  (T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                     ((T_IsCommutativeBand_612 -> T_IsBand_526)
-> AgdaAny -> T_IsBand_526
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))
                  AgdaAny
v2 AgdaAny
v3 AgdaAny
v3)))
         ((T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188
            (T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
               ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe
                  T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                  ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1))))
            AgdaAny
v2 AgdaAny
v2 AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3)
            ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
               (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                        ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))
               AgdaAny
v2)
            ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
               (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                        ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v3) AgdaAny
v3
               ((T_IsBand_526 -> AgdaAny -> AgdaAny)
-> T_IsBand_526 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsBand_526 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_536
                  (T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> T_IsCommutativeBand_612
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)) AgdaAny
v3))))
-- Relation.Binary.Construct.NaturalOrder.Left._.∙-presʳ-≤
d_'8729''45'pres'691''45''8804'_3742 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'pres'691''45''8804'_3742 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8729''45'pres'691''45''8804'_3742 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
                                     AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8729''45'pres'691''45''8804'_3742 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_'8729''45'pres'691''45''8804'_3742 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8729''45'pres'691''45''8804'_3742 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8729''45'pres'691''45''8804'_3742 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v9)
      AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                  ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                     ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                        ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
         AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3))
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                     ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                        ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                           ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2) AgdaAny
v3)
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3))
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                     ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                        ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                           ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                              ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2) AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3))
               (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                     ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                        ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                           ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                              ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                                 ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))))
                  ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)))
               ((T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_498
                  (T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                     ((T_IsCommutativeBand_612 -> T_IsBand_526)
-> AgdaAny -> T_IsBand_526
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))
                  AgdaAny
v4 AgdaAny
v2 AgdaAny
v3))
            ((T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188
               (T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                  ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe
                     T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                     ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1))))
               AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2) AgdaAny
v3 AgdaAny
v3 AgdaAny
v5
               ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                  (T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
                     ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
                        T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                        ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                           ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))
                  AgdaAny
v3)))
         AgdaAny
v6)
-- Relation.Binary.Construct.NaturalOrder.Left._.infimum
d_infimum_3754 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_infimum_3754 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_infimum_3754 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> T_Σ_14
du_infimum_3754 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny
v6 AgdaAny
v7
du_infimum_3754 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_infimum_3754 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> T_Σ_14
du_infimum_3754 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny
v2 AgdaAny
v3
  = (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 -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'x_3720 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
         (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'y_3730 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
         (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8729''45'pres'691''45''8804'_3742 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)))
-- Relation.Binary.Construct.NaturalOrder.Left.isPreorder
d_isPreorder_3760 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_isPreorder_3760 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_526
-> T_IsPreorder_76
d_isPreorder_3760 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsBand_526
v5 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_526 -> T_IsPreorder_76
du_isPreorder_3760 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsBand_526
v5
du_isPreorder_3760 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_isPreorder_3760 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_526 -> T_IsPreorder_76
du_isPreorder_3760 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsBand_526
v1
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
         ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
            ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534 (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v1))))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_3208 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
            ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534 (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v1)))
         ((T_IsBand_526 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_526 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_536 (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_488
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_trans_3380 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534 (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v1)))
-- Relation.Binary.Construct.NaturalOrder.Left.isPartialOrder
d_isPartialOrder_3794 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
d_isPartialOrder_3794 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> T_IsPartialOrder_248
d_isPartialOrder_3794 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_IsPartialOrder_248
du_isPartialOrder_3794 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5
du_isPartialOrder_3794 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
du_isPartialOrder_3794 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_IsPartialOrder_248
du_isPartialOrder_3794 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1
  = (T_IsPreorder_76
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
      T_IsPreorder_76
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.C_constructor_294
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsBand_526 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_526 -> T_IsPreorder_76
du_isPreorder_3760 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antisym_3294 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
            ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
               ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                  ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))))
         ((T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_622 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))
-- Relation.Binary.Construct.NaturalOrder.Left.isDecPartialOrder
d_isDecPartialOrder_3836 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_300
d_isDecPartialOrder_3836 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_300
d_isDecPartialOrder_3836 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T_Dec_20
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_300
du_isDecPartialOrder_3836 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T_Dec_20
v6
du_isDecPartialOrder_3836 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_300
du_isDecPartialOrder_3836 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_300
du_isDecPartialOrder_3836 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny -> AgdaAny -> T_Dec_20
v2
  = (T_IsPartialOrder_248
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecPartialOrder_300)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_300
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_300
MAlonzo.Code.Relation.Binary.Structures.C_constructor_364
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_IsPartialOrder_248
du_isPartialOrder_3794 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v2)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_dec_3628 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v2))
-- Relation.Binary.Construct.NaturalOrder.Left.isTotalOrder
d_isTotalOrder_3842 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_488
d_isTotalOrder_3842 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_488
d_isTotalOrder_3842 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_488
du_isTotalOrder_3842 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6
du_isTotalOrder_3842 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_488
du_isTotalOrder_3842 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_488
du_isTotalOrder_3842 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2
  = (T_IsPartialOrder_248
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_488)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_488
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Structures.C_constructor_540
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_IsPartialOrder_248
du_isPartialOrder_3794 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
du_total_3364 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
               ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                  ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                     ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1))))))
         ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
            ((T_IsMagma_178 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186
               ((T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496
                  ((T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534
                     ((T_IsCommutativeBand_612 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.d_isBand_620 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1))))))
         ((AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2) ((T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_622 (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1)))
-- Relation.Binary.Construct.NaturalOrder.Left.isDecTotalOrder
d_isDecTotalOrder_3886 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_546
d_isDecTotalOrder_3886 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecTotalOrder_546
d_isDecTotalOrder_3886 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecTotalOrder_546
du_isDecTotalOrder_3886 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7
du_isDecTotalOrder_3886 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_546
du_isDecTotalOrder_3886 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecTotalOrder_546
du_isDecTotalOrder_3886 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny -> AgdaAny -> T_Dec_20
v3
  = (T_IsTotalOrder_488
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecTotalOrder_546)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_546
forall a b. a -> b
coe
      T_IsTotalOrder_488
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecTotalOrder_546
MAlonzo.Code.Relation.Binary.Structures.C_constructor_618
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> T_IsTotalOrder_488)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_488
du_isTotalOrder_3842 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1) ((AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2)) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_dec_3628 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v3))
-- Relation.Binary.Construct.NaturalOrder.Left.preorder
d_preorder_3894 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_preorder_3894 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_526
-> T_Preorder_142
d_preorder_3894 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsBand_526
v5 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_526 -> T_Preorder_142
du_preorder_3894 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsBand_526
v5
du_preorder_3894 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_preorder_3894 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_526 -> T_Preorder_142
du_preorder_3894 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsBand_526
v1
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsBand_526 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_526 -> T_IsPreorder_76
du_isPreorder_3760 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v1))
-- Relation.Binary.Construct.NaturalOrder.Left.poset
d_poset_3898 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_poset_3898 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> T_Poset_492
d_poset_3898 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_Poset_492
du_poset_3898 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5
du_poset_3898 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_poset_3898 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_Poset_492
du_poset_3898 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1
  = (T_IsPartialOrder_248 -> T_Poset_492) -> AgdaAny -> T_Poset_492
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_588
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_IsPartialOrder_248
du_isPartialOrder_3794 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1))
-- Relation.Binary.Construct.NaturalOrder.Left.decPoset
d_decPoset_3902 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_596
d_decPoset_3902 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecPoset_596
d_decPoset_3902 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T_Dec_20
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecPoset_596
du_decPoset_3902 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T_Dec_20
v6
du_decPoset_3902 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_596
du_decPoset_3902 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecPoset_596
du_decPoset_3902 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny -> AgdaAny -> T_Dec_20
v2
  = (T_IsDecPartialOrder_300 -> T_DecPoset_596)
-> AgdaAny -> T_DecPoset_596
forall a b. a -> b
coe
      T_IsDecPartialOrder_300 -> T_DecPoset_596
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_752
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecPartialOrder_300)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_300
du_isDecPartialOrder_3836 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v2))
-- Relation.Binary.Construct.NaturalOrder.Left.totalOrder
d_totalOrder_3908 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986
d_totalOrder_3908 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_TotalOrder_986
d_totalOrder_3908 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_TotalOrder_986
du_totalOrder_3908 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6
du_totalOrder_3908 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986
du_totalOrder_3908 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_TotalOrder_986
du_totalOrder_3908 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2
  = (T_IsTotalOrder_488 -> T_TotalOrder_986)
-> AgdaAny -> T_TotalOrder_986
forall a b. a -> b
coe
      T_IsTotalOrder_488 -> T_TotalOrder_986
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1090
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> T_IsTotalOrder_488)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_488
du_isTotalOrder_3842 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1) ((AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2))
-- Relation.Binary.Construct.NaturalOrder.Left.decTotalOrder
d_decTotalOrder_3914 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_1098
d_decTotalOrder_3914 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecTotalOrder_1098
d_decTotalOrder_3914 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecTotalOrder_1098
du_decTotalOrder_3914 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsCommutativeBand_612
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> T_Dec_20
v7
du_decTotalOrder_3914 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_1098
du_decTotalOrder_3914 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecTotalOrder_1098
du_decTotalOrder_3914 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsCommutativeBand_612
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny -> AgdaAny -> T_Dec_20
v3
  = (T_IsDecTotalOrder_546 -> T_DecTotalOrder_1098)
-> AgdaAny -> T_DecTotalOrder_1098
forall a b. a -> b
coe
      T_IsDecTotalOrder_546 -> T_DecTotalOrder_1098
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1272
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecTotalOrder_546)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecTotalOrder_546
du_isDecTotalOrder_3886 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsCommutativeBand_612 -> AgdaAny
forall a b. a -> b
coe T_IsCommutativeBand_612
v1) ((AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v3))