{-# 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'__100 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__100 :: T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8851'__100 ~T_TotalPreorder_240
v0 T_MinOperator_106
v1 ~T_MaxOperator_138
v2 = T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__100 T_MinOperator_106
v1
du__'8851'__100 ::
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__100 :: T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8851'__100 T_MinOperator_106
v0
  = (T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__122
      (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsDistributiveLattice
d_IsDistributiveLattice_126 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d_IsDistributiveLattice_126 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice
d_IsLattice_132 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d_IsLattice_132 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_354 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
d_isLattice_354 :: T_IsDistributiveLattice_3146 -> T_IsLattice_3070
d_isLattice_354 T_IsDistributiveLattice_3146
v0
  = (T_IsDistributiveLattice_3146 -> T_IsLattice_3070)
-> AgdaAny -> T_IsLattice_3070
forall a b. a -> b
coe
      T_IsDistributiveLattice_3146 -> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Structures.d_isLattice_3158 (T_IsDistributiveLattice_3146 -> AgdaAny
forall a b. a -> b
coe T_IsDistributiveLattice_3146
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsDistributiveLattice.∧-distrib-∨
d_'8743''45'distrib'45''8744'_378 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'distrib'45''8744'_378 :: T_IsDistributiveLattice_3146 -> T_Σ_14
d_'8743''45'distrib'45''8744'_378 T_IsDistributiveLattice_3146
v0
  = (T_IsDistributiveLattice_3146 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsDistributiveLattice_3146 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'distrib'45''8744'_3162
      (T_IsDistributiveLattice_3146 -> AgdaAny
forall a b. a -> b
coe T_IsDistributiveLattice_3146
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsDistributiveLattice.∨-distrib-∧
d_'8744''45'distrib'45''8743'_396 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'distrib'45''8743'_396 :: T_IsDistributiveLattice_3146 -> T_Σ_14
d_'8744''45'distrib'45''8743'_396 T_IsDistributiveLattice_3146
v0
  = (T_IsDistributiveLattice_3146 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsDistributiveLattice_3146 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'distrib'45''8743'_3160
      (T_IsDistributiveLattice_3146 -> AgdaAny
forall a b. a -> b
coe T_IsDistributiveLattice_3146
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.absorptive
d_absorptive_438 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_absorptive_438 :: T_IsLattice_3070 -> T_Σ_14
d_absorptive_438 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsLattice_3070 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_3106 (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.isEquivalence
d_isEquivalence_440 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence_440 :: T_IsLattice_3070 -> T_IsEquivalence_28
d_isEquivalence_440 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
      T_IsLattice_3070 -> T_IsEquivalence_28
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_3092
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∧-assoc
d_'8743''45'assoc_454 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'assoc_454 :: T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'assoc_454 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_3102
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∧-comm
d_'8743''45'comm_456 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'comm_456 :: T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'comm_456 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_3100
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∧-cong
d_'8743''45'cong_458 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'cong_458 :: T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8743''45'cong_458 T_IsLattice_3070
v0
  = (T_IsLattice_3070
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_3104
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∨-assoc
d_'8744''45'assoc_466 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'assoc_466 :: T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'assoc_466 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_3096
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∨-comm
d_'8744''45'comm_468 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'comm_468 :: T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'comm_468 T_IsLattice_3070
v0
  = (T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_3094
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice.∨-cong
d_'8744''45'cong_470 ::
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'cong_470 :: T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8744''45'cong_470 T_IsLattice_3070
v0
  = (T_IsLattice_3070
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsLattice_3070
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_3098
      (T_IsLattice_3070 -> AgdaAny
forall a b. a -> b
coe T_IsLattice_3070
v0)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.⊓-isSemilattice
d_'8851''45'isSemilattice_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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
d_'8851''45'isSemilattice_798 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsCommutativeBand_612
d_'8851''45'isSemilattice_798 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4 ~T_MaxOperator_138
v5
  = T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsCommutativeBand_612
du_'8851''45'isSemilattice_798 T_TotalPreorder_240
v3 T_MinOperator_106
v4
du_'8851''45'isSemilattice_798 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
du_'8851''45'isSemilattice_798 :: T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsCommutativeBand_612
du_'8851''45'isSemilattice_798 T_TotalPreorder_240
v0 T_MinOperator_106
v1
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsCommutativeBand_612)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_612
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_616
      (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.⊓-semilattice
d_'8851''45'semilattice_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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8851''45'semilattice_800 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_Semilattice_10
d_'8851''45'semilattice_800 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4 ~T_MaxOperator_138
v5
  = T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semilattice_10
du_'8851''45'semilattice_800 T_TotalPreorder_240
v3 T_MinOperator_106
v4
du_'8851''45'semilattice_800 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8851''45'semilattice_800 :: T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semilattice_10
du_'8851''45'semilattice_800 T_TotalPreorder_240
v0 T_MinOperator_106
v1
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semilattice_10)
-> AgdaAny -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_618
      (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1)
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.⊓-isSemilattice
d_'8851''45'isSemilattice_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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
d_'8851''45'isSemilattice_804 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsCommutativeBand_612
d_'8851''45'isSemilattice_804 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 ~T_MinOperator_106
v4 T_MaxOperator_138
v5
  = T_TotalPreorder_240 -> T_MaxOperator_138 -> T_IsCommutativeBand_612
du_'8851''45'isSemilattice_804 T_TotalPreorder_240
v3 T_MaxOperator_138
v5
du_'8851''45'isSemilattice_804 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
du_'8851''45'isSemilattice_804 :: T_TotalPreorder_240 -> T_MaxOperator_138 -> T_IsCommutativeBand_612
du_'8851''45'isSemilattice_804 T_TotalPreorder_240
v0 T_MaxOperator_138
v1
  = (T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsCommutativeBand_612)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_612
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_616
      ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))
      ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
         (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v1))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.⊓-semilattice
d_'8851''45'semilattice_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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8851''45'semilattice_806 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_Semilattice_10
d_'8851''45'semilattice_806 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 ~T_MinOperator_106
v4 T_MaxOperator_138
v5
  = T_TotalPreorder_240 -> T_MaxOperator_138 -> T_Semilattice_10
du_'8851''45'semilattice_806 T_TotalPreorder_240
v3 T_MaxOperator_138
v5
du_'8851''45'semilattice_806 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8851''45'semilattice_806 :: T_TotalPreorder_240 -> T_MaxOperator_138 -> T_Semilattice_10
du_'8851''45'semilattice_806 T_TotalPreorder_240
v0 T_MaxOperator_138
v1
  = (T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semilattice_10)
-> AgdaAny -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_618
      ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))
      ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
         (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v1))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊔-⊓-isLattice
d_'8852''45''8851''45'isLattice_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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
d_'8852''45''8851''45'isLattice_808 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsLattice_3070
d_'8852''45''8851''45'isLattice_808 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
  = T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070
du_'8852''45''8851''45'isLattice_808 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
du_'8852''45''8851''45'isLattice_808 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
du_'8852''45''8851''45'isLattice_808 :: T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070
du_'8852''45''8851''45'isLattice_808 T_TotalPreorder_240
v0 T_MinOperator_106
v1 T_MaxOperator_138
v2
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsLattice_3070)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsLattice_3070
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Structures.C_constructor_3140
      ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
         ((T_IsTotalPreorder_132 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalPreorder_132 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_140
            ((T_TotalPreorder_240 -> T_IsTotalPreorder_132)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_IsTotalPreorder_132
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalPreorder_262
               (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2972
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2)))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_3060
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2)))
      ((T_TotalPreorder_240
 -> T_MinOperator_106
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_3046
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2)))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2972
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_3060
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_3046
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45''8851''45'absorptive_3338
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊓-⊔-isLattice
d_'8851''45''8852''45'isLattice_810 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
d_'8851''45''8852''45'isLattice_810 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsLattice_3070
d_'8851''45''8852''45'isLattice_810 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
  = T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070
du_'8851''45''8852''45'isLattice_810 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
du_'8851''45''8852''45'isLattice_810 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_3070
du_'8851''45''8852''45'isLattice_810 :: T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070
du_'8851''45''8852''45'isLattice_810 T_TotalPreorder_240
v0 T_MinOperator_106
v1 T_MaxOperator_138
v2
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsLattice_3070)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsLattice_3070
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsLattice_3070
MAlonzo.Code.Algebra.Lattice.Structures.C_constructor_3140
      ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
         ((T_IsTotalPreorder_132 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalPreorder_132 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_140
            ((T_TotalPreorder_240 -> T_IsTotalPreorder_132)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalPreorder_240 -> T_IsTotalPreorder_132
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalPreorder_262
               (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2972
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_3060
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_3046
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2972
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2)))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_3060
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2)))
      ((T_TotalPreorder_240
 -> T_MinOperator_106
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_3046
         ((T_TotalPreorder_240 -> T_TotalPreorder_240) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_TotalPreorder_240 -> T_TotalPreorder_240
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_760
            (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0))
         ((T_MaxOperator_138 -> T_MinOperator_106) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_MaxOperator_138 -> T_MinOperator_106
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_186
            (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2)))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45''8852''45'absorptive_3340
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊓-⊔-isDistributiveLattice
d_'8851''45''8852''45'isDistributiveLattice_812 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146
d_'8851''45''8852''45'isDistributiveLattice_812 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsDistributiveLattice_3146
d_'8851''45''8852''45'isDistributiveLattice_812 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4
                                                T_MaxOperator_138
v5
  = T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsDistributiveLattice_3146
du_'8851''45''8852''45'isDistributiveLattice_812 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
du_'8851''45''8852''45'isDistributiveLattice_812 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146
du_'8851''45''8852''45'isDistributiveLattice_812 :: T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsDistributiveLattice_3146
du_'8851''45''8852''45'isDistributiveLattice_812 T_TotalPreorder_240
v0 T_MinOperator_106
v1 T_MaxOperator_138
v2
  = (T_IsLattice_3070
 -> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3146)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDistributiveLattice_3146
forall a b. a -> b
coe
      T_IsLattice_3070
-> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3146
MAlonzo.Code.Algebra.Lattice.Structures.C_constructor_3212
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070
du_'8851''45''8852''45'isLattice_810 (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45'distrib'45''8852'_3260
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45'distrib'45''8851'_3292
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊔-⊓-isDistributiveLattice
d_'8852''45''8851''45'isDistributiveLattice_814 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146
d_'8852''45''8851''45'isDistributiveLattice_814 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsDistributiveLattice_3146
d_'8852''45''8851''45'isDistributiveLattice_814 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4
                                                T_MaxOperator_138
v5
  = T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsDistributiveLattice_3146
du_'8852''45''8851''45'isDistributiveLattice_814 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
du_'8852''45''8851''45'isDistributiveLattice_814 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3146
du_'8852''45''8851''45'isDistributiveLattice_814 :: T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsDistributiveLattice_3146
du_'8852''45''8851''45'isDistributiveLattice_814 T_TotalPreorder_240
v0 T_MinOperator_106
v1 T_MaxOperator_138
v2
  = (T_IsLattice_3070
 -> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3146)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDistributiveLattice_3146
forall a b. a -> b
coe
      T_IsLattice_3070
-> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3146
MAlonzo.Code.Algebra.Lattice.Structures.C_constructor_3212
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070
du_'8852''45''8851''45'isLattice_808 (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45'distrib'45''8851'_3292
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Σ_14
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45'distrib'45''8852'_3260
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊔-⊓-lattice
d_'8852''45''8851''45'lattice_816 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512
d_'8852''45''8851''45'lattice_816 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_Lattice_512
d_'8852''45''8851''45'lattice_816 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
  = T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Lattice_512
du_'8852''45''8851''45'lattice_816 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
du_'8852''45''8851''45'lattice_816 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512
du_'8852''45''8851''45'lattice_816 :: T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Lattice_512
du_'8852''45''8851''45'lattice_816 T_TotalPreorder_240
v0 T_MinOperator_106
v1 T_MaxOperator_138
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_3070
 -> T_Lattice_512)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_512
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070
-> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_592
      (T_MaxOperator_138 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__154
         (T_MaxOperator_138 -> T_MaxOperator_138
forall a b. a -> b
coe T_MaxOperator_138
v2))
      (T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__122
         (T_MinOperator_106 -> T_MinOperator_106
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070
du_'8852''45''8851''45'isLattice_808 (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊓-⊔-lattice
d_'8851''45''8852''45'lattice_818 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512
d_'8851''45''8852''45'lattice_818 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_Lattice_512
d_'8851''45''8852''45'lattice_818 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
  = T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Lattice_512
du_'8851''45''8852''45'lattice_818 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
du_'8851''45''8852''45'lattice_818 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_512
du_'8851''45''8852''45'lattice_818 :: T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_Lattice_512
du_'8851''45''8852''45'lattice_818 T_TotalPreorder_240
v0 T_MinOperator_106
v1 T_MaxOperator_138
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_3070
 -> T_Lattice_512)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_512
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_3070
-> T_Lattice_512
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_592
      (T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__122
         (T_MinOperator_106 -> T_MinOperator_106
forall a b. a -> b
coe T_MinOperator_106
v1))
      (T_MaxOperator_138 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__154
         (T_MaxOperator_138 -> T_MaxOperator_138
forall a b. a -> b
coe T_MaxOperator_138
v2))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> T_MaxOperator_138 -> T_IsLattice_3070
du_'8851''45''8852''45'isLattice_810 (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1) (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊔-⊓-distributiveLattice
d_'8852''45''8851''45'distributiveLattice_820 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598
d_'8852''45''8851''45'distributiveLattice_820 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_DistributiveLattice_598
d_'8852''45''8851''45'distributiveLattice_820 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
  = T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_DistributiveLattice_598
du_'8852''45''8851''45'distributiveLattice_820 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
du_'8852''45''8851''45'distributiveLattice_820 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598
du_'8852''45''8851''45'distributiveLattice_820 :: T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_DistributiveLattice_598
du_'8852''45''8851''45'distributiveLattice_820 T_TotalPreorder_240
v0 T_MinOperator_106
v1 T_MaxOperator_138
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsDistributiveLattice_3146
 -> T_DistributiveLattice_598)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_DistributiveLattice_598
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_3146
-> T_DistributiveLattice_598
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_692
      (T_MaxOperator_138 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__154
         (T_MaxOperator_138 -> T_MaxOperator_138
forall a b. a -> b
coe T_MaxOperator_138
v2))
      (T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__122
         (T_MinOperator_106 -> T_MinOperator_106
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106
 -> T_MaxOperator_138
 -> T_IsDistributiveLattice_3146)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsDistributiveLattice_3146
du_'8852''45''8851''45'isDistributiveLattice_814 (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1)
         (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))
-- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.⊓-⊔-distributiveLattice
d_'8851''45''8852''45'distributiveLattice_822 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598
d_'8851''45''8852''45'distributiveLattice_822 :: ()
-> ()
-> ()
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_DistributiveLattice_598
d_'8851''45''8852''45'distributiveLattice_822 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
  = T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_DistributiveLattice_598
du_'8851''45''8852''45'distributiveLattice_822 T_TotalPreorder_240
v3 T_MinOperator_106
v4 T_MaxOperator_138
v5
du_'8851''45''8852''45'distributiveLattice_822 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_138 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_598
du_'8851''45''8852''45'distributiveLattice_822 :: T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_DistributiveLattice_598
du_'8851''45''8852''45'distributiveLattice_822 T_TotalPreorder_240
v0 T_MinOperator_106
v1 T_MaxOperator_138
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsDistributiveLattice_3146
 -> T_DistributiveLattice_598)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_DistributiveLattice_598
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_3146
-> T_DistributiveLattice_598
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_692
      (T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__122
         (T_MinOperator_106 -> T_MinOperator_106
forall a b. a -> b
coe T_MinOperator_106
v1))
      (T_MaxOperator_138 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__154
         (T_MaxOperator_138 -> T_MaxOperator_138
forall a b. a -> b
coe T_MaxOperator_138
v2))
      ((T_TotalPreorder_240
 -> T_MinOperator_106
 -> T_MaxOperator_138
 -> T_IsDistributiveLattice_3146)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106
-> T_MaxOperator_138
-> T_IsDistributiveLattice_3146
du_'8851''45''8852''45'isDistributiveLattice_812 (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1)
         (T_MaxOperator_138 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_138
v2))