{-# 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_230 :: p -> p -> p -> p -> p -> ()
d_IsDistributiveLattice_230 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Algebra.Lattice.Properties.DistributiveLattice._.IsDistributiveLattice.isLattice
d_isLattice_454 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
d_isLattice_454 :: T_IsDistributiveLattice_3036 -> T_IsLattice_2962
d_isLattice_454 T_IsDistributiveLattice_3036
v0
  = (T_IsDistributiveLattice_3036 -> T_IsLattice_2962)
-> Any -> T_IsLattice_2962
forall a b. a -> b
coe
      T_IsDistributiveLattice_3036 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Structures.d_isLattice_3048 (T_IsDistributiveLattice_3036 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
-- Algebra.Lattice.Properties.DistributiveLattice._.IsDistributiveLattice.∧-distrib-∨
d_'8743''45'distrib'45''8744'_478 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'distrib'45''8744'_478 :: T_IsDistributiveLattice_3036 -> T_Σ_14
d_'8743''45'distrib'45''8744'_478 T_IsDistributiveLattice_3036
v0
  = (T_IsDistributiveLattice_3036 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
      T_IsDistributiveLattice_3036 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'distrib'45''8744'_3052
      (T_IsDistributiveLattice_3036 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
-- Algebra.Lattice.Properties.DistributiveLattice._.IsDistributiveLattice.∨-distrib-∧
d_'8744''45'distrib'45''8743'_496 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'distrib'45''8743'_496 :: T_IsDistributiveLattice_3036 -> T_Σ_14
d_'8744''45'distrib'45''8743'_496 T_IsDistributiveLattice_3036
v0
  = (T_IsDistributiveLattice_3036 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
      T_IsDistributiveLattice_3036 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'distrib'45''8743'_3050
      (T_IsDistributiveLattice_3036 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
-- Algebra.Lattice.Properties.DistributiveLattice._.poset
d_poset_686 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_poset_686 :: () -> () -> T_DistributiveLattice_584 -> T_Poset_314
d_poset_686 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2 = T_DistributiveLattice_584 -> T_Poset_314
du_poset_686 T_DistributiveLattice_584
v2
du_poset_686 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
du_poset_686 :: T_DistributiveLattice_584 -> T_Poset_314
du_poset_686 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0) in
    Any -> T_Poset_314
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_Poset_314) -> Any -> Any
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) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_3194
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-idem
d_'8743''45'idem_688 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  AgdaAny -> AgdaAny
d_'8743''45'idem_688 :: () -> () -> T_DistributiveLattice_584 -> Any -> Any
d_'8743''45'idem_688 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2 = T_DistributiveLattice_584 -> Any -> Any
du_'8743''45'idem_688 T_DistributiveLattice_584
v2
du_'8743''45'idem_688 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  AgdaAny -> AgdaAny
du_'8743''45'idem_688 :: T_DistributiveLattice_584 -> Any -> Any
du_'8743''45'idem_688 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
      T_Lattice_500 -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'idem_3182
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isBand
d_'8743''45'isBand_690 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8743''45'isBand_690 :: () -> () -> T_DistributiveLattice_584 -> T_IsBand_508
d_'8743''45'isBand_690 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2 = T_DistributiveLattice_584 -> T_IsBand_508
du_'8743''45'isBand_690 T_DistributiveLattice_584
v2
du_'8743''45'isBand_690 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
du_'8743''45'isBand_690 :: T_DistributiveLattice_584 -> T_IsBand_508
du_'8743''45'isBand_690 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsBand_508) -> Any -> T_IsBand_508
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsBand_508
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'isBand_3190
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isMagma
d_'8743''45'isMagma_692 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8743''45'isMagma_692 :: () -> () -> T_DistributiveLattice_584 -> T_IsMagma_176
d_'8743''45'isMagma_692 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2 = T_DistributiveLattice_584 -> T_IsMagma_176
du_'8743''45'isMagma_692 T_DistributiveLattice_584
v2
du_'8743''45'isMagma_692 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'8743''45'isMagma_692 :: T_DistributiveLattice_584 -> T_IsMagma_176
du_'8743''45'isMagma_692 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsMagma_176) -> Any -> T_IsMagma_176
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsMagma_176
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'isMagma_3186
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_694 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_694 :: () -> () -> T_DistributiveLattice_584 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_694 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_694 T_DistributiveLattice_584
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_694 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_694 :: T_DistributiveLattice_584 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_694 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
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_500 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_3194
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_696 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_696 :: () -> () -> T_DistributiveLattice_584 -> T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_696 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_696 T_DistributiveLattice_584
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_696 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_696 :: T_DistributiveLattice_584 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_696 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0) in
    Any -> T_IsMeetSemilattice_180
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_IsMeetSemilattice_180) -> Any -> Any
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) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_3194
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isSemigroup
d_'8743''45'isSemigroup_698 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8743''45'isSemigroup_698 :: () -> () -> T_DistributiveLattice_584 -> T_IsSemigroup_472
d_'8743''45'isSemigroup_698 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsSemigroup_472
du_'8743''45'isSemigroup_698 T_DistributiveLattice_584
v2
du_'8743''45'isSemigroup_698 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'8743''45'isSemigroup_698 :: T_DistributiveLattice_584 -> T_IsSemigroup_472
du_'8743''45'isSemigroup_698 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsSemigroup_472) -> Any -> T_IsSemigroup_472
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'isSemigroup_3188
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isSemilattice
d_'8743''45'isSemilattice_700 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8743''45'isSemilattice_700 :: () -> () -> T_DistributiveLattice_584 -> T_IsCommutativeBand_590
d_'8743''45'isSemilattice_700 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsCommutativeBand_590
du_'8743''45'isSemilattice_700 T_DistributiveLattice_584
v2
du_'8743''45'isSemilattice_700 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
du_'8743''45'isSemilattice_700 :: T_DistributiveLattice_584 -> T_IsCommutativeBand_590
du_'8743''45'isSemilattice_700 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsCommutativeBand_590)
-> Any -> T_IsCommutativeBand_590
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'isSemilattice_3192
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_702 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_702 :: () -> () -> T_DistributiveLattice_584 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_702 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_702 T_DistributiveLattice_584
v2
du_'8743''45'orderTheoreticJoinSemilattice_702 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_702 :: T_DistributiveLattice_584 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_702 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
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_500 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_3194
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_704 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_704 :: () -> () -> T_DistributiveLattice_584 -> T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_704 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_704 T_DistributiveLattice_584
v2
du_'8743''45'orderTheoreticMeetSemilattice_704 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_704 :: T_DistributiveLattice_584 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_704 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0) in
    Any -> T_MeetSemilattice_200
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_MeetSemilattice_200) -> Any -> Any
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) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_3194
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-semilattice
d_'8743''45'semilattice_706 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8743''45'semilattice_706 :: () -> () -> T_DistributiveLattice_584 -> T_Semilattice_10
d_'8743''45'semilattice_706 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_Semilattice_10
du_'8743''45'semilattice_706 T_DistributiveLattice_584
v2
du_'8743''45'semilattice_706 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8743''45'semilattice_706 :: T_DistributiveLattice_584 -> T_Semilattice_10
du_'8743''45'semilattice_706 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_Semilattice_10) -> Any -> T_Semilattice_10
forall a b. a -> b
coe
      T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45'semilattice_3194
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-∨-isLattice
d_'8743''45''8744''45'isLattice_708 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
d_'8743''45''8744''45'isLattice_708 :: () -> () -> T_DistributiveLattice_584 -> T_IsLattice_2962
d_'8743''45''8744''45'isLattice_708 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsLattice_2962
du_'8743''45''8744''45'isLattice_708 T_DistributiveLattice_584
v2
du_'8743''45''8744''45'isLattice_708 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
du_'8743''45''8744''45'isLattice_708 :: T_DistributiveLattice_584 -> T_IsLattice_2962
du_'8743''45''8744''45'isLattice_708 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsLattice_2962) -> Any -> T_IsLattice_2962
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45''8744''45'isLattice_3230
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-∨-lattice
d_'8743''45''8744''45'lattice_710 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
d_'8743''45''8744''45'lattice_710 :: () -> () -> T_DistributiveLattice_584 -> T_Lattice_500
d_'8743''45''8744''45'lattice_710 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_Lattice_500
du_'8743''45''8744''45'lattice_710 T_DistributiveLattice_584
v2
du_'8743''45''8744''45'lattice_710 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
du_'8743''45''8744''45'lattice_710 :: T_DistributiveLattice_584 -> T_Lattice_500
du_'8743''45''8744''45'lattice_710 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_Lattice_500) -> Any -> T_Lattice_500
forall a b. a -> b
coe
      T_Lattice_500 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45''8744''45'lattice_3232
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-idem
d_'8744''45'idem_712 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  AgdaAny -> AgdaAny
d_'8744''45'idem_712 :: () -> () -> T_DistributiveLattice_584 -> Any -> Any
d_'8744''45'idem_712 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2 = T_DistributiveLattice_584 -> Any -> Any
du_'8744''45'idem_712 T_DistributiveLattice_584
v2
du_'8744''45'idem_712 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  AgdaAny -> AgdaAny
du_'8744''45'idem_712 :: T_DistributiveLattice_584 -> Any -> Any
du_'8744''45'idem_712 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
      T_Lattice_500 -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'idem_3206
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-isBand
d_'8744''45'isBand_714 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8744''45'isBand_714 :: () -> () -> T_DistributiveLattice_584 -> T_IsBand_508
d_'8744''45'isBand_714 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2 = T_DistributiveLattice_584 -> T_IsBand_508
du_'8744''45'isBand_714 T_DistributiveLattice_584
v2
du_'8744''45'isBand_714 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_508
du_'8744''45'isBand_714 :: T_DistributiveLattice_584 -> T_IsBand_508
du_'8744''45'isBand_714 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsBand_508) -> Any -> T_IsBand_508
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsBand_508
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'isBand_3214
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-isMagma
d_'8744''45'isMagma_716 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8744''45'isMagma_716 :: () -> () -> T_DistributiveLattice_584 -> T_IsMagma_176
d_'8744''45'isMagma_716 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2 = T_DistributiveLattice_584 -> T_IsMagma_176
du_'8744''45'isMagma_716 T_DistributiveLattice_584
v2
du_'8744''45'isMagma_716 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'8744''45'isMagma_716 :: T_DistributiveLattice_584 -> T_IsMagma_176
du_'8744''45'isMagma_716 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsMagma_176) -> Any -> T_IsMagma_176
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsMagma_176
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'isMagma_3210
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_718 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_718 :: () -> () -> T_DistributiveLattice_584 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_718 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_718 T_DistributiveLattice_584
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_718 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_718 :: T_DistributiveLattice_584 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_718 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
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_500 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_3218
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_720 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_720 :: () -> () -> T_DistributiveLattice_584 -> T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_720 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_720 T_DistributiveLattice_584
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_720 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_720 :: T_DistributiveLattice_584 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_720 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0) in
    Any -> T_IsMeetSemilattice_180
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_IsMeetSemilattice_180) -> Any -> Any
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) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_3218
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-isSemigroup
d_'8744''45'isSemigroup_722 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8744''45'isSemigroup_722 :: () -> () -> T_DistributiveLattice_584 -> T_IsSemigroup_472
d_'8744''45'isSemigroup_722 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsSemigroup_472
du_'8744''45'isSemigroup_722 T_DistributiveLattice_584
v2
du_'8744''45'isSemigroup_722 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'8744''45'isSemigroup_722 :: T_DistributiveLattice_584 -> T_IsSemigroup_472
du_'8744''45'isSemigroup_722 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsSemigroup_472) -> Any -> T_IsSemigroup_472
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'isSemigroup_3212
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-isSemilattice
d_'8744''45'isSemilattice_724 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8744''45'isSemilattice_724 :: () -> () -> T_DistributiveLattice_584 -> T_IsCommutativeBand_590
d_'8744''45'isSemilattice_724 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsCommutativeBand_590
du_'8744''45'isSemilattice_724 T_DistributiveLattice_584
v2
du_'8744''45'isSemilattice_724 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
du_'8744''45'isSemilattice_724 :: T_DistributiveLattice_584 -> T_IsCommutativeBand_590
du_'8744''45'isSemilattice_724 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsCommutativeBand_590)
-> Any -> T_IsCommutativeBand_590
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'isSemilattice_3216
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_726 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_726 :: () -> () -> T_DistributiveLattice_584 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_726 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_726 T_DistributiveLattice_584
v2
du_'8743''45'orderTheoreticJoinSemilattice_726 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_726 :: T_DistributiveLattice_584 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_726 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
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_500 -> T_Semilattice_10) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_3218
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_728 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_728 :: () -> () -> T_DistributiveLattice_584 -> T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_728 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_728 T_DistributiveLattice_584
v2
du_'8743''45'orderTheoreticMeetSemilattice_728 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_728 :: T_DistributiveLattice_584 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_728 T_DistributiveLattice_584
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> t
forall a b. a -> b
coe
              T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0) in
    Any -> T_MeetSemilattice_200
forall a b. a -> b
coe
      ((T_Semilattice_10 -> T_MeetSemilattice_200) -> Any -> Any
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) -> Any -> Any
forall a b. a -> b
coe
            T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_3218
            (Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-semilattice
d_'8744''45'semilattice_730 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8744''45'semilattice_730 :: () -> () -> T_DistributiveLattice_584 -> T_Semilattice_10
d_'8744''45'semilattice_730 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_Semilattice_10
du_'8744''45'semilattice_730 T_DistributiveLattice_584
v2
du_'8744''45'semilattice_730 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8744''45'semilattice_730 :: T_DistributiveLattice_584 -> T_Semilattice_10
du_'8744''45'semilattice_730 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_Semilattice_10) -> Any -> T_Semilattice_10
forall a b. a -> b
coe
      T_Lattice_500 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45'semilattice_3218
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-∧-isOrderTheoreticLattice
d_'8744''45''8743''45'isOrderTheoreticLattice_732 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsLattice_340
d_'8744''45''8743''45'isOrderTheoreticLattice_732 :: () -> () -> T_DistributiveLattice_584 -> T_IsLattice_340
d_'8744''45''8743''45'isOrderTheoreticLattice_732 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsLattice_340
du_'8744''45''8743''45'isOrderTheoreticLattice_732 T_DistributiveLattice_584
v2
du_'8744''45''8743''45'isOrderTheoreticLattice_732 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsLattice_340
du_'8744''45''8743''45'isOrderTheoreticLattice_732 :: T_DistributiveLattice_584 -> T_IsLattice_340
du_'8744''45''8743''45'isOrderTheoreticLattice_732 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_IsLattice_340) -> Any -> T_IsLattice_340
forall a b. a -> b
coe
      T_Lattice_500 -> T_IsLattice_340
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45''8743''45'isOrderTheoreticLattice_3244
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice._.∨-∧-orderTheoreticLattice
d_'8744''45''8743''45'orderTheoreticLattice_734 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_Lattice_386
d_'8744''45''8743''45'orderTheoreticLattice_734 :: () -> () -> T_DistributiveLattice_584 -> T_Lattice_386
d_'8744''45''8743''45'orderTheoreticLattice_734 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_Lattice_386
du_'8744''45''8743''45'orderTheoreticLattice_734 T_DistributiveLattice_584
v2
du_'8744''45''8743''45'orderTheoreticLattice_734 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_Lattice_386
du_'8744''45''8743''45'orderTheoreticLattice_734 :: T_DistributiveLattice_584 -> T_Lattice_386
du_'8744''45''8743''45'orderTheoreticLattice_734 T_DistributiveLattice_584
v0
  = (T_Lattice_500 -> T_Lattice_386) -> Any -> T_Lattice_386
forall a b. a -> b
coe
      T_Lattice_500 -> T_Lattice_386
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8744''45''8743''45'orderTheoreticLattice_3300
      ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
-- Algebra.Lattice.Properties.DistributiveLattice.∧-∨-isDistributiveLattice
d_'8743''45''8744''45'isDistributiveLattice_736 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
d_'8743''45''8744''45'isDistributiveLattice_736 :: ()
-> () -> T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036
d_'8743''45''8744''45'isDistributiveLattice_736 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036
du_'8743''45''8744''45'isDistributiveLattice_736 T_DistributiveLattice_584
v2
du_'8743''45''8744''45'isDistributiveLattice_736 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
du_'8743''45''8744''45'isDistributiveLattice_736 :: T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036
du_'8743''45''8744''45'isDistributiveLattice_736 T_DistributiveLattice_584
v0
  = (T_IsLattice_2962
 -> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3036)
-> Any -> Any -> Any -> T_IsDistributiveLattice_3036
forall a b. a -> b
coe
      T_IsLattice_2962
-> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3036
MAlonzo.Code.Algebra.Lattice.Structures.C_IsDistributiveLattice'46'constructor_40943
      ((T_Lattice_500 -> T_IsLattice_2962) -> Any -> Any
forall a b. a -> b
coe
         T_Lattice_500 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Properties.Lattice.du_'8743''45''8744''45'isLattice_3230
         ((T_DistributiveLattice_584 -> T_Lattice_500) -> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.du_lattice_664 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0)))
      ((T_IsDistributiveLattice_3036 -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe
         T_IsDistributiveLattice_3036 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'distrib'45''8744'_3052
         ((T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036)
-> Any -> Any
forall a b. a -> b
coe
            T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036
MAlonzo.Code.Algebra.Lattice.Bundles.d_isDistributiveLattice_608
            (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0)))
      ((T_IsDistributiveLattice_3036 -> T_Σ_14) -> Any -> Any
forall a b. a -> b
coe
         T_IsDistributiveLattice_3036 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'distrib'45''8743'_3050
         ((T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036)
-> Any -> Any
forall a b. a -> b
coe
            T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036
MAlonzo.Code.Algebra.Lattice.Bundles.d_isDistributiveLattice_608
            (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0)))
-- Algebra.Lattice.Properties.DistributiveLattice.∧-∨-distributiveLattice
d_'8743''45''8744''45'distributiveLattice_738 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584
d_'8743''45''8744''45'distributiveLattice_738 :: () -> () -> T_DistributiveLattice_584 -> T_DistributiveLattice_584
d_'8743''45''8744''45'distributiveLattice_738 ~()
v0 ~()
v1 T_DistributiveLattice_584
v2
  = T_DistributiveLattice_584 -> T_DistributiveLattice_584
du_'8743''45''8744''45'distributiveLattice_738 T_DistributiveLattice_584
v2
du_'8743''45''8744''45'distributiveLattice_738 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584
du_'8743''45''8744''45'distributiveLattice_738 :: T_DistributiveLattice_584 -> T_DistributiveLattice_584
du_'8743''45''8744''45'distributiveLattice_738 T_DistributiveLattice_584
v0
  = ((Any -> Any -> Any)
 -> (Any -> Any -> Any)
 -> T_IsDistributiveLattice_3036
 -> T_DistributiveLattice_584)
-> (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> Any
-> T_DistributiveLattice_584
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_IsDistributiveLattice_3036
-> T_DistributiveLattice_584
MAlonzo.Code.Algebra.Lattice.Bundles.C_DistributiveLattice'46'constructor_9515
      (T_DistributiveLattice_584 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8743'__606 (T_DistributiveLattice_584 -> T_DistributiveLattice_584
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
      (T_DistributiveLattice_584 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8744'__604 (T_DistributiveLattice_584 -> T_DistributiveLattice_584
forall a b. a -> b
coe T_DistributiveLattice_584
v0))
      ((T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036)
-> Any -> Any
forall a b. a -> b
coe T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036
du_'8743''45''8744''45'isDistributiveLattice_736 (T_DistributiveLattice_584 -> Any
forall a b. a -> b
coe T_DistributiveLattice_584
v0))