{-# 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.Construct.NaturalChoice.MinMaxOp 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.Construct.NaturalChoice.Base
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
import qualified MAlonzo.Code.Algebra.Lattice.Bundles
import qualified MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp
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.Construct.Flip.EqAndOrd
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._._⊓_
d__'8851'__92 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__92 :: T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8851'__92 ~T_TotalPreorder_222
v0 T_MinOperator_98
v1 ~T_MaxOperator_128
v2 = T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__92 T_MinOperator_98
v1
du__'8851'__92 ::
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__92 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__92 T_MinOperator_98
v0
  = (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
      (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsDistributiveLattice
d_IsDistributiveLattice_116 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d_IsDistributiveLattice_116 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice
d_IsLattice_120 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d_IsLattice_120 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsDistributiveLattice.isLattice
d_isLattice_340 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
d_isLattice_340 :: T_IsDistributiveLattice_3036 -> T_IsLattice_2962
d_isLattice_340 T_IsDistributiveLattice_3036
v0
  = (T_IsDistributiveLattice_3036 -> T_IsLattice_2962)
-> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsDistributiveLattice.∧-distrib-∨
d_'8743''45'distrib'45''8744'_364 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'distrib'45''8744'_364 :: T_IsDistributiveLattice_3036 -> T_Σ_14
d_'8743''45'distrib'45''8744'_364 T_IsDistributiveLattice_3036
v0
  = (T_IsDistributiveLattice_3036 -> T_Σ_14) -> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsDistributiveLattice.∨-distrib-∧
d_'8744''45'distrib'45''8743'_382 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'distrib'45''8743'_382 :: T_IsDistributiveLattice_3036 -> T_Σ_14
d_'8744''45'distrib'45''8743'_382 T_IsDistributiveLattice_3036
v0
  = (T_IsDistributiveLattice_3036 -> T_Σ_14) -> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.absorptive
d_absorptive_424 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_absorptive_424 :: T_IsLattice_2962 -> T_Σ_14
d_absorptive_424 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsLattice_2962 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_2998 (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.isEquivalence
d_isEquivalence_426 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_426 :: T_IsLattice_2962 -> T_IsEquivalence_26
d_isEquivalence_426 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∧-assoc
d_'8743''45'assoc_440 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'assoc_440 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'assoc_440 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_2994
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∧-comm
d_'8743''45'comm_442 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'comm_442 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'comm_442 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_2992
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∧-cong
d_'8743''45'cong_444 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'cong_444 :: T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8743''45'cong_444 T_IsLattice_2962
v0
  = (T_IsLattice_2962
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_2996
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∨-assoc
d_'8744''45'assoc_452 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'assoc_452 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'assoc_452 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_2988
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∨-comm
d_'8744''45'comm_454 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'comm_454 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'comm_454 T_IsLattice_2962
v0
  = (T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_2986
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∨-cong
d_'8744''45'cong_456 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'cong_456 :: T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8744''45'cong_456 T_IsLattice_2962
v0
  = (T_IsLattice_2962
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_2962
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_2990
      (T_IsLattice_2962 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_2962
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.⊓-isSemilattice
d_'8851''45'isSemilattice_784 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8851''45'isSemilattice_784 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsCommutativeBand_590
d_'8851''45'isSemilattice_784 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4 ~T_MaxOperator_128
v5
  = T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsCommutativeBand_590
du_'8851''45'isSemilattice_784 T_TotalPreorder_222
v3 T_MinOperator_98
v4
du_'8851''45'isSemilattice_784 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
du_'8851''45'isSemilattice_784 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsCommutativeBand_590
du_'8851''45'isSemilattice_784 T_TotalPreorder_222
v0 T_MinOperator_98
v1
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> T_IsCommutativeBand_590)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_590
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_602
      (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.⊓-semilattice
d_'8851''45'semilattice_786 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8851''45'semilattice_786 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_Semilattice_10
d_'8851''45'semilattice_786 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4 ~T_MaxOperator_128
v5
  = T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10
du_'8851''45'semilattice_786 T_TotalPreorder_222
v3 T_MinOperator_98
v4
du_'8851''45'semilattice_786 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8851''45'semilattice_786 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10
du_'8851''45'semilattice_786 T_TotalPreorder_222
v0 T_MinOperator_98
v1
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10)
-> AgdaAny -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_604
      (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.⊓-isSemilattice
d_'8851''45'isSemilattice_790 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8851''45'isSemilattice_790 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsCommutativeBand_590
d_'8851''45'isSemilattice_790 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 ~T_MinOperator_98
v4 T_MaxOperator_128
v5
  = T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsCommutativeBand_590
du_'8851''45'isSemilattice_790 T_TotalPreorder_222
v3 T_MaxOperator_128
v5
du_'8851''45'isSemilattice_790 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
du_'8851''45'isSemilattice_790 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsCommutativeBand_590
du_'8851''45'isSemilattice_790 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
  = (T_TotalPreorder_222
 -> T_MinOperator_98 -> T_IsCommutativeBand_590)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_590
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_602
      ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
      ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
         (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.⊓-semilattice
d_'8851''45'semilattice_792 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8851''45'semilattice_792 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_Semilattice_10
d_'8851''45'semilattice_792 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 ~T_MinOperator_98
v4 T_MaxOperator_128
v5
  = T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Semilattice_10
du_'8851''45'semilattice_792 T_TotalPreorder_222
v3 T_MaxOperator_128
v5
du_'8851''45'semilattice_792 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8851''45'semilattice_792 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Semilattice_10
du_'8851''45'semilattice_792 T_TotalPreorder_222
v0 T_MaxOperator_128
v1
  = (T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10)
-> AgdaAny -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_604
      ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
      ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
         (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v1))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊔-⊓-isLattice
d_'8852''45''8851''45'isLattice_794 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
d_'8852''45''8851''45'isLattice_794 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsLattice_2962
d_'8852''45''8851''45'isLattice_794 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
  = T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962
du_'8852''45''8851''45'isLattice_794 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
du_'8852''45''8851''45'isLattice_794 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
du_'8852''45''8851''45'isLattice_794 :: T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962
du_'8852''45''8851''45'isLattice_794 T_TotalPreorder_222
v0 T_MinOperator_98
v1 T_MaxOperator_128
v2
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsLattice_2962)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsLattice_2962
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Structures.C_IsLattice'46'constructor_36793
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
         ((T_IsTotalPreorder_124 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalPreorder_124 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
            ((T_TotalPreorder_222 -> T_IsTotalPreorder_124)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_IsTotalPreorder_124
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalPreorder_244
               (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
         ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
            (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
         ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
            (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2)))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
         ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
            (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
         ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
            (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2)))
      ((T_TotalPreorder_222
 -> T_MinOperator_98
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
         ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
            (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
         ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
            (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2)))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45''8851''45'absorptive_3216
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊓-⊔-isLattice
d_'8851''45''8852''45'isLattice_796 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
d_'8851''45''8852''45'isLattice_796 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsLattice_2962
d_'8851''45''8852''45'isLattice_796 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
  = T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962
du_'8851''45''8852''45'isLattice_796 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
du_'8851''45''8852''45'isLattice_796 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
du_'8851''45''8852''45'isLattice_796 :: T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962
du_'8851''45''8852''45'isLattice_796 T_TotalPreorder_222
v0 T_MinOperator_98
v1 T_MaxOperator_128
v2
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsLattice_2962)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsLattice_2962
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Structures.C_IsLattice'46'constructor_36793
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
         ((T_IsTotalPreorder_124 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalPreorder_124 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
            ((T_TotalPreorder_222 -> T_IsTotalPreorder_124)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_222 -> T_IsTotalPreorder_124
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalPreorder_244
               (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
         ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
            (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
         ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
            (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2)))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
         ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
            (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
         ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
            (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2)))
      ((T_TotalPreorder_222
 -> T_MinOperator_98
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
         ((T_TotalPreorder_222 -> T_TotalPreorder_222) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_222 -> T_TotalPreorder_222
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
            (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
         ((T_MaxOperator_128 -> T_MinOperator_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_128 -> T_MinOperator_98
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
            (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2)))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45''8852''45'absorptive_3218
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊓-⊔-isDistributiveLattice
d_'8851''45''8852''45'isDistributiveLattice_798 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
d_'8851''45''8852''45'isDistributiveLattice_798 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsDistributiveLattice_3036
d_'8851''45''8852''45'isDistributiveLattice_798 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4
                                                T_MaxOperator_128
v5
  = T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsDistributiveLattice_3036
du_'8851''45''8852''45'isDistributiveLattice_798 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
du_'8851''45''8852''45'isDistributiveLattice_798 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
du_'8851''45''8852''45'isDistributiveLattice_798 :: T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsDistributiveLattice_3036
du_'8851''45''8852''45'isDistributiveLattice_798 T_TotalPreorder_222
v0 T_MinOperator_98
v1 T_MaxOperator_128
v2
  = (T_IsLattice_2962
 -> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3036)
-> AgdaAny -> AgdaAny -> AgdaAny -> 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_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962
du_'8851''45''8852''45'isLattice_796 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45'distrib'45''8852'_3138
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45'distrib'45''8851'_3170
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊔-⊓-isDistributiveLattice
d_'8852''45''8851''45'isDistributiveLattice_800 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
d_'8852''45''8851''45'isDistributiveLattice_800 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsDistributiveLattice_3036
d_'8852''45''8851''45'isDistributiveLattice_800 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4
                                                T_MaxOperator_128
v5
  = T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsDistributiveLattice_3036
du_'8852''45''8851''45'isDistributiveLattice_800 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
du_'8852''45''8851''45'isDistributiveLattice_800 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
du_'8852''45''8851''45'isDistributiveLattice_800 :: T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsDistributiveLattice_3036
du_'8852''45''8851''45'isDistributiveLattice_800 T_TotalPreorder_222
v0 T_MinOperator_98
v1 T_MaxOperator_128
v2
  = (T_IsLattice_2962
 -> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3036)
-> AgdaAny -> AgdaAny -> AgdaAny -> 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_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962
du_'8852''45''8851''45'isLattice_794 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45'distrib'45''8851'_3170
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45'distrib'45''8852'_3138
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊔-⊓-lattice
d_'8852''45''8851''45'lattice_802 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
d_'8852''45''8851''45'lattice_802 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_Lattice_500
d_'8852''45''8851''45'lattice_802 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
  = T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Lattice_500
du_'8852''45''8851''45'lattice_802 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
du_'8852''45''8851''45'lattice_802 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
du_'8852''45''8851''45'lattice_802 :: T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Lattice_500
du_'8852''45''8851''45'lattice_802 T_TotalPreorder_222
v0 T_MinOperator_98
v1 T_MaxOperator_128
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_2962
 -> T_Lattice_500)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_500
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962
-> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.C_Lattice'46'constructor_7925
      (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__144
         (T_MaxOperator_128 -> T_MaxOperator_128
forall a b. a -> b
coe T_MaxOperator_128
v2))
      (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
         (T_MinOperator_98 -> T_MinOperator_98
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962
du_'8852''45''8851''45'isLattice_794 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊓-⊔-lattice
d_'8851''45''8852''45'lattice_804 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
d_'8851''45''8852''45'lattice_804 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_Lattice_500
d_'8851''45''8852''45'lattice_804 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
  = T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Lattice_500
du_'8851''45''8852''45'lattice_804 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
du_'8851''45''8852''45'lattice_804 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
du_'8851''45''8852''45'lattice_804 :: T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_Lattice_500
du_'8851''45''8852''45'lattice_804 T_TotalPreorder_222
v0 T_MinOperator_98
v1 T_MaxOperator_128
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_2962
 -> T_Lattice_500)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_500
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_2962
-> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.C_Lattice'46'constructor_7925
      (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
         (T_MinOperator_98 -> T_MinOperator_98
forall a b. a -> b
coe T_MinOperator_98
v1))
      (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__144
         (T_MaxOperator_128 -> T_MaxOperator_128
forall a b. a -> b
coe T_MaxOperator_128
v2))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962
du_'8851''45''8852''45'isLattice_796 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1) (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊔-⊓-distributiveLattice
d_'8852''45''8851''45'distributiveLattice_806 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584
d_'8852''45''8851''45'distributiveLattice_806 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_DistributiveLattice_584
d_'8852''45''8851''45'distributiveLattice_806 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
  = T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_DistributiveLattice_584
du_'8852''45''8851''45'distributiveLattice_806 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
du_'8852''45''8851''45'distributiveLattice_806 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584
du_'8852''45''8851''45'distributiveLattice_806 :: T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_DistributiveLattice_584
du_'8852''45''8851''45'distributiveLattice_806 T_TotalPreorder_222
v0 T_MinOperator_98
v1 T_MaxOperator_128
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsDistributiveLattice_3036
 -> T_DistributiveLattice_584)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_DistributiveLattice_584
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_3036
-> T_DistributiveLattice_584
MAlonzo.Code.Algebra.Lattice.Bundles.C_DistributiveLattice'46'constructor_9515
      (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__144
         (T_MaxOperator_128 -> T_MaxOperator_128
forall a b. a -> b
coe T_MaxOperator_128
v2))
      (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
         (T_MinOperator_98 -> T_MinOperator_98
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98
 -> T_MaxOperator_128
 -> T_IsDistributiveLattice_3036)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsDistributiveLattice_3036
du_'8852''45''8851''45'isDistributiveLattice_800 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1)
         (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊓-⊔-distributiveLattice
d_'8851''45''8852''45'distributiveLattice_808 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584
d_'8851''45''8852''45'distributiveLattice_808 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_DistributiveLattice_584
d_'8851''45''8852''45'distributiveLattice_808 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
  = T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_DistributiveLattice_584
du_'8851''45''8852''45'distributiveLattice_808 T_TotalPreorder_222
v3 T_MinOperator_98
v4 T_MaxOperator_128
v5
du_'8851''45''8852''45'distributiveLattice_808 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584
du_'8851''45''8852''45'distributiveLattice_808 :: T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_DistributiveLattice_584
du_'8851''45''8852''45'distributiveLattice_808 T_TotalPreorder_222
v0 T_MinOperator_98
v1 T_MaxOperator_128
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsDistributiveLattice_3036
 -> T_DistributiveLattice_584)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_DistributiveLattice_584
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_3036
-> T_DistributiveLattice_584
MAlonzo.Code.Algebra.Lattice.Bundles.C_DistributiveLattice'46'constructor_9515
      (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
         (T_MinOperator_98 -> T_MinOperator_98
forall a b. a -> b
coe T_MinOperator_98
v1))
      (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__144
         (T_MaxOperator_128 -> T_MaxOperator_128
forall a b. a -> b
coe T_MaxOperator_128
v2))
      ((T_TotalPreorder_222
 -> T_MinOperator_98
 -> T_MaxOperator_128
 -> T_IsDistributiveLattice_3036)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
-> T_IsDistributiveLattice_3036
du_'8851''45''8852''45'isDistributiveLattice_798 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1)
         (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v2))