{-# 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_112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Idempotent_112 :: T_Level_18
-> T_Level_18
-> T_Lattice_500
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_Idempotent_112 = T_Level_18
-> T_Level_18
-> T_Lattice_500
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Lattice._.IsBand
d_IsBand_210 :: p -> p -> p -> p -> T_Level_18
d_IsBand_210 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Lattice.Properties.Lattice._.IsMagma
d_IsMagma_250 :: p -> p -> p -> p -> T_Level_18
d_IsMagma_250 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Lattice.Properties.Lattice._.IsSemigroup
d_IsSemigroup_278 :: p -> p -> p -> p -> T_Level_18
d_IsSemigroup_278 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Lattice.Properties.Lattice._.IsBand.idem
d_idem_392 ::
  MAlonzo.Code.Algebra.Structures.T_IsBand_508 -> AgdaAny -> AgdaAny
d_idem_392 :: T_IsBand_508 -> AgdaAny -> AgdaAny
d_idem_392 T_IsBand_508
v0
  = (T_IsBand_508 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBand_508 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_idem_518 (T_IsBand_508 -> AgdaAny
forall a b. a -> b
coe T_IsBand_508
v0)
-- Algebra.Lattice.Properties.Lattice._.IsBand.isSemigroup
d_isSemigroup_400 ::
  MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_isSemigroup_400 :: T_IsBand_508 -> T_IsSemigroup_472
d_isSemigroup_400 T_IsBand_508
v0
  = (T_IsBand_508 -> T_IsSemigroup_472) -> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe T_IsBand_508 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (T_IsBand_508 -> AgdaAny
forall a b. a -> b
coe T_IsBand_508
v0)
-- Algebra.Lattice.Properties.Lattice._.IsMagma.isEquivalence
d_isEquivalence_1550 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_1550 :: T_IsMagma_176 -> T_IsEquivalence_26
d_isEquivalence_1550 T_IsMagma_176
v0
  = (T_IsMagma_176 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (T_IsMagma_176 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_176
v0)
-- Algebra.Lattice.Properties.Lattice._.IsMagma.∙-cong
d_'8729''45'cong_1564 ::
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8729''45'cong_1564 :: T_IsMagma_176
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8729''45'cong_1564 T_IsMagma_176
v0
  = (T_IsMagma_176
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsMagma_176
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186 (T_IsMagma_176 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_176
v0)
-- Algebra.Lattice.Properties.Lattice._.IsSemigroup.assoc
d_assoc_2404 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_assoc_2404 :: T_IsSemigroup_472 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_assoc_2404 T_IsSemigroup_472
v0
  = (T_IsSemigroup_472 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_assoc_482 (T_IsSemigroup_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
v0)
-- Algebra.Lattice.Properties.Lattice._.IsSemigroup.isMagma
d_isMagma_2408 ::
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_isMagma_2408 :: T_IsSemigroup_472 -> T_IsMagma_176
d_isMagma_2408 T_IsSemigroup_472
v0
  = (T_IsSemigroup_472 -> T_IsMagma_176) -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe T_IsSemigroup_472 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_480 (T_IsSemigroup_472 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_472
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice
d_IsLattice_2732 :: p -> p -> p -> p -> p -> T_Level_18
d_IsLattice_2732 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Algebra.Lattice.Properties.Lattice._.IsSemilattice
d_IsSemilattice_2736 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_IsSemilattice_2736 :: T_Level_18
-> T_Level_18
-> T_Lattice_500
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_IsSemilattice_2736 = T_Level_18
-> T_Level_18
-> T_Lattice_500
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Lattice._.IsLattice.absorptive
d_absorptive_3036 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_absorptive_3036 :: T_IsLattice_2962 -> T_Σ_14
d_absorptive_3036 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsLattice_2962 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_2998 (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.isEquivalence
d_isEquivalence_3038 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_3038 :: T_IsLattice_2962 -> T_IsEquivalence_26
d_isEquivalence_3038 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∧-assoc
d_'8743''45'assoc_3052 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'assoc_3052 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'assoc_3052 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_2994
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∧-comm
d_'8743''45'comm_3054 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'comm_3054 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'comm_3054 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_2992
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∧-cong
d_'8743''45'cong_3056 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'cong_3056 :: T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8743''45'cong_3056 T_IsLattice_2962
v0
  = (T_IsLattice_2962
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_2996
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∨-assoc
d_'8744''45'assoc_3064 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'assoc_3064 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'assoc_3064 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_2988
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∨-comm
d_'8744''45'comm_3066 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'comm_3066 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'comm_3066 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_2986
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Properties.Lattice._.IsLattice.∨-cong
d_'8744''45'cong_3068 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'cong_3068 :: T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8744''45'cong_3068 T_IsLattice_2962
v0
  = (T_IsLattice_2962
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_2990
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Properties.Lattice.∧-idem
d_'8743''45'idem_3182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny
d_'8743''45'idem_3182 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny
d_'8743''45'idem_3182 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 AgdaAny
v3 = T_Lattice_500 -> AgdaAny -> AgdaAny
du_'8743''45'idem_3182 T_Lattice_500
v2 AgdaAny
v3
du_'8743''45'idem_3182 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny
du_'8743''45'idem_3182 :: T_Lattice_500 -> AgdaAny -> AgdaAny
du_'8743''45'idem_3182 T_Lattice_500
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_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
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'_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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
               ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                  ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
            ((T_IsLattice_2962 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
               T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
               ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))))
         ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v1)
         ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v1
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
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'_368
            (((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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                  ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                     ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v1
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v1)))
            AgdaAny
v1 AgdaAny
v1
            (let v2 :: AgdaAny -> AgdaAny
v2
                   = T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                       ((T_IsLattice_2962 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                          T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                          ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (((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'_492
                  (((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
                     ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
            ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'absorbs'45''8744'_3014
               (T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0)) AgdaAny
v1
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v1)))
         ((T_IsLattice_2962
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_2962
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'cong'737'_3016
            ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v1
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v1))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'absorbs'45''8743'_3012
               (T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0)) AgdaAny
v1
               AgdaAny
v1)))
-- Algebra.Lattice.Properties.Lattice.∧-isMagma
d_'8743''45'isMagma_3186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8743''45'isMagma_3186 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsMagma_176
d_'8743''45'isMagma_3186 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 = T_Lattice_500 -> T_IsMagma_176
du_'8743''45'isMagma_3186 T_Lattice_500
v2
du_'8743''45'isMagma_3186 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'8743''45'isMagma_3186 :: T_Lattice_500 -> T_IsMagma_176
du_'8743''45'isMagma_3186 T_Lattice_500
v0
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_176)
-> AgdaAny -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
      ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_IsLattice_2962
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_2996
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
-- Algebra.Lattice.Properties.Lattice.∧-isSemigroup
d_'8743''45'isSemigroup_3188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8743''45'isSemigroup_3188 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsSemigroup_472
d_'8743''45'isSemigroup_3188 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsSemigroup_472
du_'8743''45'isSemigroup_3188 T_Lattice_500
v2
du_'8743''45'isSemigroup_3188 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'8743''45'isSemigroup_3188 :: T_Lattice_500 -> T_IsSemigroup_472
du_'8743''45'isSemigroup_3188 T_Lattice_500
v0
  = (T_IsMagma_176
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe
      T_IsMagma_176
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
      ((T_Lattice_500 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsMagma_176
du_'8743''45'isMagma_3186 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_2994
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
-- Algebra.Lattice.Properties.Lattice.∧-isBand
d_'8743''45'isBand_3190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8743''45'isBand_3190 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsBand_508
d_'8743''45'isBand_3190 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 = T_Lattice_500 -> T_IsBand_508
du_'8743''45'isBand_3190 T_Lattice_500
v2
du_'8743''45'isBand_3190 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
du_'8743''45'isBand_3190 :: T_Lattice_500 -> T_IsBand_508
du_'8743''45'isBand_3190 T_Lattice_500
v0
  = (T_IsSemigroup_472 -> (AgdaAny -> AgdaAny) -> T_IsBand_508)
-> AgdaAny -> AgdaAny -> T_IsBand_508
forall a b. a -> b
coe
      T_IsSemigroup_472 -> (AgdaAny -> AgdaAny) -> T_IsBand_508
MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_11205
      ((T_Lattice_500 -> T_IsSemigroup_472) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsSemigroup_472
du_'8743''45'isSemigroup_3188 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_Lattice_500 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny
du_'8743''45'idem_3182 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice.∧-isSemilattice
d_'8743''45'isSemilattice_3192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8743''45'isSemilattice_3192 :: T_Level_18
-> T_Level_18 -> T_Lattice_500 -> T_IsCommutativeBand_590
d_'8743''45'isSemilattice_3192 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsCommutativeBand_590
du_'8743''45'isSemilattice_3192 T_Lattice_500
v2
du_'8743''45'isSemilattice_3192 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
du_'8743''45'isSemilattice_3192 :: T_Lattice_500 -> T_IsCommutativeBand_590
du_'8743''45'isSemilattice_3192 T_Lattice_500
v0
  = (T_IsBand_508
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_590
forall a b. a -> b
coe
      T_IsBand_508
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Structures.C_IsCommutativeBand'46'constructor_13109
      ((T_Lattice_500 -> T_IsBand_508) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsBand_508
du_'8743''45'isBand_3190 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_2992
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
-- Algebra.Lattice.Properties.Lattice.∧-semilattice
d_'8743''45'semilattice_3194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8743''45'semilattice_3194 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Semilattice_10
d_'8743''45'semilattice_3194 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_Semilattice_10
du_'8743''45'semilattice_3194 T_Lattice_500
v2
du_'8743''45'semilattice_3194 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8743''45'semilattice_3194 :: T_Lattice_500 -> T_Semilattice_10
du_'8743''45'semilattice_3194 T_Lattice_500
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_590 -> T_Semilattice_10)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_590 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Bundles.C_Semilattice'46'constructor_193
      (T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_Lattice_500 -> T_IsCommutativeBand_590) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsCommutativeBand_590
du_'8743''45'isSemilattice_3192 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_3198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_3198 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_3198 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_3198 T_Lattice_500
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_3198 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_3198 :: T_Lattice_500 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_3198 T_Lattice_500
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_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8743''45'semilattice_3194 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_3200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_3200 :: T_Level_18
-> T_Level_18 -> T_Lattice_500 -> T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_3200 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_3200 T_Lattice_500
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_3200 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_3200 :: T_Lattice_500 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_3200 T_Lattice_500
v0
  = (T_Semilattice_10 -> T_IsMeetSemilattice_180)
-> AgdaAny -> T_IsMeetSemilattice_180
forall a b. a -> b
coe
      T_Semilattice_10 -> T_IsMeetSemilattice_180
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticMeetSemilattice_176
      ((T_Lattice_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8743''45'semilattice_3194 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_3202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_3202 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_3202 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_3202 T_Lattice_500
v2
du_'8743''45'orderTheoreticJoinSemilattice_3202 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_3202 :: T_Lattice_500 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_3202 T_Lattice_500
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_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8743''45'semilattice_3194 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_3204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_3204 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_3204 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_3204 T_Lattice_500
v2
du_'8743''45'orderTheoreticMeetSemilattice_3204 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_3204 :: T_Lattice_500 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_3204 T_Lattice_500
v0
  = (T_Semilattice_10 -> T_MeetSemilattice_200)
-> AgdaAny -> T_MeetSemilattice_200
forall a b. a -> b
coe
      T_Semilattice_10 -> T_MeetSemilattice_200
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticMeetSemilattice_180
      ((T_Lattice_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8743''45'semilattice_3194 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice.∨-idem
d_'8744''45'idem_3206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny
d_'8744''45'idem_3206 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny
d_'8744''45'idem_3206 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 AgdaAny
v3 = T_Lattice_500 -> AgdaAny -> AgdaAny
du_'8744''45'idem_3206 T_Lattice_500
v2 AgdaAny
v3
du_'8744''45'idem_3206 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny
du_'8744''45'idem_3206 :: T_Lattice_500 -> AgdaAny -> AgdaAny
du_'8744''45'idem_3206 T_Lattice_500
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_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
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'_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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
               ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                  ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
            ((T_IsLattice_2962 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
               T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
               ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))))
         ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v1)
         ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v1
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
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'_368
            (((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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                  ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                     ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v1
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v1))
            AgdaAny
v1 AgdaAny
v1
            (let v2 :: AgdaAny -> AgdaAny
v2
                   = T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                       ((T_IsLattice_2962 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                          T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                          ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (((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'_492
                  (((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
                     ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
            ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'absorbs'45''8743'_3012
               (T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0)) AgdaAny
v1
               AgdaAny
v1))
         ((T_IsLattice_2962
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_2962
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'cong'737'_3024
            ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v1)
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ((T_Lattice_500 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny
du_'8743''45'idem_3182 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
-- Algebra.Lattice.Properties.Lattice.∨-isMagma
d_'8744''45'isMagma_3210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8744''45'isMagma_3210 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsMagma_176
d_'8744''45'isMagma_3210 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 = T_Lattice_500 -> T_IsMagma_176
du_'8744''45'isMagma_3210 T_Lattice_500
v2
du_'8744''45'isMagma_3210 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'8744''45'isMagma_3210 :: T_Lattice_500 -> T_IsMagma_176
du_'8744''45'isMagma_3210 T_Lattice_500
v0
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_176)
-> AgdaAny -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
      ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_IsLattice_2962
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_2990
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
-- Algebra.Lattice.Properties.Lattice.∨-isSemigroup
d_'8744''45'isSemigroup_3212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8744''45'isSemigroup_3212 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsSemigroup_472
d_'8744''45'isSemigroup_3212 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsSemigroup_472
du_'8744''45'isSemigroup_3212 T_Lattice_500
v2
du_'8744''45'isSemigroup_3212 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'8744''45'isSemigroup_3212 :: T_Lattice_500 -> T_IsSemigroup_472
du_'8744''45'isSemigroup_3212 T_Lattice_500
v0
  = (T_IsMagma_176
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe
      T_IsMagma_176
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
      ((T_Lattice_500 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsMagma_176
du_'8744''45'isMagma_3210 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_2988
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
-- Algebra.Lattice.Properties.Lattice.∨-isBand
d_'8744''45'isBand_3214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8744''45'isBand_3214 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsBand_508
d_'8744''45'isBand_3214 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 = T_Lattice_500 -> T_IsBand_508
du_'8744''45'isBand_3214 T_Lattice_500
v2
du_'8744''45'isBand_3214 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
du_'8744''45'isBand_3214 :: T_Lattice_500 -> T_IsBand_508
du_'8744''45'isBand_3214 T_Lattice_500
v0
  = (T_IsSemigroup_472 -> (AgdaAny -> AgdaAny) -> T_IsBand_508)
-> AgdaAny -> AgdaAny -> T_IsBand_508
forall a b. a -> b
coe
      T_IsSemigroup_472 -> (AgdaAny -> AgdaAny) -> T_IsBand_508
MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_11205
      ((T_Lattice_500 -> T_IsSemigroup_472) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsSemigroup_472
du_'8744''45'isSemigroup_3212 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_Lattice_500 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny
du_'8744''45'idem_3206 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice.∨-isSemilattice
d_'8744''45'isSemilattice_3216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8744''45'isSemilattice_3216 :: T_Level_18
-> T_Level_18 -> T_Lattice_500 -> T_IsCommutativeBand_590
d_'8744''45'isSemilattice_3216 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsCommutativeBand_590
du_'8744''45'isSemilattice_3216 T_Lattice_500
v2
du_'8744''45'isSemilattice_3216 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
du_'8744''45'isSemilattice_3216 :: T_Lattice_500 -> T_IsCommutativeBand_590
du_'8744''45'isSemilattice_3216 T_Lattice_500
v0
  = (T_IsBand_508
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_590
forall a b. a -> b
coe
      T_IsBand_508
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Structures.C_IsCommutativeBand'46'constructor_13109
      ((T_Lattice_500 -> T_IsBand_508) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsBand_508
du_'8744''45'isBand_3214 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_2986
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
-- Algebra.Lattice.Properties.Lattice.∨-semilattice
d_'8744''45'semilattice_3218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8744''45'semilattice_3218 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Semilattice_10
d_'8744''45'semilattice_3218 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 T_Lattice_500
v2
du_'8744''45'semilattice_3218 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8744''45'semilattice_3218 :: T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 T_Lattice_500
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_590 -> T_Semilattice_10)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_590 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Bundles.C_Semilattice'46'constructor_193
      (T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_Lattice_500 -> T_IsCommutativeBand_590) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsCommutativeBand_590
du_'8744''45'isSemilattice_3216 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_3222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_3222 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_3222 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_3222 T_Lattice_500
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_3222 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_3222 :: T_Lattice_500 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_3222 T_Lattice_500
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_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_3224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_3224 :: T_Level_18
-> T_Level_18 -> T_Lattice_500 -> T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_3224 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_3224 T_Lattice_500
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_3224 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_3224 :: T_Lattice_500 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_3224 T_Lattice_500
v0
  = (T_Semilattice_10 -> T_IsMeetSemilattice_180)
-> AgdaAny -> T_IsMeetSemilattice_180
forall a b. a -> b
coe
      T_Semilattice_10 -> T_IsMeetSemilattice_180
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticMeetSemilattice_176
      ((T_Lattice_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_3226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_3226 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_3226 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_3226 T_Lattice_500
v2
du_'8743''45'orderTheoreticJoinSemilattice_3226 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_3226 :: T_Lattice_500 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_3226 T_Lattice_500
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_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_3228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_3228 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_3228 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_3228 T_Lattice_500
v2
du_'8743''45'orderTheoreticMeetSemilattice_3228 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_3228 :: T_Lattice_500 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_3228 T_Lattice_500
v0
  = (T_Semilattice_10 -> T_MeetSemilattice_200)
-> AgdaAny -> T_MeetSemilattice_200
forall a b. a -> b
coe
      T_Semilattice_10 -> T_MeetSemilattice_200
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticMeetSemilattice_180
      ((T_Lattice_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice.∧-∨-isLattice
d_'8743''45''8744''45'isLattice_3230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
d_'8743''45''8744''45'isLattice_3230 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsLattice_2962
d_'8743''45''8744''45'isLattice_3230 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsLattice_2962
du_'8743''45''8744''45'isLattice_3230 T_Lattice_500
v2
du_'8743''45''8744''45'isLattice_3230 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
du_'8743''45''8744''45'isLattice_3230 :: T_Lattice_500 -> T_IsLattice_2962
du_'8743''45''8744''45'isLattice_3230 T_Lattice_500
v0
  = (T_IsEquivalence_26
 -> (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_2962)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsLattice_2962
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (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_2962
MAlonzo.Code.Algebra.Lattice.Structures.C_IsLattice'46'constructor_36793
      ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_2992
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_2994
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_IsLattice_2962
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_2996
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_2986
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_2988
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_IsLattice_2962
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_2990
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
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_2962 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_2962 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_2998
            ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))))
-- Algebra.Lattice.Properties.Lattice.∧-∨-lattice
d_'8743''45''8744''45'lattice_3232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
d_'8743''45''8744''45'lattice_3232 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Lattice_500
d_'8743''45''8744''45'lattice_3232 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_Lattice_500
du_'8743''45''8744''45'lattice_3232 T_Lattice_500
v2
du_'8743''45''8744''45'lattice_3232 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
du_'8743''45''8744''45'lattice_3232 :: T_Lattice_500 -> T_Lattice_500
du_'8743''45''8744''45'lattice_3232 T_Lattice_500
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_2962
 -> T_Lattice_500)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_500
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962
-> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.C_Lattice'46'constructor_7925
      (T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0))
      (T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsLattice_2962
du_'8743''45''8744''45'isLattice_3230 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._.poset
d_poset_3236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_poset_3236 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Poset_314
d_poset_3236 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 = T_Lattice_500 -> T_Poset_314
du_poset_3236 T_Lattice_500
v2
du_poset_3236 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
du_poset_3236 :: T_Lattice_500 -> T_Poset_314
du_poset_3236 T_Lattice_500
v0
  = (T_Semilattice_10 -> T_Poset_314) -> AgdaAny -> T_Poset_314
forall a b. a -> b
coe
      T_Semilattice_10 -> T_Poset_314
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_poset_162
      ((T_Lattice_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8743''45'semilattice_3194 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
-- Algebra.Lattice.Properties.Lattice._._≤_
d__'8804'__3240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny -> ()
d__'8804'__3240 :: T_Level_18
-> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Level_18
d__'8804'__3240 = T_Level_18
-> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Lattice.∨-∧-isOrderTheoreticLattice
d_'8744''45''8743''45'isOrderTheoreticLattice_3244 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsLattice_340
d_'8744''45''8743''45'isOrderTheoreticLattice_3244 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_IsLattice_340
d_'8744''45''8743''45'isOrderTheoreticLattice_3244 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_IsLattice_340
du_'8744''45''8743''45'isOrderTheoreticLattice_3244 T_Lattice_500
v2
du_'8744''45''8743''45'isOrderTheoreticLattice_3244 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsLattice_340
du_'8744''45''8743''45'isOrderTheoreticLattice_3244 :: T_Lattice_500 -> T_IsLattice_340
du_'8744''45''8743''45'isOrderTheoreticLattice_3244 T_Lattice_500
v0
  = (T_IsPartialOrder_174
 -> (AgdaAny -> AgdaAny -> T_Σ_14)
 -> (AgdaAny -> AgdaAny -> T_Σ_14)
 -> T_IsLattice_340)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLattice_340
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> T_Σ_14)
-> T_IsLattice_340
MAlonzo.Code.Relation.Binary.Lattice.Structures.C_IsLattice'46'constructor_14941
      ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
         ((T_Semilattice_10 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Semilattice_10 -> T_Poset_314
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_poset_162
            ((T_Lattice_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8743''45'semilattice_3194 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))))
      ((T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_3288 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_590 -> AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_3640
         ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
         ((T_Lattice_500 -> T_IsCommutativeBand_590) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsCommutativeBand_590
du_'8743''45'isSemilattice_3192 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
-- Algebra.Lattice.Properties.Lattice._._._≤_
d__'8804'__3256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny -> ()
d__'8804'__3256 :: T_Level_18
-> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Level_18
d__'8804'__3256 = T_Level_18
-> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Lattice._.sound
d_sound_3268 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sound_3268 :: T_Level_18
-> T_Level_18
-> T_Lattice_500
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_sound_3268 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 = T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_3268 T_Lattice_500
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_sound_3268 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_3268 :: T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_3268 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
      (T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> T_IsLattice_2962
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
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_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
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'_368
            (((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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                  ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                     ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v2)
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
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'_368
               (((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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                     ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                        ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v2 AgdaAny
v1))
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
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'_368
                  (((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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                        ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                           ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1
                     ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v2))
                  AgdaAny
v1 AgdaAny
v1
                  (let v4 :: AgdaAny -> AgdaAny
v4
                         = T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                             ((T_IsLattice_2962 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                                T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                                ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                   T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524
                                   (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (((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'_492
                        (((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
                           ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v4))
                        (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
                  ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'absorbs'45''8744'_3014
                     (T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0)) AgdaAny
v1
                     AgdaAny
v2))
               ((T_IsLattice_2962
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_2962
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'cong'737'_3016
                  ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_2986
                     (T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0)) AgdaAny
v2
                     AgdaAny
v1)))
            ((T_IsLattice_2962
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_2962
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8743''45'cong'737'_3016
               ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v2 AgdaAny
v1)
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))
-- Algebra.Lattice.Properties.Lattice._.complete
d_complete_3280 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_complete_3280 :: T_Level_18
-> T_Level_18
-> T_Lattice_500
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_complete_3280 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 = T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_3280 T_Lattice_500
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_complete_3280 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_3280 :: T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_3280 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
      (T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
         ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> T_IsLattice_2962
forall a b. a -> b
coe
            T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
      ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
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_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
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'_368
            (((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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                  ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                     ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v2 AgdaAny
v1)
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v2
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
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'_368
               (((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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                     ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                        ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v2
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v2))
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v2
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
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'_368
                  (((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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                        ((T_IsLattice_2962 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                           ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))))
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
v0 AgdaAny
v2
                     ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v2 AgdaAny
v1))
                  AgdaAny
v2 AgdaAny
v2
                  (let v4 :: AgdaAny -> AgdaAny
v4
                         = T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                             ((T_IsLattice_2962 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                                T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
                                ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                   T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524
                                   (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (((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'_492
                        (((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
                           ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v4))
                        (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
                  ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'absorbs'45''8743'_3012
                     (T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0)) AgdaAny
v2
                     AgdaAny
v1))
               ((T_IsLattice_2962
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_2962
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'cong'737'_3024
                  ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_2992
                     (T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0)) AgdaAny
v1
                     AgdaAny
v2)))
            ((T_IsLattice_2962
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_2962
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.du_'8744''45'cong'737'_3024
               ((T_Lattice_500 -> T_IsLattice_2962) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Bundles.d_isLattice_524 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
               ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 T_Lattice_500
v0 AgdaAny
v1 AgdaAny
v2)
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))
-- Algebra.Lattice.Properties.Lattice._.supremum
d_supremum_3288 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_supremum_3288 :: T_Level_18
-> T_Level_18 -> T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Σ_14
d_supremum_3288 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2 AgdaAny
v3 AgdaAny
v4 = T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_3288 T_Lattice_500
v2 AgdaAny
v3 AgdaAny
v4
du_supremum_3288 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_supremum_3288 :: T_Lattice_500 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_3288 T_Lattice_500
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_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_3268 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
         ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
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_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
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_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_3268 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
            ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
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_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
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_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_3268 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)
                 ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 T_Lattice_500
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_500 -> T_Semilattice_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_Semilattice_10
du_'8744''45'semilattice_3218 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0)))
                    AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ((T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_3280 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
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_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_3280 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
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_3300 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_Lattice_386
d_'8744''45''8743''45'orderTheoreticLattice_3300 :: T_Level_18 -> T_Level_18 -> T_Lattice_500 -> T_Lattice_386
d_'8744''45''8743''45'orderTheoreticLattice_3300 ~T_Level_18
v0 ~T_Level_18
v1 T_Lattice_500
v2
  = T_Lattice_500 -> T_Lattice_386
du_'8744''45''8743''45'orderTheoreticLattice_3300 T_Lattice_500
v2
du_'8744''45''8743''45'orderTheoreticLattice_3300 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_Lattice_386
du_'8744''45''8743''45'orderTheoreticLattice_3300 :: T_Lattice_500 -> T_Lattice_386
du_'8744''45''8743''45'orderTheoreticLattice_3300 T_Lattice_500
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_340
 -> T_Lattice_386)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_386
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_340
-> T_Lattice_386
MAlonzo.Code.Relation.Binary.Lattice.Bundles.C_Lattice'46'constructor_8977
      (T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__520 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0))
      (T_Lattice_500 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__522 (T_Lattice_500 -> T_Lattice_500
forall a b. a -> b
coe T_Lattice_500
v0))
      ((T_Lattice_500 -> T_IsLattice_340) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_500 -> T_IsLattice_340
du_'8744''45''8743''45'isOrderTheoreticLattice_3244 (T_Lattice_500 -> AgdaAny
forall a b. a -> b
coe T_Lattice_500
v0))