{-# 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.DistributiveLattice 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.Lattice
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.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Lattice.Bundles
import qualified MAlonzo.Code.Relation.Binary.Lattice.Structures

-- Algebra.Lattice.Properties.DistributiveLattice._.IsDistributiveLattice
d_IsDistributiveLattice_232 :: p -> p -> p -> p -> p -> ()
d_IsDistributiveLattice_232 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Algebra.Lattice.Properties.DistributiveLattice._.IsDistributiveLattice.isLattice
d_isLattice_460 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
d_isLattice_460 :: T_IsDistributiveLattice_3146 -> T_IsLattice_3070
d_isLattice_460 T_IsDistributiveLattice_3146
v0
  = (T_IsDistributiveLattice_3146 -> T_IsLattice_3070)
-> Any -> T_IsLattice_3070
forall a b. a -> b
coe
      T_IsDistributiveLattice_3146 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Structures.d_isLattice_3158 (T_IsDistributiveLattice_3146 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3146
v0)
-- Algebra.Lattice.Properties.DistributiveLattice._.IsDistributiveLattice.∧-distrib-∨
d_'8743''45'distrib'45''8744'_484 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'distrib'45''8744'_484 :: T_IsDistributiveLattice_3146 -> T_Σ_14
d_'8743''45'distrib'45''8744'_484 T_IsDistributiveLattice_3146
v0
  = (T_IsDistributiveLattice_3146 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
      T_IsDistributiveLattice_3146 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'distrib'45''8744'_3162
      (T_IsDistributiveLattice_3146 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3146
v0)
-- Algebra.Lattice.Properties.DistributiveLattice._.IsDistributiveLattice.∨-distrib-∧
d_'8744''45'distrib'45''8743'_502 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'distrib'45''8743'_502 :: T_IsDistributiveLattice_3146 -> T_Σ_14
d_'8744''45'distrib'45''8743'_502 T_IsDistributiveLattice_3146
v0
  = (T_IsDistributiveLattice_3146 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
      T_IsDistributiveLattice_3146 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'distrib'45''8743'_3160
      (T_IsDistributiveLattice_3146 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3146
v0)
-- Algebra.Lattice.Properties.DistributiveLattice._.poset
d_poset_692 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_poset_692 :: () -> () -> T_DistributiveLattice_598 -> T_Poset_492
d_poset_692 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2 = T_DistributiveLattice_598 -> T_Poset_492
du_poset_692 T_DistributiveLattice_598
v2
du_poset_692 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_poset_692 :: T_DistributiveLattice_598 -> T_Poset_492
du_poset_692 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_Poset_492
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_Poset_492) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_Poset_492
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_poset_162
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_306
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-idem
d_'8743''45'idem_694 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  AgdaAny -> AgdaAny
d_'8743''45'idem_694 :: () -> () -> T_DistributiveLattice_598 -> Any -> Any
d_'8743''45'idem_694 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2 = T_DistributiveLattice_598 -> Any -> Any
du_'8743''45'idem_694 T_DistributiveLattice_598
v2
du_'8743''45'idem_694 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  AgdaAny -> AgdaAny
du_'8743''45'idem_694 :: T_DistributiveLattice_598 -> Any -> Any
du_'8743''45'idem_694 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
      T_Lattice_512 -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'idem_294
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isBand
d_'8743''45'isBand_696 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
d_'8743''45'isBand_696 :: () -> () -> T_DistributiveLattice_598 -> T_IsBand_526
d_'8743''45'isBand_696 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2 = T_DistributiveLattice_598 -> T_IsBand_526
du_'8743''45'isBand_696 T_DistributiveLattice_598
v2
du_'8743''45'isBand_696 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
du_'8743''45'isBand_696 :: T_DistributiveLattice_598 -> T_IsBand_526
du_'8743''45'isBand_696 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsBand_526) -> Any -> T_IsBand_526
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsBand_526
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'isBand_302
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isMagma
d_'8743''45'isMagma_698 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'8743''45'isMagma_698 :: () -> () -> T_DistributiveLattice_598 -> T_IsMagma_178
d_'8743''45'isMagma_698 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2 = T_DistributiveLattice_598 -> T_IsMagma_178
du_'8743''45'isMagma_698 T_DistributiveLattice_598
v2
du_'8743''45'isMagma_698 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'8743''45'isMagma_698 :: T_DistributiveLattice_598 -> T_IsMagma_178
du_'8743''45'isMagma_698 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsMagma_178) -> Any -> T_IsMagma_178
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsMagma_178
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'isMagma_298
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_700 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_700 :: () -> () -> T_DistributiveLattice_598 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_700 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_700 T_DistributiveLattice_598
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_700 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_700 :: T_DistributiveLattice_598 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_700 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_IsJoinSemilattice_22
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_IsJoinSemilattice_22) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_IsJoinSemilattice_22
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_306
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_702 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_702 :: () -> () -> T_DistributiveLattice_598 -> T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_702 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_702 T_DistributiveLattice_598
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_702 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_702 :: T_DistributiveLattice_598 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_702 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_IsMeetSemilattice_184
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_IsMeetSemilattice_184) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_IsMeetSemilattice_184
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticMeetSemilattice_176
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_306
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isSemigroup
d_'8743''45'isSemigroup_704 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'8743''45'isSemigroup_704 :: () -> () -> T_DistributiveLattice_598 -> T_IsSemigroup_488
d_'8743''45'isSemigroup_704 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsSemigroup_488
du_'8743''45'isSemigroup_704 T_DistributiveLattice_598
v2
du_'8743''45'isSemigroup_704 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'8743''45'isSemigroup_704 :: T_DistributiveLattice_598 -> T_IsSemigroup_488
du_'8743''45'isSemigroup_704 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsSemigroup_488) -> Any -> T_IsSemigroup_488
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'isSemigroup_300
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isSemilattice
d_'8743''45'isSemilattice_706 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
d_'8743''45'isSemilattice_706 :: () -> () -> T_DistributiveLattice_598 -> T_IsCommutativeBand_612
d_'8743''45'isSemilattice_706 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsCommutativeBand_612
du_'8743''45'isSemilattice_706 T_DistributiveLattice_598
v2
du_'8743''45'isSemilattice_706 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
du_'8743''45'isSemilattice_706 :: T_DistributiveLattice_598 -> T_IsCommutativeBand_612
du_'8743''45'isSemilattice_706 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsCommutativeBand_612)
-> Any -> T_IsCommutativeBand_612
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'isSemilattice_304
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_708 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_708 :: () -> () -> T_DistributiveLattice_598 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_708 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_708 T_DistributiveLattice_598
v2
du_'8743''45'orderTheoreticJoinSemilattice_708 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_708 :: T_DistributiveLattice_598 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_708 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_JoinSemilattice_14
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_JoinSemilattice_14) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_JoinSemilattice_14
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticJoinSemilattice_182
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_306
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_710 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_710 :: () -> () -> T_DistributiveLattice_598 -> T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_710 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_710 T_DistributiveLattice_598
v2
du_'8743''45'orderTheoreticMeetSemilattice_710 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_710 :: T_DistributiveLattice_598 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_710 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_MeetSemilattice_204
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_MeetSemilattice_204) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_MeetSemilattice_204
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticMeetSemilattice_180
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_306
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-semilattice
d_'8743''45'semilattice_712 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8743''45'semilattice_712 :: () -> () -> T_DistributiveLattice_598 -> T_Semilattice_10
d_'8743''45'semilattice_712 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_Semilattice_10
du_'8743''45'semilattice_712 T_DistributiveLattice_598
v2
du_'8743''45'semilattice_712 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8743''45'semilattice_712 :: T_DistributiveLattice_598 -> T_Semilattice_10
du_'8743''45'semilattice_712 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_Semilattice_10) -> Any -> T_Semilattice_10
forall a b. a -> b
coe
      T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_306
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-∨-isLattice
d_'8743''45''8744''45'isLattice_714 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
d_'8743''45''8744''45'isLattice_714 :: () -> () -> T_DistributiveLattice_598 -> T_IsLattice_3070
d_'8743''45''8744''45'isLattice_714 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsLattice_3070
du_'8743''45''8744''45'isLattice_714 T_DistributiveLattice_598
v2
du_'8743''45''8744''45'isLattice_714 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
du_'8743''45''8744''45'isLattice_714 :: T_DistributiveLattice_598 -> T_IsLattice_3070
du_'8743''45''8744''45'isLattice_714 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsLattice_3070) -> Any -> T_IsLattice_3070
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45''8744''45'isLattice_342
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-∨-lattice
d_'8743''45''8744''45'lattice_716 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512
d_'8743''45''8744''45'lattice_716 :: () -> () -> T_DistributiveLattice_598 -> T_Lattice_512
d_'8743''45''8744''45'lattice_716 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_Lattice_512
du_'8743''45''8744''45'lattice_716 T_DistributiveLattice_598
v2
du_'8743''45''8744''45'lattice_716 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512
du_'8743''45''8744''45'lattice_716 :: T_DistributiveLattice_598 -> T_Lattice_512
du_'8743''45''8744''45'lattice_716 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_Lattice_512) -> Any -> T_Lattice_512
forall a b. a -> b
coe
      T_Lattice_512 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45''8744''45'lattice_344
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-idem
d_'8744''45'idem_718 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  AgdaAny -> AgdaAny
d_'8744''45'idem_718 :: () -> () -> T_DistributiveLattice_598 -> Any -> Any
d_'8744''45'idem_718 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2 = T_DistributiveLattice_598 -> Any -> Any
du_'8744''45'idem_718 T_DistributiveLattice_598
v2
du_'8744''45'idem_718 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  AgdaAny -> AgdaAny
du_'8744''45'idem_718 :: T_DistributiveLattice_598 -> Any -> Any
du_'8744''45'idem_718 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
      T_Lattice_512 -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'idem_318
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-isBand
d_'8744''45'isBand_720 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
d_'8744''45'isBand_720 :: () -> () -> T_DistributiveLattice_598 -> T_IsBand_526
d_'8744''45'isBand_720 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2 = T_DistributiveLattice_598 -> T_IsBand_526
du_'8744''45'isBand_720 T_DistributiveLattice_598
v2
du_'8744''45'isBand_720 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_526
du_'8744''45'isBand_720 :: T_DistributiveLattice_598 -> T_IsBand_526
du_'8744''45'isBand_720 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsBand_526) -> Any -> T_IsBand_526
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsBand_526
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'isBand_326
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-isMagma
d_'8744''45'isMagma_722 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'8744''45'isMagma_722 :: () -> () -> T_DistributiveLattice_598 -> T_IsMagma_178
d_'8744''45'isMagma_722 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2 = T_DistributiveLattice_598 -> T_IsMagma_178
du_'8744''45'isMagma_722 T_DistributiveLattice_598
v2
du_'8744''45'isMagma_722 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'8744''45'isMagma_722 :: T_DistributiveLattice_598 -> T_IsMagma_178
du_'8744''45'isMagma_722 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsMagma_178) -> Any -> T_IsMagma_178
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsMagma_178
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'isMagma_322
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_724 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_724 :: () -> () -> T_DistributiveLattice_598 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_724 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_724 T_DistributiveLattice_598
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_724 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_724 :: T_DistributiveLattice_598 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_724 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_IsJoinSemilattice_22
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_IsJoinSemilattice_22) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_IsJoinSemilattice_22
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_330
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_726 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_726 :: () -> () -> T_DistributiveLattice_598 -> T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_726 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_726 T_DistributiveLattice_598
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_726 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_726 :: T_DistributiveLattice_598 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_726 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_IsMeetSemilattice_184
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_IsMeetSemilattice_184) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_IsMeetSemilattice_184
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'isOrderTheoreticMeetSemilattice_176
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_330
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-isSemigroup
d_'8744''45'isSemigroup_728 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'8744''45'isSemigroup_728 :: () -> () -> T_DistributiveLattice_598 -> T_IsSemigroup_488
d_'8744''45'isSemigroup_728 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsSemigroup_488
du_'8744''45'isSemigroup_728 T_DistributiveLattice_598
v2
du_'8744''45'isSemigroup_728 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'8744''45'isSemigroup_728 :: T_DistributiveLattice_598 -> T_IsSemigroup_488
du_'8744''45'isSemigroup_728 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsSemigroup_488) -> Any -> T_IsSemigroup_488
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'isSemigroup_324
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-isSemilattice
d_'8744''45'isSemilattice_730 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
d_'8744''45'isSemilattice_730 :: () -> () -> T_DistributiveLattice_598 -> T_IsCommutativeBand_612
d_'8744''45'isSemilattice_730 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsCommutativeBand_612
du_'8744''45'isSemilattice_730 T_DistributiveLattice_598
v2
du_'8744''45'isSemilattice_730 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
du_'8744''45'isSemilattice_730 :: T_DistributiveLattice_598 -> T_IsCommutativeBand_612
du_'8744''45'isSemilattice_730 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsCommutativeBand_612)
-> Any -> T_IsCommutativeBand_612
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'isSemilattice_328
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_732 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_732 :: () -> () -> T_DistributiveLattice_598 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_732 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_732 T_DistributiveLattice_598
v2
du_'8743''45'orderTheoreticJoinSemilattice_732 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_732 :: T_DistributiveLattice_598 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_732 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_JoinSemilattice_14
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_JoinSemilattice_14) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_JoinSemilattice_14
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticJoinSemilattice_182
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_330
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_734 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_734 :: () -> () -> T_DistributiveLattice_598 -> T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_734 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_734 T_DistributiveLattice_598
v2
du_'8743''45'orderTheoreticMeetSemilattice_734 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_734 :: T_DistributiveLattice_598 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_734 T_DistributiveLattice_598
v0
  = let v1 :: Any
v1
          = (T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe
              T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0) in
    Any -> T_MeetSemilattice_204
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_MeetSemilattice_204) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_MeetSemilattice_204
MAlonzo.Code.Algebra.Lattice.Properties.Semilattice.du_'8743''45'orderTheoreticMeetSemilattice_180
         ((T_Lattice_512 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_330
            (Any -> Any
forall a b. a -> b
coe Any
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-semilattice
d_'8744''45'semilattice_736 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8744''45'semilattice_736 :: () -> () -> T_DistributiveLattice_598 -> T_Semilattice_10
d_'8744''45'semilattice_736 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_Semilattice_10
du_'8744''45'semilattice_736 T_DistributiveLattice_598
v2
du_'8744''45'semilattice_736 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8744''45'semilattice_736 :: T_DistributiveLattice_598 -> T_Semilattice_10
du_'8744''45'semilattice_736 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_Semilattice_10) -> Any -> T_Semilattice_10
forall a b. a -> b
coe
      T_Lattice_512 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_330
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-∧-isOrderTheoreticLattice
d_'8744''45''8743''45'isOrderTheoreticLattice_738 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsLattice_348
d_'8744''45''8743''45'isOrderTheoreticLattice_738 :: () -> () -> T_DistributiveLattice_598 -> T_IsLattice_348
d_'8744''45''8743''45'isOrderTheoreticLattice_738 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsLattice_348
du_'8744''45''8743''45'isOrderTheoreticLattice_738 T_DistributiveLattice_598
v2
du_'8744''45''8743''45'isOrderTheoreticLattice_738 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsLattice_348
du_'8744''45''8743''45'isOrderTheoreticLattice_738 :: T_DistributiveLattice_598 -> T_IsLattice_348
du_'8744''45''8743''45'isOrderTheoreticLattice_738 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_IsLattice_348) -> Any -> T_IsLattice_348
forall a b. a -> b
coe
      T_Lattice_512 -> T_IsLattice_348
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45''8743''45'isOrderTheoreticLattice_356
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-∧-orderTheoreticLattice
d_'8744''45''8743''45'orderTheoreticLattice_740 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_Lattice_394
d_'8744''45''8743''45'orderTheoreticLattice_740 :: () -> () -> T_DistributiveLattice_598 -> T_Lattice_394
d_'8744''45''8743''45'orderTheoreticLattice_740 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_Lattice_394
du_'8744''45''8743''45'orderTheoreticLattice_740 T_DistributiveLattice_598
v2
du_'8744''45''8743''45'orderTheoreticLattice_740 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_Lattice_394
du_'8744''45''8743''45'orderTheoreticLattice_740 :: T_DistributiveLattice_598 -> T_Lattice_394
du_'8744''45''8743''45'orderTheoreticLattice_740 T_DistributiveLattice_598
v0
  = (T_Lattice_512 -> T_Lattice_394) -> Any -> T_Lattice_394
forall a b. a -> b
coe
      T_Lattice_512 -> T_Lattice_394
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45''8743''45'orderTheoreticLattice_412
      ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
-- Algebra.Lattice.Properties.DistributiveLattice.∧-∨-isDistributiveLattice
d_'8743''45''8744''45'isDistributiveLattice_742 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146
d_'8743''45''8744''45'isDistributiveLattice_742 :: ()
-> () -> T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146
d_'8743''45''8744''45'isDistributiveLattice_742 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146
du_'8743''45''8744''45'isDistributiveLattice_742 T_DistributiveLattice_598
v2
du_'8743''45''8744''45'isDistributiveLattice_742 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146
du_'8743''45''8744''45'isDistributiveLattice_742 :: T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146
du_'8743''45''8744''45'isDistributiveLattice_742 T_DistributiveLattice_598
v0
  = (T_IsLattice_3070
 -> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3146)
-> Any -> Any -> Any -> T_IsDistributiveLattice_3146
forall a b. a -> b
coe
      T_IsLattice_3070
-> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3146
MAlonzo.Code.Algebra.Lattice.Structures.C_constructor_3212
      ((T_Lattice_512 -> T_IsLattice_3070) -> Any -> Any
forall a b. a -> b
coe
         T_Lattice_512 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45''8744''45'isLattice_342
         ((T_DistributiveLattice_598 -> T_Lattice_512) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_678 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0)))
      ((T_IsDistributiveLattice_3146 -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe
         T_IsDistributiveLattice_3146 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'distrib'45''8744'_3162
         ((T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146)
-> Any -> Any
forall a b. a -> b
coe
            T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146
MAlonzo.Code.Algebra.Lattice.Bundles.d_isDistributiveLattice_622
            (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0)))
      ((T_IsDistributiveLattice_3146 -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe
         T_IsDistributiveLattice_3146 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'distrib'45''8743'_3160
         ((T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146)
-> Any -> Any
forall a b. a -> b
coe
            T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146
MAlonzo.Code.Algebra.Lattice.Bundles.d_isDistributiveLattice_622
            (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0)))
-- Algebra.Lattice.Properties.DistributiveLattice.∧-∨-distributiveLattice
d_'8743''45''8744''45'distributiveLattice_744 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598
d_'8743''45''8744''45'distributiveLattice_744 :: () -> () -> T_DistributiveLattice_598 -> T_DistributiveLattice_598
d_'8743''45''8744''45'distributiveLattice_744 ~()
v0 ~()
v1 T_DistributiveLattice_598
v2
  = T_DistributiveLattice_598 -> T_DistributiveLattice_598
du_'8743''45''8744''45'distributiveLattice_744 T_DistributiveLattice_598
v2
du_'8743''45''8744''45'distributiveLattice_744 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598
du_'8743''45''8744''45'distributiveLattice_744 :: T_DistributiveLattice_598 -> T_DistributiveLattice_598
du_'8743''45''8744''45'distributiveLattice_744 T_DistributiveLattice_598
v0
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any)
 -> T_IsDistributiveLattice_3146
 -> T_DistributiveLattice_598)
-> (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> Any
-> T_DistributiveLattice_598
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_IsDistributiveLattice_3146
-> T_DistributiveLattice_598
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_692
      (T_DistributiveLattice_598 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__620 (T_DistributiveLattice_598 -> T_DistributiveLattice_598
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
      (T_DistributiveLattice_598 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__618 (T_DistributiveLattice_598 -> T_DistributiveLattice_598
forall a b. a -> b
coe T_DistributiveLattice_598
v0))
      ((T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146)
-> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_598 -> T_IsDistributiveLattice_3146
du_'8743''45''8744''45'isDistributiveLattice_742 (T_DistributiveLattice_598 -> Any
forall a b. a -> b
coe T_DistributiveLattice_598
v0))