content: {-# 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 ~v0 v1 ~v2 = du__'8851'__92 v1
  du__'8851'__92 ::
    MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
    AgdaAny -> AgdaAny -> AgdaAny
  du__'8851'__92 v0
    = coe
        MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
        (coe v0)
  -- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsDistributiveLattice
  d_IsDistributiveLattice_116 a0 a1 a2 a3 a4 a5 a6 a7 = ()
  -- Algebra.Lattice.Construct.NaturalChoice.MinMaxOp._.IsLattice
  d_IsLattice_120 a0 a1 a2 a3 a4 a5 a6 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_isLattice_3048 (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'distrib'45''8744'_3052
        (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'distrib'45''8743'_3050
        (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_2998 (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
        (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'assoc_2994
        (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'comm_2992
        (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'cong_2996
        (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'assoc_2988
        (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'comm_2986
        (coe 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 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'cong_2990
        (coe 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 ~v0 ~v1 ~v2 v3 v4 ~v5
    = du_'8851''45'isSemilattice_784 v3 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 v0 v1
    = coe
        MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_602
        (coe v0) (coe 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 ~v0 ~v1 ~v2 v3 v4 ~v5
    = du_'8851''45'semilattice_786 v3 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 v0 v1
    = coe
        MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_604
        (coe v0) (coe 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 ~v0 ~v1 ~v2 v3 ~v4 v5
    = du_'8851''45'isSemilattice_790 v3 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 v0 v1
    = coe
        MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_602
        (coe
           MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
           (coe v0))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
           (coe 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 ~v0 ~v1 ~v2 v3 ~v4 v5
    = du_'8851''45'semilattice_792 v3 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 v0 v1
    = coe
        MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_604
        (coe
           MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
           (coe v0))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
           (coe 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 ~v0 ~v1 ~v2 v3 v4 v5
    = du_'8852''45''8851''45'isLattice_794 v3 v4 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 v0 v1 v2
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.C_IsLattice'46'constructor_36793
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
              (coe
                 MAlonzo.Code.Relation.Binary.Bundles.d_isTotalPreorder_244
                 (coe v0))))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
           (coe
              MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
              (coe v0))
           (coe
              MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
              (coe v2)))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
           (coe
              MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
              (coe v0))
           (coe
              MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
              (coe v2)))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
           (coe
              MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
              (coe v0))
           (coe
              MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
              (coe v2)))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
           (coe v0) (coe v1))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
           (coe v0) (coe v1))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
           (coe v0) (coe v1))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45''8851''45'absorptive_3216
           (coe v0) (coe v1) (coe 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 ~v0 ~v1 ~v2 v3 v4 v5
    = du_'8851''45''8852''45'isLattice_796 v3 v4 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 v0 v1 v2
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.C_IsLattice'46'constructor_36793
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
              (coe
                 MAlonzo.Code.Relation.Binary.Bundles.d_isTotalPreorder_244
                 (coe v0))))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
           (coe v0) (coe v1))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
           (coe v0) (coe v1))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
           (coe v0) (coe v1))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
           (coe
              MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
              (coe v0))
           (coe
              MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
              (coe v2)))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'assoc_2944
           (coe
              MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
              (coe v0))
           (coe
              MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
              (coe v2)))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'cong_2930
           (coe
              MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
              (coe v0))
           (coe
              MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
              (coe v2)))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45''8852''45'absorptive_3218
           (coe v0) (coe v1) (coe 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 ~v0 ~v1 ~v2 v3 v4
                                                  v5
    = du_'8851''45''8852''45'isDistributiveLattice_798 v3 v4 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 v0 v1 v2
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.C_IsDistributiveLattice'46'constructor_40943
        (coe
           du_'8851''45''8852''45'isLattice_796 (coe v0) (coe v1) (coe v2))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45'distrib'45''8852'_3138
           (coe v0) (coe v1) (coe v2))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45'distrib'45''8851'_3170
           (coe v0) (coe v1) (coe 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 ~v0 ~v1 ~v2 v3 v4
                                                  v5
    = du_'8852''45''8851''45'isDistributiveLattice_800 v3 v4 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 v0 v1 v2
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.C_IsDistributiveLattice'46'constructor_40943
        (coe
           du_'8852''45''8851''45'isLattice_794 (coe v0) (coe v1) (coe v2))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8852''45'distrib'45''8851'_3170
           (coe v0) (coe v1) (coe v2))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.MinMaxOp.du_'8851''45'distrib'45''8852'_3138
           (coe v0) (coe v1) (coe 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 ~v0 ~v1 ~v2 v3 v4 v5
    = du_'8852''45''8851''45'lattice_802 v3 v4 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 v0 v1 v2
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_Lattice'46'constructor_7925
        (MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__144
           (coe v2))
        (MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
           (coe v1))
        (coe
           du_'8852''45''8851''45'isLattice_794 (coe v0) (coe v1) (coe 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 ~v0 ~v1 ~v2 v3 v4 v5
    = du_'8851''45''8852''45'lattice_804 v3 v4 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 v0 v1 v2
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_Lattice'46'constructor_7925
        (MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
           (coe v1))
        (MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__144
           (coe v2))
        (coe
           du_'8851''45''8852''45'isLattice_796 (coe v0) (coe v1) (coe 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 ~v0 ~v1 ~v2 v3 v4 v5
    = du_'8852''45''8851''45'distributiveLattice_806 v3 v4 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 v0 v1 v2
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_DistributiveLattice'46'constructor_9515
        (MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__144
           (coe v2))
        (MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
           (coe v1))
        (coe
           du_'8852''45''8851''45'isDistributiveLattice_800 (coe v0) (coe v1)
           (coe 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 ~v0 ~v1 ~v2 v3 v4 v5
    = du_'8851''45''8852''45'distributiveLattice_808 v3 v4 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 v0 v1 v2
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_DistributiveLattice'46'constructor_9515
        (MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
           (coe v1))
        (MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8852'__144
           (coe v2))
        (coe
           du_'8851''45''8852''45'isDistributiveLattice_798 (coe v0) (coe v1)
           (coe v2))
  