{-# 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.Setoid
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary

-- Relation.Binary.Construct.NaturalOrder.Left._.Commutative
d_Commutative_44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Commutative_44 :: 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_44 = 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_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Idempotent_52 :: 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_52 = 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_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Selective_88 :: 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_88 = 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_96 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsBand_96 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.NaturalOrder.Left._.IsMagma
d_IsMagma_124 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsMagma_124 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.NaturalOrder.Left._.IsSemigroup
d_IsSemigroup_134 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsSemigroup_134 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.NaturalOrder.Left._.IsSemilattice
d_IsSemilattice_136 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_IsSemilattice_136 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Construct.NaturalOrder.Left._≤_
d__'8804'__1516 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> ()
d__'8804'__1516 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8804'__1516 = 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_1522 ::
  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_86 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_1522 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_1522 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_86
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_1522 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_86
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_reflexive_1522 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_1522 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_1522 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsMagma_86
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
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)
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
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 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  ((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
v1)))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4))
            ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96 T_IsMagma_86
v1 AgdaAny
v3 AgdaAny
v3 AgdaAny
v3 AgdaAny
v4
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94 (T_IsMagma_86 -> T_IsMagma_86
forall a b. a -> b
coe T_IsMagma_86
v1)) AgdaAny
v3)
               AgdaAny
v5))
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
            (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94 (T_IsMagma_86 -> T_IsMagma_86
forall a b. a -> b
coe T_IsMagma_86
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_1584 ::
  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_1584 :: 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_1584 ~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_1584 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_refl_1584 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_refl_1584 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_refl_1584 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_1592 ::
  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_26 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_1592 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antisym_1592 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_26
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antisym_1592 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsEquivalence_26
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_antisym_1592 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_1592 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antisym_1592 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 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.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         ((T_IsEquivalence_26 -> T_Setoid_44)
-> T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
            T_IsEquivalence_26
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
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            ((T_IsEquivalence_26 -> T_Setoid_44)
-> T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
               T_IsEquivalence_26
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
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               ((T_IsEquivalence_26 -> T_Setoid_44)
-> T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
                  T_IsEquivalence_26
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 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v1))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 T_IsEquivalence_26
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_1646 ::
  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_1646 :: 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_1646 ~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_1646 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_1646 ::
  (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_1646 :: (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_1646 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
  = let v7 :: t
v7 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v3 AgdaAny
v5 AgdaAny
v6 in
    AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v8
           -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                ((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
v5 AgdaAny
v8)
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v8
           -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                ((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
v6 AgdaAny
v5) AgdaAny
v6
                   ((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 -> 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
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v6) AgdaAny
v6 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v6 AgdaAny
v5) AgdaAny
v8))
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Construct.NaturalOrder.Left.trans
d_trans_1692 ::
  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_194 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_1692 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_1692 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemigroup_194
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_trans_1692 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemigroup_194
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_trans_1692 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_1692 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_trans_1692 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemigroup_194
v1 AgdaAny
v2 AgdaAny
v3 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.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
            ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
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)
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
               ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
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)
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
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)
               ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
                  ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
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 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                     ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                        ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                           ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                              ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v1)))))
                     ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4))
                  ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
                     (T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> T_IsSemigroup_194
forall a b. a -> b
coe T_IsSemigroup_194
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_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                        (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                           ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
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_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                        (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                           ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v1)))
                        AgdaAny
v4)))
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                  (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
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_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_204 T_IsSemigroup_194
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4)))
            ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
               (T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> T_IsSemigroup_194
forall a b. a -> b
coe T_IsSemigroup_194
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_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v1)))
                  AgdaAny
v2)
               AgdaAny
v6))
         AgdaAny
v5)
-- Relation.Binary.Construct.NaturalOrder.Left.respʳ
d_resp'691'_1760 ::
  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_86 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp'691'_1760 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp'691'_1760 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_86
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'691'_1760 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_86
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_resp'691'_1760 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'691'_1760 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'691'_1760 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsMagma_86
v1 AgdaAny
v2 AgdaAny
v3 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.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
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)
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
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 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  ((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
v1)))
               ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v4))
            ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96 T_IsMagma_86
v1 AgdaAny
v2 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94 (T_IsMagma_86 -> T_IsMagma_86
forall a b. a -> b
coe T_IsMagma_86
v1)) AgdaAny
v2)
               AgdaAny
v5))
         AgdaAny
v6)
-- Relation.Binary.Construct.NaturalOrder.Left.respˡ
d_resp'737'_1824 ::
  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_86 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp'737'_1824 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp'737'_1824 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_86
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'737'_1824 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_86
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_resp'737'_1824 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'737'_1824 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'737'_1824 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsMagma_86
v1 AgdaAny
v2 AgdaAny
v3 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.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
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)
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
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)
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
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 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     ((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94 (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
v1)))
                  ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v2))
               ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96 T_IsMagma_86
v1 AgdaAny
v3 AgdaAny
v4 AgdaAny
v2 AgdaAny
v2
                  AgdaAny
v5
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94 (T_IsMagma_86 -> T_IsMagma_86
forall a b. a -> b
coe T_IsMagma_86
v1)) AgdaAny
v2)))
            AgdaAny
v6)
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
            (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94 (T_IsMagma_86 -> T_IsMagma_86
forall a b. a -> b
coe T_IsMagma_86
v1)) AgdaAny
v3 AgdaAny
v4
            AgdaAny
v5))
-- Relation.Binary.Construct.NaturalOrder.Left.resp₂
d_resp'8322'_1888 ::
  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_86 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_resp'8322'_1888 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> T_Σ_14
d_resp'8322'_1888 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_86
v5 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86 -> T_Σ_14
du_resp'8322'_1888 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsMagma_86
v5
du_resp'8322'_1888 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_resp'8322'_1888 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86 -> T_Σ_14
du_resp'8322'_1888 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsMagma_86
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_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'691'_1760 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
v1))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_resp'737'_1824 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
v1))
-- Relation.Binary.Construct.NaturalOrder.Left.dec
d_dec_1892 ::
  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.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dec_1892 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_dec_1892 ~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_32
v5 AgdaAny
v6 AgdaAny
v7 = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_dec_1892 AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> T_Dec_32
v5 AgdaAny
v6 AgdaAny
v7
du_dec_1892 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dec_1892 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_dec_1892 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Dec_32
v1 AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
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_1968 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8729'y'8804'x_1968 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8729'y'8804'x_1968 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'x_1968 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny
v6 AgdaAny
v7
du_x'8729'y'8804'x_1968 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'x_1968 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'x_1968 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny
v2 AgdaAny
v3
  = (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         (let v4 :: T_IsBand_230
v4 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsSemigroup_194
v5
                   = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5)))))
         ((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)
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            (let v4 :: T_IsBand_230
v4 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v5 :: T_IsSemigroup_194
v5
                      = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v4) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5)))))
            ((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)
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               (let v4 :: T_IsBand_230
v4 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v5 :: T_IsSemigroup_194
v5
                         = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v4) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                        ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5)))))
               ((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 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                        (let v4 :: T_IsBand_230
v4 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
                         AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           (let v5 :: T_IsSemigroup_194
v5
                                  = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v4) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                                 ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5)))))))
                  ((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_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_322 T_IsSemilattice_312
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_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_204
               (T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                  ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))
               AgdaAny
v2 AgdaAny
v2 AgdaAny
v3))
         ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
            (T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
               ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
                  T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                  ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
                     T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                     ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                        ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_230 -> AgdaAny -> AgdaAny)
-> T_IsBand_230 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsBand_230 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_240
                  (T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1)) AgdaAny
v2))
            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
               (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
                     T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                     ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                        ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))))
               AgdaAny
v3)))
-- Relation.Binary.Construct.NaturalOrder.Left._.x∙y≤y
d_x'8729'y'8804'y_1978 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_x'8729'y'8804'y_1978 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_x'8729'y'8804'y_1978 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'y_1978 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny
v6 AgdaAny
v7
du_x'8729'y'8804'y_1978 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'y_1978 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'y_1978 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny
v2 AgdaAny
v3
  = (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         (let v4 :: T_IsBand_230
v4 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsSemigroup_194
v5
                   = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5)))))
         ((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)
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            (let v4 :: T_IsBand_230
v4 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v5 :: T_IsSemigroup_194
v5
                      = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v4) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5)))))
            ((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 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                     (let v4 :: T_IsBand_230
v4 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (let v5 :: T_IsSemigroup_194
v5
                               = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v4) in
                         AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                              ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v5)))))))
               ((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_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
                     T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                     ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                        ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_204
                  (T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                     ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))
                  AgdaAny
v2 AgdaAny
v3 AgdaAny
v3)))
         ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
            (T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
               ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
                  T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                  ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
               (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
                     T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                     ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                        ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))))
               AgdaAny
v2)
            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
                     T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                     ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                        ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_230 -> AgdaAny -> AgdaAny)
-> T_IsBand_230 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsBand_230 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_240
                  (T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1)) AgdaAny
v3))))
-- Relation.Binary.Construct.NaturalOrder.Left._.∙-presʳ-≤
d_'8729''45'pres'691''45''8804'_1990 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'pres'691''45''8804'_1990 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8729''45'pres'691''45''8804'_1990 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
                                     AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8729''45'pres'691''45''8804'_1990 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_'8729''45'pres'691''45''8804'_1990 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8729''45'pres'691''45''8804'_1990 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8729''45'pres'691''45''8804'_1990 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny
v2 AgdaAny
v3 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.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         (let v7 :: T_IsBand_230
v7 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v8 :: T_IsSemigroup_194
v8
                   = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v7) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                  ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v8)))))
         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))
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            (let v7 :: T_IsBand_230
v7 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v8 :: T_IsSemigroup_194
v8
                      = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v7) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v8)))))
            ((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))
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               (let v7 :: T_IsBand_230
v7 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v8 :: T_IsSemigroup_194
v8
                         = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v7) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                        ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v8)))))
               ((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 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                        (let v7 :: T_IsBand_230
v7 = T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> T_IsSemilattice_312
forall a b. a -> b
coe T_IsSemilattice_312
v1) in
                         AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           (let v8 :: T_IsSemigroup_194
v8
                                  = T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> T_IsBand_230
forall a b. a -> b
coe T_IsBand_230
v7) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              ((T_IsMagma_86 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsMagma_86 -> T_Setoid_44
MAlonzo.Code.Algebra.Structures.du_setoid_110
                                 ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202 (T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
v8)))))))
                  ((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_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroup_194 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_204
                  (T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                     ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))
                  AgdaAny
v4 AgdaAny
v2 AgdaAny
v3))
            ((T_IsMagma_86
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_86
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_96
               (T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                  ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
                     T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                     ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  (T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
                     ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
                        T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                        ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                           ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))))
                  AgdaAny
v3)))
         AgdaAny
v6)
-- Relation.Binary.Construct.NaturalOrder.Left._.infimum
d_infimum_2002 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_infimum_2002 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_infimum_2002 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> T_Σ_14
du_infimum_2002 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny
v6 AgdaAny
v7
du_infimum_2002 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_infimum_2002 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> T_Σ_14
du_infimum_2002 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
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_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'x_1968 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
du_x'8729'y'8804'y_1978 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_IsSemilattice_312
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8729''45'pres'691''45''8804'_1990 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_2008 ::
  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_230 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_2008 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_230
-> T_IsPreorder_70
d_isPreorder_2008 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsBand_230
v5 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_230 -> T_IsPreorder_70
du_isPreorder_2008 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsBand_230
v5
du_isPreorder_2008 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_2008 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_230 -> T_IsPreorder_70
du_isPreorder_2008 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsBand_230
v1
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
      ((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
         ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
            ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> AgdaAny
forall a b. a -> b
coe T_IsBand_230
v1))))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_reflexive_1522 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
            ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> AgdaAny
forall a b. a -> b
coe T_IsBand_230
v1)))
         ((T_IsBand_230 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_230 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_240 (T_IsBand_230 -> AgdaAny
forall a b. a -> b
coe T_IsBand_230
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_194
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_trans_1692 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238 (T_IsBand_230 -> AgdaAny
forall a b. a -> b
coe T_IsBand_230
v1)))
-- Relation.Binary.Construct.NaturalOrder.Left.isPartialOrder
d_isPartialOrder_2042 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_isPartialOrder_2042 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> T_IsPartialOrder_162
d_isPartialOrder_2042 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_IsPartialOrder_162
du_isPartialOrder_2042 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5
du_isPartialOrder_2042 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_isPartialOrder_2042 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_IsPartialOrder_162
du_isPartialOrder_2042 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsBand_230 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_230 -> T_IsPreorder_70
du_isPreorder_2008 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antisym_1592 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
            ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
               ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                  ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))))
         ((T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_322 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))
-- Relation.Binary.Construct.NaturalOrder.Left.isDecPartialOrder
d_isDecPartialOrder_2084 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
d_isDecPartialOrder_2084 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
d_isDecPartialOrder_2084 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T_Dec_32
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
du_isDecPartialOrder_2084 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T_Dec_32
v6
du_isDecPartialOrder_2084 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
du_isDecPartialOrder_2084 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
du_isDecPartialOrder_2084 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_206
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_10957
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_IsPartialOrder_162
du_isPartialOrder_2042 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v2)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_dec_1892 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v2))
-- Relation.Binary.Construct.NaturalOrder.Left.isTotalOrder
d_isTotalOrder_2090 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
d_isTotalOrder_2090 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_384
d_isTotalOrder_2090 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_384
du_isTotalOrder_2090 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6
du_isTotalOrder_2090 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
du_isTotalOrder_2090 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_384
du_isTotalOrder_2090 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_384
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_19815
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_IsPartialOrder_162
du_isPartialOrder_2042 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_1646 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0)
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
            ((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
               ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                  ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                     ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1))))))
         ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
            ((T_IsMagma_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsMagma_86 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_94
               ((T_IsSemigroup_194 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsSemigroup_194 -> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.d_isMagma_202
                  ((T_IsBand_230 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBand_230 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.d_isSemigroup_238
                     ((T_IsSemilattice_312 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.d_isBand_320 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1))))))
         ((AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2) ((T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_comm_322 (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1)))
-- Relation.Binary.Construct.NaturalOrder.Left.isDecTotalOrder
d_isDecTotalOrder_2134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
d_isDecTotalOrder_2134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
d_isDecTotalOrder_2134 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> T_Dec_32
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
du_isDecTotalOrder_2134 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> T_Dec_32
v7
du_isDecTotalOrder_2134 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
du_isDecTotalOrder_2134 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
du_isDecTotalOrder_2134 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny -> AgdaAny -> T_Dec_32
v3
  = (T_IsTotalOrder_384
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_434
forall a b. a -> b
coe
      T_IsTotalOrder_384
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_21785
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_384
du_isTotalOrder_2090 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1) ((AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2)) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v3)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_dec_1892 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v3))
-- Relation.Binary.Construct.NaturalOrder.Left.preorder
d_preorder_2142 ::
  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_230 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_preorder_2142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBand_230
-> T_Preorder_132
d_preorder_2142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsBand_230
v5 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_230 -> T_Preorder_132
du_preorder_2142 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsBand_230
v5
du_preorder_2142 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_preorder_2142 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_230 -> T_Preorder_132
du_preorder_2142 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsBand_230
v1
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsBand_230 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_230 -> T_IsPreorder_70
du_isPreorder_2008 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsBand_230 -> AgdaAny
forall a b. a -> b
coe T_IsBand_230
v1))
-- Relation.Binary.Construct.NaturalOrder.Left.poset
d_poset_2146 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_poset_2146 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> T_Poset_282
d_poset_2146 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_Poset_282
du_poset_2146 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5
du_poset_2146 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_poset_2146 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_Poset_282
du_poset_2146 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1
  = (T_IsPartialOrder_162 -> T_Poset_282) -> AgdaAny -> T_Poset_282
forall a b. a -> b
coe
      T_IsPartialOrder_162 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_5219
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_IsPartialOrder_162
du_isPartialOrder_2042 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1))
-- Relation.Binary.Construct.NaturalOrder.Left.decPoset
d_decPoset_2150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
d_decPoset_2150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecPoset_360
d_decPoset_2150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T_Dec_32
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecPoset_360
du_decPoset_2150 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T_Dec_32
v6
du_decPoset_2150 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
du_decPoset_2150 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecPoset_360
du_decPoset_2150 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2
  = (T_IsDecPartialOrder_206 -> T_DecPoset_360)
-> AgdaAny -> T_DecPoset_360
forall a b. a -> b
coe
      T_IsDecPartialOrder_206 -> T_DecPoset_360
MAlonzo.Code.Relation.Binary.Bundles.C_DecPoset'46'constructor_6777
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
du_isDecPartialOrder_2084 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v2))
-- Relation.Binary.Construct.NaturalOrder.Left.totalOrder
d_totalOrder_2156 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652
d_totalOrder_2156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_TotalOrder_652
d_totalOrder_2156 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_TotalOrder_652
du_totalOrder_2156 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6
du_totalOrder_2156 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652
du_totalOrder_2156 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_TotalOrder_652
du_totalOrder_2156 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2
  = (T_IsTotalOrder_384 -> T_TotalOrder_652)
-> AgdaAny -> T_TotalOrder_652
forall a b. a -> b
coe
      T_IsTotalOrder_384 -> T_TotalOrder_652
MAlonzo.Code.Relation.Binary.Bundles.C_TotalOrder'46'constructor_12489
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_IsTotalOrder_384
du_isTotalOrder_2090 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
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_2162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740
d_decTotalOrder_2162 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecTotalOrder_740
d_decTotalOrder_2162 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> T_Dec_32
v7
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecTotalOrder_740
du_decTotalOrder_2162 AgdaAny -> AgdaAny -> AgdaAny
v4 T_IsSemilattice_312
v5 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> T_Dec_32
v7
du_decTotalOrder_2162 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312 ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740
du_decTotalOrder_2162 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecTotalOrder_740
du_decTotalOrder_2162 AgdaAny -> AgdaAny -> AgdaAny
v0 T_IsSemilattice_312
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny -> AgdaAny -> T_Dec_32
v3
  = (T_IsDecTotalOrder_434 -> T_DecTotalOrder_740)
-> AgdaAny -> T_DecTotalOrder_740
forall a b. a -> b
coe
      T_IsDecTotalOrder_434 -> T_DecTotalOrder_740
MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_14337
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
du_isDecTotalOrder_2134 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_IsSemilattice_312 -> AgdaAny
forall a b. a -> b
coe T_IsSemilattice_312
v1) ((AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v3))