{-# 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 Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Algebra.Construct.NaturalChoice.Base qualified
import MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp qualified
import MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp qualified
import MAlonzo.Code.Algebra.Lattice.Bundles qualified
import MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp qualified
import MAlonzo.Code.Algebra.Lattice.Structures qualified
import MAlonzo.Code.Algebra.Structures qualified
import MAlonzo.Code.Relation.Binary.Bundles qualified
import MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd qualified
import MAlonzo.Code.Relation.Binary.Structures qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- 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))