{-# 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.Algebra.Lattice.Properties.Lattice 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.Lattice.Bundles
import qualified MAlonzo.Code.Algebra.Lattice.Properties.Semilattice
import qualified MAlonzo.Code.Algebra.Lattice.Structures
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left
import qualified MAlonzo.Code.Relation.Binary.Lattice.Bundles
import qualified MAlonzo.Code.Relation.Binary.Lattice.Structures
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Algebra.Lattice.Properties.Lattice._.Idempotent
d_Idempotent_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Idempotent_78 :: T_Level_18
-> T_Level_18
-> T_Lattice_512
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Idempotent_78 = T_Level_18
-> T_Level_18
-> T_Lattice_512
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Lattice._.IsBand
d_IsBand_82 :: p -> p -> p -> p -> T_Level_18
d_IsBand_82 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Lattice.Properties.Lattice._.IsMagma
d_IsMagma_86 :: p -> p -> p -> p -> T_Level_18
d_IsMagma_86 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Lattice.Properties.Lattice._.IsSemigroup
d_IsSemigroup_90 :: p -> p -> p -> p -> T_Level_18
d_IsSemigroup_90 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Lattice.Properties.Lattice._.IsBand.idem
d_idem_98 ::
  MAlonzo.Code.Algebra.Structures.T_IsBand_526 -> AgdaAny -> AgdaAny
d_idem_98 :: T_IsBand_526 -> AgdaAny -> AgdaAny
d_idem_98 T_IsBand_526
v0
  = (T_IsBand_526 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_526 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_536 (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v0)
-- Algebra.Lattice.Properties.Lattice._.IsBand.isSemigroup
d_isSemigroup_106 ::
  MAlonzo.Code.Algebra.Structures.T_IsBand_526 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_isSemigroup_106 :: T_IsBand_526 -> T_IsSemigroup_488
d_isSemigroup_106 T_IsBand_526
v0
  = (T_IsBand_526 -> T_IsSemigroup_488) -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe T_IsBand_526 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.d_isSemigroup_534 (T_IsBand_526 -> AgdaAny
forall a b. a -> b
coe T_IsBand_526
v0)
-- Algebra.Lattice.Properties.Lattice._.IsMagma.isEquivalence
d_isEquivalence_126 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence_126 :: T_IsMagma_178 -> T_IsEquivalence_28
d_isEquivalence_126 T_IsMagma_178
v0
  = (T_IsMagma_178 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe T_IsMagma_178 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Structures.d_isEquivalence_186 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v0)
-- Algebra.Lattice.Properties.Lattice._.IsMagma.∙-cong
d_'8729''45'cong_140 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'cong_140 :: T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8729''45'cong_140 T_IsMagma_178
v0
  = (T_IsMagma_178
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_188 (T_IsMagma_178 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_178
v0)
-- Algebra.Lattice.Properties.Lattice._.IsSemigroup.assoc
d_assoc_148 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_assoc_148 :: T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_assoc_148 T_IsSemigroup_488
v0
  = (T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_498 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v0)
-- Algebra.Lattice.Properties.Lattice._.IsSemigroup.isMagma
d_isMagma_152 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_isMagma_152 :: T_IsSemigroup_488 -> T_IsMagma_178
d_isMagma_152 T_IsSemigroup_488
v0
  = (T_IsSemigroup_488 -> T_IsMagma_178) -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe T_IsSemigroup_488 -> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.d_isMagma_496 (T_IsSemigroup_488 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_488
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice
d_IsLattice_174 :: p -> p -> p -> p -> p -> T_Level_18
d_IsLattice_174 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Algebra.Lattice.Properties.Lattice._.IsSemilattice
d_IsSemilattice_178 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_IsSemilattice_178 :: T_Level_18
-> T_Level_18
-> T_Lattice_512
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_IsSemilattice_178 = T_Level_18
-> T_Level_18
-> T_Lattice_512
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Lattice._.IsLattice.absorptive
d_absorptive_182 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_absorptive_182 :: T_IsLattice_3070 -> T_Σ_14
d_absorptive_182 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsLattice_3070 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_3106 (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.isEquivalence
d_isEquivalence_184 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence_184 :: T_IsLattice_3070 -> T_IsEquivalence_28
d_isEquivalence_184 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
      T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∧-assoc
d_'8743''45'assoc_198 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'assoc_198 :: T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'assoc_198 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_3102
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∧-comm
d_'8743''45'comm_200 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'comm_200 :: T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'comm_200 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_3100
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∧-cong
d_'8743''45'cong_202 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'cong_202 :: T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8743''45'cong_202 T_IsLattice_3070
v0
  = (T_IsLattice_3070
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_3104
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∨-assoc
d_'8744''45'assoc_210 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'assoc_210 :: T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'assoc_210 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_3096
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∨-comm
d_'8744''45'comm_212 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'comm_212 :: T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'comm_212 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_3094
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∨-cong
d_'8744''45'cong_214 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'cong_214 :: T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8744''45'cong_214 T_IsLattice_3070
v0
  = (T_IsLattice_3070
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_3098
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Properties.Lattice.∧-idem
d_'8743''45'idem_294 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny
d_'8743''45'idem_294 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> AgdaAny -> AgdaAny
d_'8743''45'idem_294 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 AgdaAny
v3 = T_Lattice_512 -> AgdaAny -> AgdaAny
du_'8743''45'idem_294 T_Lattice_512
v2 AgdaAny
v3
du_'8743''45'idem_294 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny
du_'8743''45'idem_294 :: T_Lattice_512 -> AgdaAny -> AgdaAny
du_'8743''45'idem_294 T_Lattice_512
v0 AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v4)
      ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1)
      AgdaAny
v1
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10216'_372
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                  ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
         (T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            ((T_IsLattice_3070 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
               T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
               ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))))
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1)
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1)))
         AgdaAny
v1
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                     ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1)))
            AgdaAny
v1 AgdaAny
v1
            (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
               (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                  ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                     ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                        ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
            ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'absorbs'45''8744'_3122
               (T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0)) AgdaAny
v1
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1)))
         ((T_IsLattice_3070
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_3070
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'cong'737'_3124
            ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'absorbs'45''8743'_3120
               (T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0)) AgdaAny
v1
               AgdaAny
v1)))
-- Algebra.Lattice.Properties.Lattice.∧-isMagma
d_'8743''45'isMagma_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'8743''45'isMagma_298 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsMagma_178
d_'8743''45'isMagma_298 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 = T_Lattice_512 -> T_IsMagma_178
du_'8743''45'isMagma_298 T_Lattice_512
v2
du_'8743''45'isMagma_298 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'8743''45'isMagma_298 :: T_Lattice_512 -> T_IsMagma_178
du_'8743''45'isMagma_298 T_Lattice_512
v0
  = (T_IsEquivalence_28
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178)
-> AgdaAny -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.C_constructor_210
      ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_IsLattice_3070
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_3104
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
-- Algebra.Lattice.Properties.Lattice.∧-isSemigroup
d_'8743''45'isSemigroup_300 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'8743''45'isSemigroup_300 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsSemigroup_488
d_'8743''45'isSemigroup_300 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsSemigroup_488
du_'8743''45'isSemigroup_300 T_Lattice_512
v2
du_'8743''45'isSemigroup_300 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'8743''45'isSemigroup_300 :: T_Lattice_512 -> T_IsSemigroup_488
du_'8743''45'isSemigroup_300 T_Lattice_512
v0
  = (T_IsMagma_178
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe
      T_IsMagma_178
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.C_constructor_522
      ((T_Lattice_512 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsMagma_178
du_'8743''45'isMagma_298 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_3102
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
-- Algebra.Lattice.Properties.Lattice.∧-isBand
d_'8743''45'isBand_302 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
d_'8743''45'isBand_302 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsBand_526
d_'8743''45'isBand_302 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 = T_Lattice_512 -> T_IsBand_526
du_'8743''45'isBand_302 T_Lattice_512
v2
du_'8743''45'isBand_302 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
du_'8743''45'isBand_302 :: T_Lattice_512 -> T_IsBand_526
du_'8743''45'isBand_302 T_Lattice_512
v0
  = (T_IsSemigroup_488 -> (AgdaAny -> AgdaAny) -> T_IsBand_526)
-> AgdaAny -> AgdaAny -> T_IsBand_526
forall a b. a -> b
coe
      T_IsSemigroup_488 -> (AgdaAny -> AgdaAny) -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.C_constructor_564
      ((T_Lattice_512 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsSemigroup_488
du_'8743''45'isSemigroup_300 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_Lattice_512 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny
du_'8743''45'idem_294 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice.∧-isSemilattice
d_'8743''45'isSemilattice_304 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
d_'8743''45'isSemilattice_304 :: T_Level_18
-> T_Level_18 -> T_Lattice_512 -> T_IsCommutativeBand_612
d_'8743''45'isSemilattice_304 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsCommutativeBand_612
du_'8743''45'isSemilattice_304 T_Lattice_512
v2
du_'8743''45'isSemilattice_304 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
du_'8743''45'isSemilattice_304 :: T_Lattice_512 -> T_IsCommutativeBand_612
du_'8743''45'isSemilattice_304 T_Lattice_512
v0
  = (T_IsBand_526
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_612)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_612
forall a b. a -> b
coe
      T_IsBand_526
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Structures.C_constructor_660
      ((T_Lattice_512 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsBand_526
du_'8743''45'isBand_302 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_3100
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
-- Algebra.Lattice.Properties.Lattice.∧-semilattice
d_'8743''45'semilattice_306 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8743''45'semilattice_306 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_Semilattice_10
d_'8743''45'semilattice_306 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_Semilattice_10
du_'8743''45'semilattice_306 T_Lattice_512
v2
du_'8743''45'semilattice_306 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8743''45'semilattice_306 :: T_Lattice_512 -> T_Semilattice_10
du_'8743''45'semilattice_306 T_Lattice_512
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> T_Semilattice_10)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_84
      (T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_Lattice_512 -> T_IsCommutativeBand_612) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsCommutativeBand_612
du_'8743''45'isSemilattice_304 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_310 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_310 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_310 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_310 T_Lattice_512
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_310 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_310 :: T_Lattice_512 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_310 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_IsJoinSemilattice_22)
-> AgdaAny -> T_IsJoinSemilattice_22
forall a b. a -> b
coe
      T_Semilattice_10 -> T_IsJoinSemilattice_22
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8743''45'semilattice_306 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_312 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_312 :: T_Level_18
-> T_Level_18 -> T_Lattice_512 -> T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_312 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_312 T_Lattice_512
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_312 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_312 :: T_Lattice_512 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_312 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_IsMeetSemilattice_184)
-> AgdaAny -> T_IsMeetSemilattice_184
forall a b. a -> b
coe
      T_Semilattice_10 -> T_IsMeetSemilattice_184
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticMeetSemilattice_176
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8743''45'semilattice_306 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_314 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_314 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_314 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_314 T_Lattice_512
v2
du_'8743''45'orderTheoreticJoinSemilattice_314 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_314 :: T_Lattice_512 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_314 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_JoinSemilattice_14)
-> AgdaAny -> T_JoinSemilattice_14
forall a b. a -> b
coe
      T_Semilattice_10 -> T_JoinSemilattice_14
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticJoinSemilattice_182
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8743''45'semilattice_306 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_316 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_316 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_316 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_316 T_Lattice_512
v2
du_'8743''45'orderTheoreticMeetSemilattice_316 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_316 :: T_Lattice_512 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_316 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_MeetSemilattice_204)
-> AgdaAny -> T_MeetSemilattice_204
forall a b. a -> b
coe
      T_Semilattice_10 -> T_MeetSemilattice_204
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticMeetSemilattice_180
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8743''45'semilattice_306 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice.∨-idem
d_'8744''45'idem_318 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny
d_'8744''45'idem_318 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> AgdaAny -> AgdaAny
d_'8744''45'idem_318 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 AgdaAny
v3 = T_Lattice_512 -> AgdaAny -> AgdaAny
du_'8744''45'idem_318 T_Lattice_512
v2 AgdaAny
v3
du_'8744''45'idem_318 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny
du_'8744''45'idem_318 :: T_Lattice_512 -> AgdaAny -> AgdaAny
du_'8744''45'idem_318 T_Lattice_512
v0 AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v4)
      ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1)
      AgdaAny
v1
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10216'_372
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                  ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
         (T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            ((T_IsLattice_3070 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
               T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
               ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))))
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1)
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1))
         AgdaAny
v1
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                     ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1))
            AgdaAny
v1 AgdaAny
v1
            (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
               (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                  ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                     ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                        ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
            ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'absorbs'45''8743'_3120
               (T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0)) AgdaAny
v1
               AgdaAny
v1))
         ((T_IsLattice_3070
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_3070
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'cong'737'_3132
            ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v1)
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ((T_Lattice_512 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny
du_'8743''45'idem_294 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
-- Algebra.Lattice.Properties.Lattice.∨-isMagma
d_'8744''45'isMagma_322 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'8744''45'isMagma_322 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsMagma_178
d_'8744''45'isMagma_322 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 = T_Lattice_512 -> T_IsMagma_178
du_'8744''45'isMagma_322 T_Lattice_512
v2
du_'8744''45'isMagma_322 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'8744''45'isMagma_322 :: T_Lattice_512 -> T_IsMagma_178
du_'8744''45'isMagma_322 T_Lattice_512
v0
  = (T_IsEquivalence_28
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178)
-> AgdaAny -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.C_constructor_210
      ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_IsLattice_3070
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_3098
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
-- Algebra.Lattice.Properties.Lattice.∨-isSemigroup
d_'8744''45'isSemigroup_324 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'8744''45'isSemigroup_324 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsSemigroup_488
d_'8744''45'isSemigroup_324 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsSemigroup_488
du_'8744''45'isSemigroup_324 T_Lattice_512
v2
du_'8744''45'isSemigroup_324 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'8744''45'isSemigroup_324 :: T_Lattice_512 -> T_IsSemigroup_488
du_'8744''45'isSemigroup_324 T_Lattice_512
v0
  = (T_IsMagma_178
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe
      T_IsMagma_178
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.C_constructor_522
      ((T_Lattice_512 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsMagma_178
du_'8744''45'isMagma_322 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_3096
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
-- Algebra.Lattice.Properties.Lattice.∨-isBand
d_'8744''45'isBand_326 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
d_'8744''45'isBand_326 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsBand_526
d_'8744''45'isBand_326 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 = T_Lattice_512 -> T_IsBand_526
du_'8744''45'isBand_326 T_Lattice_512
v2
du_'8744''45'isBand_326 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
du_'8744''45'isBand_326 :: T_Lattice_512 -> T_IsBand_526
du_'8744''45'isBand_326 T_Lattice_512
v0
  = (T_IsSemigroup_488 -> (AgdaAny -> AgdaAny) -> T_IsBand_526)
-> AgdaAny -> AgdaAny -> T_IsBand_526
forall a b. a -> b
coe
      T_IsSemigroup_488 -> (AgdaAny -> AgdaAny) -> T_IsBand_526
MAlonzo.Code.Algebra.Structures.C_constructor_564
      ((T_Lattice_512 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsSemigroup_488
du_'8744''45'isSemigroup_324 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_Lattice_512 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny
du_'8744''45'idem_318 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice.∨-isSemilattice
d_'8744''45'isSemilattice_328 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
d_'8744''45'isSemilattice_328 :: T_Level_18
-> T_Level_18 -> T_Lattice_512 -> T_IsCommutativeBand_612
d_'8744''45'isSemilattice_328 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsCommutativeBand_612
du_'8744''45'isSemilattice_328 T_Lattice_512
v2
du_'8744''45'isSemilattice_328 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
du_'8744''45'isSemilattice_328 :: T_Lattice_512 -> T_IsCommutativeBand_612
du_'8744''45'isSemilattice_328 T_Lattice_512
v0
  = (T_IsBand_526
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_612)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_612
forall a b. a -> b
coe
      T_IsBand_526
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Structures.C_constructor_660
      ((T_Lattice_512 -> T_IsBand_526) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsBand_526
du_'8744''45'isBand_326 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_3094
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
-- Algebra.Lattice.Properties.Lattice.∨-semilattice
d_'8744''45'semilattice_330 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8744''45'semilattice_330 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_Semilattice_10
d_'8744''45'semilattice_330 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 T_Lattice_512
v2
du_'8744''45'semilattice_330 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8744''45'semilattice_330 :: T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 T_Lattice_512
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> T_Semilattice_10)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_84
      (T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_Lattice_512 -> T_IsCommutativeBand_612) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsCommutativeBand_612
du_'8744''45'isSemilattice_328 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_334 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_334 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_334 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_334 T_Lattice_512
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_334 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_334 :: T_Lattice_512 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_334 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_IsJoinSemilattice_22)
-> AgdaAny -> T_IsJoinSemilattice_22
forall a b. a -> b
coe
      T_Semilattice_10 -> T_IsJoinSemilattice_22
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_336 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_336 :: T_Level_18
-> T_Level_18 -> T_Lattice_512 -> T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_336 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_336 T_Lattice_512
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_336 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_336 :: T_Lattice_512 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_336 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_IsMeetSemilattice_184)
-> AgdaAny -> T_IsMeetSemilattice_184
forall a b. a -> b
coe
      T_Semilattice_10 -> T_IsMeetSemilattice_184
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticMeetSemilattice_176
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_338 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_338 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_338 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_338 T_Lattice_512
v2
du_'8743''45'orderTheoreticJoinSemilattice_338 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_338 :: T_Lattice_512 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_338 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_JoinSemilattice_14)
-> AgdaAny -> T_JoinSemilattice_14
forall a b. a -> b
coe
      T_Semilattice_10 -> T_JoinSemilattice_14
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticJoinSemilattice_182
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_340 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_340 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_340 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_340 T_Lattice_512
v2
du_'8743''45'orderTheoreticMeetSemilattice_340 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_340 :: T_Lattice_512 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_340 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_MeetSemilattice_204)
-> AgdaAny -> T_MeetSemilattice_204
forall a b. a -> b
coe
      T_Semilattice_10 -> T_MeetSemilattice_204
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticMeetSemilattice_180
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice.∧-∨-isLattice
d_'8743''45''8744''45'isLattice_342 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
d_'8743''45''8744''45'isLattice_342 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsLattice_3070
d_'8743''45''8744''45'isLattice_342 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsLattice_3070
du_'8743''45''8744''45'isLattice_342 T_Lattice_512
v2
du_'8743''45''8744''45'isLattice_342 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
du_'8743''45''8744''45'isLattice_342 :: T_Lattice_512 -> T_IsLattice_3070
du_'8743''45''8744''45'isLattice_342 T_Lattice_512
v0
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsLattice_3070)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsLattice_3070
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Structures.C_constructor_3140
      ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_3100
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_3102
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_IsLattice_3070
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_3104
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_3094
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_3096
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_IsLattice_3070
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_3098
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370
         ((T_IsLattice_3070 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_3070 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_3106
            ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))))
-- Algebra.Lattice.Properties.Lattice.∧-∨-lattice
d_'8743''45''8744''45'lattice_344 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512
d_'8743''45''8744''45'lattice_344 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_Lattice_512
d_'8743''45''8744''45'lattice_344 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_Lattice_512
du_'8743''45''8744''45'lattice_344 T_Lattice_512
v2
du_'8743''45''8744''45'lattice_344 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512
du_'8743''45''8744''45'lattice_344 :: T_Lattice_512 -> T_Lattice_512
du_'8743''45''8744''45'lattice_344 T_Lattice_512
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_3070
 -> T_Lattice_512)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_512
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070
-> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_592
      (T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0))
      (T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsLattice_3070
du_'8743''45''8744''45'isLattice_342 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._.poset
d_poset_348 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_poset_348 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_Poset_492
d_poset_348 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 = T_Lattice_512 -> T_Poset_492
du_poset_348 T_Lattice_512
v2
du_poset_348 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_poset_348 :: T_Lattice_512 -> T_Poset_492
du_poset_348 T_Lattice_512
v0
  = (T_Semilattice_10 -> T_Poset_492) -> AgdaAny -> T_Poset_492
forall a b. a -> b
coe
      T_Semilattice_10 -> T_Poset_492
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_poset_162
      ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8743''45'semilattice_306 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
-- Algebra.Lattice.Properties.Lattice._._≤_
d__'8804'__352 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny -> ()
d__'8804'__352 :: T_Level_18
-> T_Level_18 -> T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Level_18
d__'8804'__352 = T_Level_18
-> T_Level_18 -> T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Lattice.∨-∧-isOrderTheoreticLattice
d_'8744''45''8743''45'isOrderTheoreticLattice_356 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsLattice_348
d_'8744''45''8743''45'isOrderTheoreticLattice_356 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_IsLattice_348
d_'8744''45''8743''45'isOrderTheoreticLattice_356 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_IsLattice_348
du_'8744''45''8743''45'isOrderTheoreticLattice_356 T_Lattice_512
v2
du_'8744''45''8743''45'isOrderTheoreticLattice_356 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsLattice_348
du_'8744''45''8743''45'isOrderTheoreticLattice_356 :: T_Lattice_512 -> T_IsLattice_348
du_'8744''45''8743''45'isOrderTheoreticLattice_356 T_Lattice_512
v0
  = (T_IsPartialOrder_248
 -> (AgdaAny -> AgdaAny -> T_Σ_14)
 -> (AgdaAny -> AgdaAny -> T_Σ_14)
 -> T_IsLattice_348)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLattice_348
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> T_Σ_14)
-> T_IsLattice_348
MAlonzo.Code.Relation.Binary.Lattice.Structures.C_constructor_424
      ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
         ((T_Semilattice_10 -> T_Poset_492) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Semilattice_10 -> T_Poset_492
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_poset_162
            ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8743''45'semilattice_306 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))))
      ((T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_400 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_3754
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
         ((T_Lattice_512 -> T_IsCommutativeBand_612) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsCommutativeBand_612
du_'8743''45'isSemilattice_304 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
-- Algebra.Lattice.Properties.Lattice._._._≤_
d__'8804'__368 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny -> ()
d__'8804'__368 :: T_Level_18
-> T_Level_18 -> T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Level_18
d__'8804'__368 = T_Level_18
-> T_Level_18 -> T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Lattice._.sound
d_sound_380 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sound_380 :: T_Level_18
-> T_Level_18
-> T_Lattice_512
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_sound_380 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 = T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_380 T_Lattice_512
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_sound_380 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_380 :: T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_380 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
      (T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> T_IsLattice_3070
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
      AgdaAny
v1
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
         (\ AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v6)
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
         AgdaAny
v1
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                     ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1))
            AgdaAny
v1
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                     ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                        ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1))
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2))
               AgdaAny
v1
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                     ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                        ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                           ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1
                     ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2))
                  AgdaAny
v1 AgdaAny
v1
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                     (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                        ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                           ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                              ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                  ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'absorbs'45''8744'_3122
                     (T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0)) AgdaAny
v1
                     AgdaAny
v2))
               ((T_IsLattice_3070
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_3070
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'cong'737'_3124
                  ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_3094
                     (T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0)) AgdaAny
v2
                     AgdaAny
v1)))
            ((T_IsLattice_3070
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_3070
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'cong'737'_3124
               ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1)
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))
-- Algebra.Lattice.Properties.Lattice._.complete
d_complete_392 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_complete_392 :: T_Level_18
-> T_Level_18
-> T_Lattice_512
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_complete_392 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 = T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_392 T_Lattice_512
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_complete_392 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_392 :: T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_392 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
      (T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
         ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> T_IsLattice_3070
forall a b. a -> b
coe
            T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
      ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1)
      AgdaAny
v2
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
         (\ AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 AgdaAny
v6)
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1)
         AgdaAny
v2
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
               ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                  ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                     ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1)
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2))
            AgdaAny
v2
            (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                  ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                     ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                        ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2))
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1))
               AgdaAny
v2
               (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_370
                  (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
                     ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
                        ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                           ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v2
                     ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1))
                  AgdaAny
v2 AgdaAny
v2
                  (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                     (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
                        ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
                           ((T_IsLattice_3070 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
                              ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))))
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
                  ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'absorbs'45''8743'_3120
                     (T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0)) AgdaAny
v2
                     AgdaAny
v1))
               ((T_IsLattice_3070
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_3070
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'cong'737'_3132
                  ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_3100
                     (T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0)) AgdaAny
v1
                     AgdaAny
v2)))
            ((T_IsLattice_3070
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_3070
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'cong'737'_3132
               ((T_Lattice_512 -> T_IsLattice_3070) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_536 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
               ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))
-- Algebra.Lattice.Properties.Lattice._.supremum
d_supremum_400 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_supremum_400 :: T_Level_18
-> T_Level_18 -> T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Σ_14
d_supremum_400 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2 AgdaAny
v3 AgdaAny
v4 = T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_400 T_Lattice_512
v2 AgdaAny
v3 AgdaAny
v4
du_supremum_400 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_supremum_400 :: T_Lattice_512 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_400 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2
  = (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
      ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_380 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
         ((T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Lattice.Structures.du_x'8804'x'8744'y_38
            ((T_Semilattice_10 -> T_IsJoinSemilattice_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Semilattice_10 -> T_IsJoinSemilattice_22
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
               ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
      ((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
         ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_380 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
            ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
            ((T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsJoinSemilattice_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Lattice.Structures.du_y'8804'x'8744'y_50
               ((T_Semilattice_10 -> T_IsJoinSemilattice_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Semilattice_10 -> T_IsJoinSemilattice_22
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
                  ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
               (T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_380 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)
                 ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 T_Lattice_512
v0 AgdaAny
v1 AgdaAny
v2)
                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                 ((T_IsJoinSemilattice_22
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                    T_IsJoinSemilattice_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Lattice.Structures.du_'8744''45'least_64
                    ((T_Semilattice_10 -> T_IsJoinSemilattice_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Semilattice_10 -> T_IsJoinSemilattice_22
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
                       ((T_Lattice_512 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_Semilattice_10
du_'8744''45'semilattice_330 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0)))
                    AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_392 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                    ((T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_392 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))))))
-- Algebra.Lattice.Properties.Lattice.∨-∧-orderTheoreticLattice
d_'8744''45''8743''45'orderTheoreticLattice_412 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_Lattice_394
d_'8744''45''8743''45'orderTheoreticLattice_412 :: T_Level_18 -> T_Level_18 -> T_Lattice_512 -> T_Lattice_394
d_'8744''45''8743''45'orderTheoreticLattice_412 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_512
v2
  = T_Lattice_512 -> T_Lattice_394
du_'8744''45''8743''45'orderTheoreticLattice_412 T_Lattice_512
v2
du_'8744''45''8743''45'orderTheoreticLattice_412 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_Lattice_394
du_'8744''45''8743''45'orderTheoreticLattice_412 :: T_Lattice_512 -> T_Lattice_394
du_'8744''45''8743''45'orderTheoreticLattice_412 T_Lattice_512
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_348
 -> T_Lattice_394)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_394
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_348
-> T_Lattice_394
MAlonzo.Code.Relation.Binary.Lattice.Bundles.C_constructor_498
      (T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__532 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0))
      (T_Lattice_512 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__534 (T_Lattice_512 -> T_Lattice_512
forall a b. a -> b
coe T_Lattice_512
v0))
      ((T_Lattice_512 -> T_IsLattice_348) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_512 -> T_IsLattice_348
du_'8744''45''8743''45'isOrderTheoreticLattice_356 (T_Lattice_512 -> AgdaAny
forall a b. a -> b
coe T_Lattice_512
v0))