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.Structures where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Algebra.Structures qualified
  import MAlonzo.Code.Relation.Binary.Bundles 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.Structures._._Absorbs_
  d__Absorbs__16 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d__Absorbs__16 = erased
  -- Algebra.Lattice.Structures._._DistributesOver_
  d__DistributesOver__18 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d__DistributesOver__18 = erased
  -- Algebra.Lattice.Structures._._DistributesOverʳ_
  d__DistributesOver'691'__20 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d__DistributesOver'691'__20 = erased
  -- Algebra.Lattice.Structures._._DistributesOverˡ_
  d__DistributesOver'737'__22 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d__DistributesOver'737'__22 = erased
  -- Algebra.Lattice.Structures._.Absorptive
  d_Absorptive_28 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Absorptive_28 = erased
  -- Algebra.Lattice.Structures._.Associative
  d_Associative_38 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Associative_38 = erased
  -- Algebra.Lattice.Structures._.Commutative
  d_Commutative_42 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Commutative_42 = erased
  -- Algebra.Lattice.Structures._.Congruent₁
  d_Congruent'8321'_44 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> ()
  d_Congruent'8321'_44 = erased
  -- Algebra.Lattice.Structures._.Congruent₂
  d_Congruent'8322'_46 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Congruent'8322'_46 = erased
  -- Algebra.Lattice.Structures._.Inverse
  d_Inverse_62 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Inverse_62 = erased
  -- Algebra.Lattice.Structures._.LeftCongruent
  d_LeftCongruent_74 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_LeftCongruent_74 = erased
  -- Algebra.Lattice.Structures._.LeftInverse
  d_LeftInverse_86 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_LeftInverse_86 = erased
  -- Algebra.Lattice.Structures._.RightCongruent
  d_RightCongruent_104 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_RightCongruent_104 = erased
  -- Algebra.Lattice.Structures._.RightInverse
  d_RightInverse_116 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_RightInverse_116 = erased
  -- Algebra.Lattice.Structures._.IsCommutativeBand
  d_IsCommutativeBand_154 a0 a1 a2 a3 a4 = ()
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid
  d_IsIdempotentCommutativeMonoid_172 a0 a1 a2 a3 a4 a5 = ()
  -- Algebra.Lattice.Structures._.IsBand.isPartialEquivalence
  d_isPartialEquivalence_338 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_338 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_isPartialEquivalence_338 v5
  du_isPartialEquivalence_338 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_338 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v2))))
  -- Algebra.Lattice.Structures._.IsBand.reflexive
  d_reflexive_344 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_344 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_reflexive_344 v5
  du_reflexive_344 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_344 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v1) in
         coe
           (\ v3 v4 v5 ->
              coe
                MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                (coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v2))
                v3))
  -- Algebra.Lattice.Structures._.IsBand.setoid
  d_setoid_346 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_346 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_setoid_346 v5
  du_setoid_346 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_346 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_setoid_200
           (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v1)))
  -- Algebra.Lattice.Structures._.IsBand.∙-congʳ
  d_'8729''45'cong'691'_354 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'691'_354 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong'691'_354 v5
  du_'8729''45'cong'691'_354 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'691'_354 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
           (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v1)))
  -- Algebra.Lattice.Structures._.IsBand.∙-congˡ
  d_'8729''45'cong'737'_356 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'737'_356 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong'737'_356 v5
  du_'8729''45'cong'737'_356 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'737'_356 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
           (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v1)))
  -- Algebra.Lattice.Structures._.IsCommutativeBand.comm
  d_comm_464 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny
  d_comm_464 v0
    = coe MAlonzo.Code.Algebra.Structures.d_comm_600 (coe v0)
  -- Algebra.Lattice.Structures._.IsCommutativeBand.isBand
  d_isBand_468 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_isBand_468 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.idem
  d_idem_976 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_idem_976 v0
    = coe MAlonzo.Code.Algebra.Structures.d_idem_864 (coe v0)
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.identityʳ
  d_identity'691'_980 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_identity'691'_980 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_identity'691'_980 v6
  du_identity'691'_980 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_identity'691'_980 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_identity'691'_728
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.identityˡ
  d_identity'737'_982 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_identity'737'_982 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_identity'737'_982 v6
  du_identity'737'_982 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_identity'737'_982 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_identity'737'_726
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.isBand
  d_isBand_984 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_isBand_984 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_isBand_984 v6
  du_isBand_984 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  du_isBand_984 v0
    = coe
        MAlonzo.Code.Algebra.Structures.du_isBand_846
        (coe
           MAlonzo.Code.Algebra.Structures.du_isIdempotentMonoid_910 (coe v0))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.isCommutativeBand
  d_isCommutativeBand_986 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  d_isCommutativeBand_986 ~v0 ~v1 ~v2 ~v3 = du_isCommutativeBand_986
  du_isCommutativeBand_986 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  du_isCommutativeBand_986 v0 v1 v2
    = coe MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916 v2
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.isCommutativeMagma
  d_isCommutativeMagma_988 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMagma_212
  d_isCommutativeMagma_988 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isCommutativeMagma_988 v6
  du_isCommutativeMagma_988 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMagma_212
  du_isCommutativeMagma_988 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_isCommutativeMagma_586
           (coe
              MAlonzo.Code.Algebra.Structures.du_isCommutativeSemigroup_786
              (coe v1)))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.isCommutativeMonoid
  d_isCommutativeMonoid_990 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
  d_isCommutativeMonoid_990 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862 (coe v0)
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.isCommutativeSemigroup
  d_isCommutativeSemigroup_992 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
  d_isCommutativeSemigroup_992 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isCommutativeSemigroup_992 v6
  du_isCommutativeSemigroup_992 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
  du_isCommutativeSemigroup_992 v0
    = coe
        MAlonzo.Code.Algebra.Structures.du_isCommutativeSemigroup_786
        (coe
           MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862 (coe v0))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.isIdempotentMonoid
  d_isIdempotentMonoid_996 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentMonoid_796
  d_isIdempotentMonoid_996 ~v0 ~v1 ~v2 ~v3
    = du_isIdempotentMonoid_996
  du_isIdempotentMonoid_996 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentMonoid_796
  du_isIdempotentMonoid_996 v0 v1 v2
    = coe MAlonzo.Code.Algebra.Structures.du_isIdempotentMonoid_910 v2
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.isPartialEquivalence
  d_isPartialEquivalence_1002 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_1002 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isPartialEquivalence_1002 v6
  du_isPartialEquivalence_1002 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_1002 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (let v4 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3) in
               coe
                 (coe
                    MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
                    (coe
                       MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v4))))))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.isUnitalMagma
  d_isUnitalMagma_1006 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsUnitalMagma_642
  d_isUnitalMagma_1006 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isUnitalMagma_1006 v6
  du_isUnitalMagma_1006 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsUnitalMagma_642
  du_isUnitalMagma_1006 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_isUnitalMagma_730
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.reflexive
  d_reflexive_1010 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_1010 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_reflexive_1010 v6
  du_reflexive_1010 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_1010 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (let v4 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3) in
               coe
                 (\ v5 v6 v7 ->
                    coe
                      MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                      (coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v4))
                      v5))))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.setoid
  d_setoid_1012 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_1012 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_setoid_1012 v6
  du_setoid_1012 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_1012 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_setoid_200
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.∙-congʳ
  d_'8729''45'cong'691'_1020 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'691'_1020 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong'691'_1020 v6
  du_'8729''45'cong'691'_1020 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'691'_1020 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures._.IsIdempotentCommutativeMonoid.∙-congˡ
  d_'8729''45'cong'737'_1022 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'737'_1022 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong'737'_1022 v6
  du_'8729''45'cong'737'_1022 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'737'_1022 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsSemilattice
  d_IsSemilattice_2658 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_IsSemilattice_2658 = erased
  -- Algebra.Lattice.Structures.IsSemilattice._.comm
  d_comm_2668 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny
  d_comm_2668 v0
    = coe MAlonzo.Code.Algebra.Structures.d_comm_600 (coe v0)
  -- Algebra.Lattice.Structures.IsSemilattice._.isBand
  d_isBand_2670 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_isBand_2670 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)
  -- Algebra.Lattice.Structures.IsSemilattice._.assoc
  d_assoc_2674 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_assoc_2674 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_assoc_2674 v5
  du_assoc_2674 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_assoc_2674 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_assoc_482
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))
  -- Algebra.Lattice.Structures.IsSemilattice._.idem
  d_idem_2676 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  d_idem_2676 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_idem_2676 v5
  du_idem_2676 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  du_idem_2676 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_idem_518
        (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))
  -- Algebra.Lattice.Structures.IsSemilattice._.isEquivalence
  d_isEquivalence_2678 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_2678 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_isEquivalence_2678 v5
  du_isEquivalence_2678 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  du_isEquivalence_2678 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))))
  -- Algebra.Lattice.Structures.IsSemilattice._.isMagma
  d_isMagma_2680 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2680 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_isMagma_2680 v5
  du_isMagma_2680 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  du_isMagma_2680 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isMagma_480
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))
  -- Algebra.Lattice.Structures.IsSemilattice._.isPartialEquivalence
  d_isPartialEquivalence_2682 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_2682 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_isPartialEquivalence_2682 v5
  du_isPartialEquivalence_2682 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_2682 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (let v3 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v3)))))
  -- Algebra.Lattice.Structures.IsSemilattice._.isSemigroup
  d_isSemigroup_2684 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_2684 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_isSemigroup_2684 v5
  du_isSemigroup_2684 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  du_isSemigroup_2684 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
        (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))
  -- Algebra.Lattice.Structures.IsSemilattice._.refl
  d_refl_2686 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  d_refl_2686 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_refl_2686 v5
  du_refl_2686 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  du_refl_2686 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_refl_34
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsSemilattice._.reflexive
  d_reflexive_2688 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_2688 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_reflexive_2688 v5
  du_reflexive_2688 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_2688 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (let v3 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2) in
            coe
              (\ v4 v5 v6 ->
                 coe
                   MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                   (coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v3))
                   v4)))
  -- Algebra.Lattice.Structures.IsSemilattice._.setoid
  d_setoid_2690 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_2690 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_setoid_2690 v5
  du_setoid_2690 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_2690 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_setoid_200
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsSemilattice._.sym
  d_sym_2692 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_2692 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_sym_2692 v5
  du_sym_2692 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_sym_2692 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_sym_36
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsSemilattice._.trans
  d_trans_2694 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_2694 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_trans_2694 v5
  du_trans_2694 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_trans_2694 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsSemilattice._.∙-cong
  d_'8729''45'cong_2696 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong_2696 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong_2696 v5
  du_'8729''45'cong_2696 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong_2696 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))))
  -- Algebra.Lattice.Structures.IsSemilattice._.∙-congʳ
  d_'8729''45'cong'691'_2698 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'691'_2698 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong'691'_2698 v5
  du_'8729''45'cong'691'_2698 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'691'_2698 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsSemilattice._.∙-congˡ
  d_'8729''45'cong'737'_2700 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'737'_2700 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong'737'_2700 v5
  du_'8729''45'cong'737'_2700 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'737'_2700 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice
  d_IsMeetSemilattice_2702 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_IsMeetSemilattice_2702 = erased
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.assoc
  d_assoc_2712 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_assoc_2712 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_assoc_2712 v5
  du_assoc_2712 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_assoc_2712 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_assoc_482
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.comm
  d_comm_2714 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny
  d_comm_2714 v0
    = coe MAlonzo.Code.Algebra.Structures.d_comm_600 (coe v0)
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.idem
  d_idem_2716 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  d_idem_2716 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_idem_2716 v5
  du_idem_2716 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  du_idem_2716 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_idem_518
        (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.isBand
  d_isBand_2718 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_isBand_2718 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.isEquivalence
  d_isEquivalence_2720 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_2720 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_isEquivalence_2720 v5
  du_isEquivalence_2720 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  du_isEquivalence_2720 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.isMagma
  d_isMagma_2722 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2722 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_isMagma_2722 v5
  du_isMagma_2722 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  du_isMagma_2722 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isMagma_480
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.isPartialEquivalence
  d_isPartialEquivalence_2724 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_2724 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_isPartialEquivalence_2724 v5
  du_isPartialEquivalence_2724 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_2724 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (let v3 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v3)))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.isSemigroup
  d_isSemigroup_2726 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_2726 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_isSemigroup_2726 v5
  du_isSemigroup_2726 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  du_isSemigroup_2726 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
        (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.refl
  d_refl_2728 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  d_refl_2728 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_refl_2728 v5
  du_refl_2728 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  du_refl_2728 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_refl_34
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.reflexive
  d_reflexive_2730 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_2730 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_reflexive_2730 v5
  du_reflexive_2730 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_2730 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (let v3 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2) in
            coe
              (\ v4 v5 v6 ->
                 coe
                   MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                   (coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v3))
                   v4)))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.setoid
  d_setoid_2732 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_2732 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_setoid_2732 v5
  du_setoid_2732 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_2732 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_setoid_200
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.sym
  d_sym_2734 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_2734 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_sym_2734 v5
  du_sym_2734 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_sym_2734 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_sym_36
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.trans
  d_trans_2736 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_2736 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_trans_2736 v5
  du_trans_2736 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_trans_2736 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.∙-cong
  d_'8729''45'cong_2738 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong_2738 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong_2738 v5
  du_'8729''45'cong_2738 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong_2738 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.∙-congʳ
  d_'8729''45'cong'691'_2740 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'691'_2740 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong'691'_2740 v5
  du_'8729''45'cong'691'_2740 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'691'_2740 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsMeetSemilattice._.∙-congˡ
  d_'8729''45'cong'737'_2742 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'737'_2742 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong'737'_2742 v5
  du_'8729''45'cong'737'_2742 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'737'_2742 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice
  d_IsJoinSemilattice_2744 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_IsJoinSemilattice_2744 = erased
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.assoc
  d_assoc_2754 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_assoc_2754 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_assoc_2754 v5
  du_assoc_2754 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_assoc_2754 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_assoc_482
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.comm
  d_comm_2756 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny
  d_comm_2756 v0
    = coe MAlonzo.Code.Algebra.Structures.d_comm_600 (coe v0)
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.idem
  d_idem_2758 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  d_idem_2758 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_idem_2758 v5
  du_idem_2758 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  du_idem_2758 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_idem_518
        (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.isBand
  d_isBand_2760 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_isBand_2760 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.isEquivalence
  d_isEquivalence_2762 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_2762 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_isEquivalence_2762 v5
  du_isEquivalence_2762 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  du_isEquivalence_2762 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.isMagma
  d_isMagma_2764 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2764 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_isMagma_2764 v5
  du_isMagma_2764 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  du_isMagma_2764 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isMagma_480
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.isPartialEquivalence
  d_isPartialEquivalence_2766 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_2766 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_isPartialEquivalence_2766 v5
  du_isPartialEquivalence_2766 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_2766 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (let v3 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v3)))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.isSemigroup
  d_isSemigroup_2768 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_2768 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_isSemigroup_2768 v5
  du_isSemigroup_2768 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  du_isSemigroup_2768 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
        (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.refl
  d_refl_2770 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  d_refl_2770 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_refl_2770 v5
  du_refl_2770 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny
  du_refl_2770 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_refl_34
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.reflexive
  d_reflexive_2772 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_2772 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_reflexive_2772 v5
  du_reflexive_2772 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_2772 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (let v3 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2) in
            coe
              (\ v4 v5 v6 ->
                 coe
                   MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                   (coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v3))
                   v4)))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.setoid
  d_setoid_2774 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_2774 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_setoid_2774 v5
  du_setoid_2774 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_2774 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_setoid_200
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.sym
  d_sym_2776 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_2776 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_sym_2776 v5
  du_sym_2776 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_sym_2776 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_sym_36
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.trans
  d_trans_2778 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_2778 ~v0 ~v1 ~v2 ~v3 ~v4 v5 = du_trans_2778 v5
  du_trans_2778 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_trans_2778 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0)))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.∙-cong
  d_'8729''45'cong_2780 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong_2780 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong_2780 v5
  du_'8729''45'cong_2780 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong_2780 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.∙-congʳ
  d_'8729''45'cong'691'_2782 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'691'_2782 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong'691'_2782 v5
  du_'8729''45'cong'691'_2782 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'691'_2782 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsJoinSemilattice._.∙-congˡ
  d_'8729''45'cong'737'_2784 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'737'_2784 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_'8729''45'cong'737'_2784 v5
  du_'8729''45'cong'737'_2784 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'737'_2784 v0
    = let v1 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
              (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v2))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice
  d_IsBoundedSemilattice_2786 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> ()
  d_IsBoundedSemilattice_2786 = erased
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.assoc
  d_assoc_2798 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_assoc_2798 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_assoc_482
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMonoid_746
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                 (coe v0))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.comm
  d_comm_2800 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny
  d_comm_2800 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_comm_748
        (coe
           MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862 (coe v0))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.idem
  d_idem_2802 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_idem_2802 v0
    = coe MAlonzo.Code.Algebra.Structures.d_idem_864 (coe v0)
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.identity
  d_identity_2804 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_identity_2804 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_identity_698
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMonoid_746
           (coe
              MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
              (coe v0)))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.identityʳ
  d_identity'691'_2806 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_identity'691'_2806 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_identity'691'_2806 v6
  du_identity'691'_2806 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_identity'691'_2806 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_identity'691'_728
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.identityˡ
  d_identity'737'_2808 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_identity'737'_2808 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_identity'737'_2808 v6
  du_identity'737'_2808 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_identity'737'_2808 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_identity'737'_726
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isBand
  d_isBand_2810 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_isBand_2810 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_isBand_2810 v6
  du_isBand_2810 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  du_isBand_2810 v0
    = coe
        MAlonzo.Code.Algebra.Structures.du_isBand_846
        (coe
           MAlonzo.Code.Algebra.Structures.du_isIdempotentMonoid_910 (coe v0))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isCommutativeMagma
  d_isCommutativeMagma_2812 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMagma_212
  d_isCommutativeMagma_2812 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isCommutativeMagma_2812 v6
  du_isCommutativeMagma_2812 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMagma_212
  du_isCommutativeMagma_2812 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_isCommutativeMagma_586
           (coe
              MAlonzo.Code.Algebra.Structures.du_isCommutativeSemigroup_786
              (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isCommutativeMonoid
  d_isCommutativeMonoid_2814 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
  d_isCommutativeMonoid_2814 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862 (coe v0)
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isCommutativeSemigroup
  d_isCommutativeSemigroup_2816 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
  d_isCommutativeSemigroup_2816 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isCommutativeSemigroup_2816 v6
  du_isCommutativeSemigroup_2816 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
  du_isCommutativeSemigroup_2816 v0
    = coe
        MAlonzo.Code.Algebra.Structures.du_isCommutativeSemigroup_786
        (coe
           MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862 (coe v0))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isEquivalence
  d_isEquivalence_2818 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_2818 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isMonoid_746
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                    (coe v0)))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isIdempotentMonoid
  d_isIdempotentMonoid_2820 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentMonoid_796
  d_isIdempotentMonoid_2820 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isIdempotentMonoid_2820 v6
  du_isIdempotentMonoid_2820 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentMonoid_796
  du_isIdempotentMonoid_2820 v0
    = coe
        MAlonzo.Code.Algebra.Structures.du_isIdempotentMonoid_910 (coe v0)
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isMagma
  d_isMagma_2822 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2822 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isMagma_480
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMonoid_746
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                 (coe v0))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isMonoid
  d_isMonoid_2824 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  d_isMonoid_2824 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isMonoid_746
        (coe
           MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862 (coe v0))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isPartialEquivalence
  d_isPartialEquivalence_2826 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_2826 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isPartialEquivalence_2826 v6
  du_isPartialEquivalence_2826 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_2826 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (let v4 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3) in
               coe
                 (coe
                    MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
                    (coe
                       MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v4))))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isSemigroup
  d_isSemigroup_2828 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_2828 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMonoid_746
           (coe
              MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
              (coe v0)))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isCommutativeBand
  d_isCommutativeBand_2830 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  d_isCommutativeBand_2830 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isCommutativeBand_2830 v6
  du_isCommutativeBand_2830 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  du_isCommutativeBand_2830 v0
    = coe
        MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916 (coe v0)
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.isUnitalMagma
  d_isUnitalMagma_2832 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsUnitalMagma_642
  d_isUnitalMagma_2832 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isUnitalMagma_2832 v6
  du_isUnitalMagma_2832 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsUnitalMagma_642
  du_isUnitalMagma_2832 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_isUnitalMagma_730
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.refl
  d_refl_2834 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_refl_2834 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_refl_34
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isMonoid_746
                    (coe
                       MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                       (coe v0))))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.reflexive
  d_reflexive_2836 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_2836 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_reflexive_2836 v6
  du_reflexive_2836 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_2836 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (let v4 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3) in
               coe
                 (\ v5 v6 v7 ->
                    coe
                      MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                      (coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v4))
                      v5))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.setoid
  d_setoid_2838 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_2838 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_setoid_2838 v6
  du_setoid_2838 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_2838 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_setoid_200
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.sym
  d_sym_2840 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_2840 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_sym_36
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isMonoid_746
                    (coe
                       MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                       (coe v0))))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.trans
  d_trans_2842 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_2842 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isMonoid_746
                    (coe
                       MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                       (coe v0))))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.∙-cong
  d_'8729''45'cong_2844 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong_2844 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_696
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isMonoid_746
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                    (coe v0)))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.∙-congʳ
  d_'8729''45'cong'691'_2846 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'691'_2846 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong'691'_2846 v6
  du_'8729''45'cong'691'_2846 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'691'_2846 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsBoundedSemilattice._.∙-congˡ
  d_'8729''45'cong'737'_2848 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'737'_2848 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong'737'_2848 v6
  du_'8729''45'cong'737'_2848 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'737'_2848 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (let v2
               = MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice
  d_IsBoundedMeetSemilattice_2850 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> ()
  d_IsBoundedMeetSemilattice_2850 = erased
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.identity
  d_identity_2862 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_identity_2862 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_identity_698
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMonoid_746
           (coe
              MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
              (coe v0)))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.identityʳ
  d_identity'691'_2864 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_identity'691'_2864 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_identity'691'_2864 v6
  du_identity'691'_2864 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_identity'691'_2864 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_identity'691'_728
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.identityˡ
  d_identity'737'_2866 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_identity'737'_2866 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_identity'737'_2866 v6
  du_identity'737'_2866 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_identity'737'_2866 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_identity'737'_726
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.isCommutativeBand
  d_isCommutativeBand_2868 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  d_isCommutativeBand_2868 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isCommutativeBand_2868 v6
  du_isCommutativeBand_2868 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  du_isCommutativeBand_2868 v0
    = coe
        MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916 (coe v0)
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.assoc
  d_assoc_2872 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_assoc_2872 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_assoc_2872 v6
  du_assoc_2872 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_assoc_2872 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_assoc_482
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.comm
  d_comm_2874 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny
  d_comm_2874 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_comm_2874 v6
  du_comm_2874 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny
  du_comm_2874 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_comm_600
        (coe
           MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916 (coe v0))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.idem
  d_idem_2876 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_idem_2876 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_idem_2876 v6
  du_idem_2876 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_idem_2876 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_idem_518
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.isBand
  d_isBand_2878 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_isBand_2878 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_isBand_2878 v6
  du_isBand_2878 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  du_isBand_2878 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isBand_598
        (coe
           MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916 (coe v0))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.isEquivalence
  d_isEquivalence_2880 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_2880 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isEquivalence_2880 v6
  du_isEquivalence_2880 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  du_isEquivalence_2880 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1)))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.isMagma
  d_isMagma_2882 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2882 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_isMagma_2882 v6
  du_isMagma_2882 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  du_isMagma_2882 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.isPartialEquivalence
  d_isPartialEquivalence_2884 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_2884 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isPartialEquivalence_2884 v6
  du_isPartialEquivalence_2884 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_2884 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (let v4 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3) in
               coe
                 (coe
                    MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
                    (coe
                       MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v4))))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.isSemigroup
  d_isSemigroup_2886 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_2886 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isSemigroup_2886 v6
  du_isSemigroup_2886 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  du_isSemigroup_2886 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.refl
  d_refl_2888 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_refl_2888 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_refl_2888 v6
  du_refl_2888 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_refl_2888 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isMagma_480
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                    (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.reflexive
  d_reflexive_2890 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_2890 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_reflexive_2890 v6
  du_reflexive_2890 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_2890 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (let v4 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3) in
               coe
                 (\ v5 v6 v7 ->
                    coe
                      MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                      (coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v4))
                      v5))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.setoid
  d_setoid_2892 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_2892 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_setoid_2892 v6
  du_setoid_2892 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_2892 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_setoid_200
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.sym
  d_sym_2894 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_2894 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_sym_2894 v6
  du_sym_2894 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_sym_2894 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_sym_36
           (coe
              MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isMagma_480
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                    (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.trans
  d_trans_2896 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_2896 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_trans_2896 v6
  du_trans_2896 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_trans_2896 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isMagma_480
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                    (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.∙-cong
  d_'8729''45'cong_2898 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong_2898 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong_2898 v6
  du_'8729''45'cong_2898 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong_2898 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1)))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.∙-congʳ
  d_'8729''45'cong'691'_2900 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'691'_2900 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong'691'_2900 v6
  du_'8729''45'cong'691'_2900 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'691'_2900 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsBoundedMeetSemilattice._.∙-congˡ
  d_'8729''45'cong'737'_2902 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'737'_2902 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong'737'_2902 v6
  du_'8729''45'cong'737'_2902 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'737'_2902 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice
  d_IsBoundedJoinSemilattice_2904 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> ()
  d_IsBoundedJoinSemilattice_2904 = erased
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.identity
  d_identity_2916 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_identity_2916 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_identity_698
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMonoid_746
           (coe
              MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
              (coe v0)))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.identityʳ
  d_identity'691'_2918 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_identity'691'_2918 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_identity'691'_2918 v6
  du_identity'691'_2918 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_identity'691'_2918 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_identity'691'_728
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.identityˡ
  d_identity'737'_2920 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_identity'737'_2920 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_identity'737'_2920 v6
  du_identity'737'_2920 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_identity'737'_2920 v0
    = let v1
            = MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.du_identity'737'_726
           (coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.isCommutativeBand
  d_isCommutativeBand_2922 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  d_isCommutativeBand_2922 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isCommutativeBand_2922 v6
  du_isCommutativeBand_2922 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  du_isCommutativeBand_2922 v0
    = coe
        MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916 (coe v0)
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.assoc
  d_assoc_2926 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_assoc_2926 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_assoc_2926 v6
  du_assoc_2926 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_assoc_2926 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_assoc_482
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.comm
  d_comm_2928 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny
  d_comm_2928 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_comm_2928 v6
  du_comm_2928 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny
  du_comm_2928 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_comm_600
        (coe
           MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916 (coe v0))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.idem
  d_idem_2930 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_idem_2930 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_idem_2930 v6
  du_idem_2930 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_idem_2930 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_idem_518
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.isBand
  d_isBand_2932 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_isBand_2932 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_isBand_2932 v6
  du_isBand_2932 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  du_isBand_2932 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isBand_598
        (coe
           MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916 (coe v0))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.isEquivalence
  d_isEquivalence_2934 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_2934 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isEquivalence_2934 v6
  du_isEquivalence_2934 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  du_isEquivalence_2934 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1)))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.isMagma
  d_isMagma_2936 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2936 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_isMagma_2936 v6
  du_isMagma_2936 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  du_isMagma_2936 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_isMagma_480
           (coe
              MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
              (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.isPartialEquivalence
  d_isPartialEquivalence_2938 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_2938 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isPartialEquivalence_2938 v6
  du_isPartialEquivalence_2938 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_2938 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (let v4 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3) in
               coe
                 (coe
                    MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
                    (coe
                       MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v4))))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.isSemigroup
  d_isSemigroup_2940 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_2940 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isSemigroup_2940 v6
  du_isSemigroup_2940 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  du_isSemigroup_2940 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
           (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1)))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.refl
  d_refl_2942 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  d_refl_2942 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_refl_2942 v6
  du_refl_2942 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny
  du_refl_2942 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isMagma_480
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                    (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.reflexive
  d_reflexive_2944 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_2944 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_reflexive_2944 v6
  du_reflexive_2944 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_2944 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (let v4 = MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3) in
               coe
                 (\ v5 v6 v7 ->
                    coe
                      MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                      (coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v4))
                      v5))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.setoid
  d_setoid_2946 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_2946 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_setoid_2946 v6
  du_setoid_2946 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_2946 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_setoid_200
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.sym
  d_sym_2948 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_2948 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_sym_2948 v6
  du_sym_2948 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_sym_2948 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_sym_36
           (coe
              MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isMagma_480
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                    (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.trans
  d_trans_2950 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_2950 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_trans_2950 v6
  du_trans_2950 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_trans_2950 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Algebra.Structures.d_isEquivalence_184
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isMagma_480
                 (coe
                    MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                    (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1))))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.∙-cong
  d_'8729''45'cong_2952 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong_2952 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong_2952 v6
  du_'8729''45'cong_2952 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong_2952 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (coe
           MAlonzo.Code.Algebra.Structures.d_'8729''45'cong_186
           (coe
              MAlonzo.Code.Algebra.Structures.d_isMagma_480
              (coe
                 MAlonzo.Code.Algebra.Structures.d_isSemigroup_516
                 (coe MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1)))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.∙-congʳ
  d_'8729''45'cong'691'_2954 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'691'_2954 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong'691'_2954 v6
  du_'8729''45'cong'691'_2954 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'691'_2954 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'691'_206
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsBoundedJoinSemilattice._.∙-congˡ
  d_'8729''45'cong'737'_2956 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8729''45'cong'737'_2956 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8729''45'cong'737'_2956 v6
  du_'8729''45'cong'737'_2956 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8729''45'cong'737'_2956 v0
    = let v1
            = coe
                MAlonzo.Code.Algebra.Structures.du_isCommutativeBand_916
                (coe v0) in
      coe
        (let v2 = MAlonzo.Code.Algebra.Structures.d_isBand_598 (coe v1) in
         coe
           (let v3
                  = MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v2) in
            coe
              (coe
                 MAlonzo.Code.Algebra.Structures.du_'8729''45'cong'737'_202
                 (coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v3)))))
  -- Algebra.Lattice.Structures.IsLattice
  d_IsLattice_2962 a0 a1 a2 a3 a4 a5 = ()
  data T_IsLattice_2962
    = C_IsLattice'46'constructor_36793 MAlonzo.Code.Relation.Binary.Structures.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)
                                       MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  -- Algebra.Lattice.Structures.IsLattice.isEquivalence
  d_isEquivalence_2984 ::
    T_IsLattice_2962 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_2984 v0
    = case coe v0 of
        C_IsLattice'46'constructor_36793 v1 v2 v3 v4 v5 v6 v7 v8 -> coe v1
        _                                                        -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsLattice.∨-comm
  d_'8744''45'comm_2986 ::
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'comm_2986 v0
    = case coe v0 of
        C_IsLattice'46'constructor_36793 v1 v2 v3 v4 v5 v6 v7 v8 -> coe v2
        _                                                        -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsLattice.∨-assoc
  d_'8744''45'assoc_2988 ::
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'assoc_2988 v0
    = case coe v0 of
        C_IsLattice'46'constructor_36793 v1 v2 v3 v4 v5 v6 v7 v8 -> coe v3
        _                                                        -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsLattice.∨-cong
  d_'8744''45'cong_2990 ::
    T_IsLattice_2962 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong_2990 v0
    = case coe v0 of
        C_IsLattice'46'constructor_36793 v1 v2 v3 v4 v5 v6 v7 v8 -> coe v4
        _                                                        -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsLattice.∧-comm
  d_'8743''45'comm_2992 ::
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'comm_2992 v0
    = case coe v0 of
        C_IsLattice'46'constructor_36793 v1 v2 v3 v4 v5 v6 v7 v8 -> coe v5
        _                                                        -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsLattice.∧-assoc
  d_'8743''45'assoc_2994 ::
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'assoc_2994 v0
    = case coe v0 of
        C_IsLattice'46'constructor_36793 v1 v2 v3 v4 v5 v6 v7 v8 -> coe v6
        _                                                        -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsLattice.∧-cong
  d_'8743''45'cong_2996 ::
    T_IsLattice_2962 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong_2996 v0
    = case coe v0 of
        C_IsLattice'46'constructor_36793 v1 v2 v3 v4 v5 v6 v7 v8 -> coe v7
        _                                                        -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsLattice.absorptive
  d_absorptive_2998 ::
    T_IsLattice_2962 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_absorptive_2998 v0
    = case coe v0 of
        C_IsLattice'46'constructor_36793 v1 v2 v3 v4 v5 v6 v7 v8 -> coe v8
        _                                                        -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsLattice._.isPartialEquivalence
  d_isPartialEquivalence_3002 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsLattice_2962 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_3002 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isPartialEquivalence_3002 v6
  du_isPartialEquivalence_3002 ::
    T_IsLattice_2962 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_3002 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
        (coe d_isEquivalence_2984 (coe v0))
  -- Algebra.Lattice.Structures.IsLattice._.refl
  d_refl_3004 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny
  d_refl_3004 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_refl_34
        (coe d_isEquivalence_2984 (coe v0))
  -- Algebra.Lattice.Structures.IsLattice._.reflexive
  d_reflexive_3006 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsLattice_2962 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_3006 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_reflexive_3006 v6
  du_reflexive_3006 ::
    T_IsLattice_2962 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_3006 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
        (coe d_isEquivalence_2984 (coe v0)) v1
  -- Algebra.Lattice.Structures.IsLattice._.sym
  d_sym_3008 ::
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_3008 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_sym_36
        (coe d_isEquivalence_2984 (coe v0))
  -- Algebra.Lattice.Structures.IsLattice._.trans
  d_trans_3010 ::
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_3010 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (coe d_isEquivalence_2984 (coe v0))
  -- Algebra.Lattice.Structures.IsLattice.∨-absorbs-∧
  d_'8744''45'absorbs'45''8743'_3012 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'absorbs'45''8743'_3012 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8744''45'absorbs'45''8743'_3012 v6
  du_'8744''45'absorbs'45''8743'_3012 ::
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'absorbs'45''8743'_3012 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
        (coe d_absorptive_2998 (coe v0))
  -- Algebra.Lattice.Structures.IsLattice.∧-absorbs-∨
  d_'8743''45'absorbs'45''8744'_3014 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'absorbs'45''8744'_3014 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8743''45'absorbs'45''8744'_3014 v6
  du_'8743''45'absorbs'45''8744'_3014 ::
    T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'absorbs'45''8744'_3014 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
        (coe d_absorptive_2998 (coe v0))
  -- Algebra.Lattice.Structures.IsLattice.∧-congˡ
  d_'8743''45'cong'737'_3016 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong'737'_3016 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10
    = du_'8743''45'cong'737'_3016 v6 v7 v8 v9 v10
  du_'8743''45'cong'737'_3016 ::
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'cong'737'_3016 v0 v1 v2 v3 v4
    = coe
        d_'8743''45'cong_2996 v0 v1 v1 v2 v3
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (d_isEquivalence_2984 (coe v0)) v1)
        v4
  -- Algebra.Lattice.Structures.IsLattice.∧-congʳ
  d_'8743''45'cong'691'_3020 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong'691'_3020 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10
    = du_'8743''45'cong'691'_3020 v6 v7 v8 v9 v10
  du_'8743''45'cong'691'_3020 ::
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'cong'691'_3020 v0 v1 v2 v3 v4
    = coe
        d_'8743''45'cong_2996 v0 v2 v3 v1 v1 v4
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (d_isEquivalence_2984 (coe v0)) v1)
  -- Algebra.Lattice.Structures.IsLattice.∨-congˡ
  d_'8744''45'cong'737'_3024 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong'737'_3024 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10
    = du_'8744''45'cong'737'_3024 v6 v7 v8 v9 v10
  du_'8744''45'cong'737'_3024 ::
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'cong'737'_3024 v0 v1 v2 v3 v4
    = coe
        d_'8744''45'cong_2990 v0 v1 v1 v2 v3
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (d_isEquivalence_2984 (coe v0)) v1)
        v4
  -- Algebra.Lattice.Structures.IsLattice.∨-congʳ
  d_'8744''45'cong'691'_3028 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong'691'_3028 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10
    = du_'8744''45'cong'691'_3028 v6 v7 v8 v9 v10
  du_'8744''45'cong'691'_3028 ::
    T_IsLattice_2962 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'cong'691'_3028 v0 v1 v2 v3 v4
    = coe
        d_'8744''45'cong_2990 v0 v2 v3 v1 v1 v4
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (d_isEquivalence_2984 (coe v0)) v1)
  -- Algebra.Lattice.Structures.IsDistributiveLattice
  d_IsDistributiveLattice_3036 a0 a1 a2 a3 a4 a5 = ()
  data T_IsDistributiveLattice_3036
    = C_IsDistributiveLattice'46'constructor_40943 T_IsLattice_2962
                                                   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
                                                   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  -- Algebra.Lattice.Structures.IsDistributiveLattice.isLattice
  d_isLattice_3048 ::
    T_IsDistributiveLattice_3036 -> T_IsLattice_2962
  d_isLattice_3048 v0
    = case coe v0 of
        C_IsDistributiveLattice'46'constructor_40943 v1 v2 v3 -> coe v1
        _                                                     -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsDistributiveLattice.∨-distrib-∧
  d_'8744''45'distrib'45''8743'_3050 ::
    T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'distrib'45''8743'_3050 v0
    = case coe v0 of
        C_IsDistributiveLattice'46'constructor_40943 v1 v2 v3 -> coe v2
        _                                                     -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsDistributiveLattice.∧-distrib-∨
  d_'8743''45'distrib'45''8744'_3052 ::
    T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'distrib'45''8744'_3052 v0
    = case coe v0 of
        C_IsDistributiveLattice'46'constructor_40943 v1 v2 v3 -> coe v3
        _                                                     -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.absorptive
  d_absorptive_3056 ::
    T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_absorptive_3056 v0
    = coe d_absorptive_2998 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.isEquivalence
  d_isEquivalence_3058 ::
    T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_3058 v0
    = coe d_isEquivalence_2984 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.isPartialEquivalence
  d_isPartialEquivalence_3060 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_3060 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isPartialEquivalence_3060 v6
  du_isPartialEquivalence_3060 ::
    T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_3060 v0
    = let v1 = d_isLattice_3048 (coe v0) in
      coe
        (coe
           MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
           (coe d_isEquivalence_2984 (coe v1)))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.refl
  d_refl_3062 :: T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny
  d_refl_3062 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_refl_34
        (coe d_isEquivalence_2984 (coe d_isLattice_3048 (coe v0)))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.reflexive
  d_reflexive_3064 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_3064 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_reflexive_3064 v6
  du_reflexive_3064 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_3064 v0
    = let v1 = d_isLattice_3048 (coe v0) in
      coe
        (\ v2 v3 v4 ->
           coe
             MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
             (coe d_isEquivalence_2984 (coe v1)) v2)
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.sym
  d_sym_3066 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_3066 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_sym_36
        (coe d_isEquivalence_2984 (coe d_isLattice_3048 (coe v0)))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.trans
  d_trans_3068 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_3068 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (coe d_isEquivalence_2984 (coe d_isLattice_3048 (coe v0)))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∧-absorbs-∨
  d_'8743''45'absorbs'45''8744'_3070 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'absorbs'45''8744'_3070 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8743''45'absorbs'45''8744'_3070 v6
  du_'8743''45'absorbs'45''8744'_3070 ::
    T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'absorbs'45''8744'_3070 v0
    = coe
        du_'8743''45'absorbs'45''8744'_3014 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∧-assoc
  d_'8743''45'assoc_3072 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'assoc_3072 v0
    = coe d_'8743''45'assoc_2994 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∧-comm
  d_'8743''45'comm_3074 ::
    T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'comm_3074 v0
    = coe d_'8743''45'comm_2992 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∧-cong
  d_'8743''45'cong_3076 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong_3076 v0
    = coe d_'8743''45'cong_2996 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∧-congʳ
  d_'8743''45'cong'691'_3078 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong'691'_3078 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8743''45'cong'691'_3078 v6
  du_'8743''45'cong'691'_3078 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'cong'691'_3078 v0
    = coe du_'8743''45'cong'691'_3020 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∧-congˡ
  d_'8743''45'cong'737'_3080 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong'737'_3080 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8743''45'cong'737'_3080 v6
  du_'8743''45'cong'737'_3080 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'cong'737'_3080 v0
    = coe du_'8743''45'cong'737'_3016 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∨-absorbs-∧
  d_'8744''45'absorbs'45''8743'_3082 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'absorbs'45''8743'_3082 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8744''45'absorbs'45''8743'_3082 v6
  du_'8744''45'absorbs'45''8743'_3082 ::
    T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'absorbs'45''8743'_3082 v0
    = coe
        du_'8744''45'absorbs'45''8743'_3012 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∨-assoc
  d_'8744''45'assoc_3084 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'assoc_3084 v0
    = coe d_'8744''45'assoc_2988 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∨-comm
  d_'8744''45'comm_3086 ::
    T_IsDistributiveLattice_3036 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'comm_3086 v0
    = coe d_'8744''45'comm_2986 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∨-cong
  d_'8744''45'cong_3088 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong_3088 v0
    = coe d_'8744''45'cong_2990 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∨-congʳ
  d_'8744''45'cong'691'_3090 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong'691'_3090 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8744''45'cong'691'_3090 v6
  du_'8744''45'cong'691'_3090 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'cong'691'_3090 v0
    = coe du_'8744''45'cong'691'_3028 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice._.∨-congˡ
  d_'8744''45'cong'737'_3092 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong'737'_3092 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8744''45'cong'737'_3092 v6
  du_'8744''45'cong'737'_3092 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'cong'737'_3092 v0
    = coe du_'8744''45'cong'737'_3024 (coe d_isLattice_3048 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice.∨-distribˡ-∧
  d_'8744''45'distrib'737''45''8743'_3094 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'distrib'737''45''8743'_3094 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8744''45'distrib'737''45''8743'_3094 v6
  du_'8744''45'distrib'737''45''8743'_3094 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'distrib'737''45''8743'_3094 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
        (coe d_'8744''45'distrib'45''8743'_3050 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice.∨-distribʳ-∧
  d_'8744''45'distrib'691''45''8743'_3096 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'distrib'691''45''8743'_3096 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8744''45'distrib'691''45''8743'_3096 v6
  du_'8744''45'distrib'691''45''8743'_3096 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'distrib'691''45''8743'_3096 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
        (coe d_'8744''45'distrib'45''8743'_3050 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice.∧-distribˡ-∨
  d_'8743''45'distrib'737''45''8744'_3098 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'distrib'737''45''8744'_3098 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8743''45'distrib'737''45''8744'_3098 v6
  du_'8743''45'distrib'737''45''8744'_3098 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'distrib'737''45''8744'_3098 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
        (coe d_'8743''45'distrib'45''8744'_3052 (coe v0))
  -- Algebra.Lattice.Structures.IsDistributiveLattice.∧-distribʳ-∨
  d_'8743''45'distrib'691''45''8744'_3100 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'distrib'691''45''8744'_3100 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_'8743''45'distrib'691''45''8744'_3100 v6
  du_'8743''45'distrib'691''45''8744'_3100 ::
    T_IsDistributiveLattice_3036 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'distrib'691''45''8744'_3100 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
        (coe d_'8743''45'distrib'45''8744'_3052 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra
  d_IsBooleanAlgebra_3112 a0 a1 a2 a3 a4 a5 a6 a7 a8 = ()
  data T_IsBooleanAlgebra_3112
    = C_IsBooleanAlgebra'46'constructor_44015 T_IsDistributiveLattice_3036
                                              MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
                                              MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
                                              (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
  -- Algebra.Lattice.Structures.IsBooleanAlgebra.isDistributiveLattice
  d_isDistributiveLattice_3132 ::
    T_IsBooleanAlgebra_3112 -> T_IsDistributiveLattice_3036
  d_isDistributiveLattice_3132 v0
    = case coe v0 of
        C_IsBooleanAlgebra'46'constructor_44015 v1 v2 v3 v4 -> coe v1
        _                                                   -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsBooleanAlgebra.∨-complement
  d_'8744''45'complement_3134 ::
    T_IsBooleanAlgebra_3112 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'complement_3134 v0
    = case coe v0 of
        C_IsBooleanAlgebra'46'constructor_44015 v1 v2 v3 v4 -> coe v2
        _                                                   -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsBooleanAlgebra.∧-complement
  d_'8743''45'complement_3136 ::
    T_IsBooleanAlgebra_3112 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'complement_3136 v0
    = case coe v0 of
        C_IsBooleanAlgebra'46'constructor_44015 v1 v2 v3 v4 -> coe v3
        _                                                   -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsBooleanAlgebra.¬-cong
  d_'172''45'cong_3138 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'172''45'cong_3138 v0
    = case coe v0 of
        C_IsBooleanAlgebra'46'constructor_44015 v1 v2 v3 v4 -> coe v4
        _                                                   -> MAlonzo.RTE.mazUnreachableError
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.absorptive
  d_absorptive_3142 ::
    T_IsBooleanAlgebra_3112 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_absorptive_3142 v0
    = coe
        d_absorptive_2998
        (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.isEquivalence
  d_isEquivalence_3144 ::
    T_IsBooleanAlgebra_3112 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_3144 v0
    = coe
        d_isEquivalence_2984
        (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.isLattice
  d_isLattice_3146 :: T_IsBooleanAlgebra_3112 -> T_IsLattice_2962
  d_isLattice_3146 v0
    = coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.isPartialEquivalence
  d_isPartialEquivalence_3148 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  d_isPartialEquivalence_3148 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9
    = du_isPartialEquivalence_3148 v9
  du_isPartialEquivalence_3148 ::
    T_IsBooleanAlgebra_3112 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
  du_isPartialEquivalence_3148 v0
    = let v1 = d_isDistributiveLattice_3132 (coe v0) in
      coe
        (let v2 = d_isLattice_3048 (coe v1) in
         coe
           (coe
              MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
              (coe d_isEquivalence_2984 (coe v2))))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.refl
  d_refl_3150 :: T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  d_refl_3150 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_refl_34
        (coe
           d_isEquivalence_2984
           (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0))))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.reflexive
  d_reflexive_3152 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_reflexive_3152 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9
    = du_reflexive_3152 v9
  du_reflexive_3152 ::
    T_IsBooleanAlgebra_3112 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_reflexive_3152 v0
    = let v1 = d_isDistributiveLattice_3132 (coe v0) in
      coe
        (let v2 = d_isLattice_3048 (coe v1) in
         coe
           (\ v3 v4 v5 ->
              coe
                MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                (coe d_isEquivalence_2984 (coe v2)) v3))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.sym
  d_sym_3154 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_sym_3154 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_sym_36
        (coe
           d_isEquivalence_2984
           (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0))))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.trans
  d_trans_3156 ::
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_trans_3156 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.d_trans_38
        (coe
           d_isEquivalence_2984
           (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0))))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-absorbs-∨
  d_'8743''45'absorbs'45''8744'_3158 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny -> T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'absorbs'45''8744'_3158 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7
                                     ~v8 v9
    = du_'8743''45'absorbs'45''8744'_3158 v9
  du_'8743''45'absorbs'45''8744'_3158 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'absorbs'45''8744'_3158 v0
    = let v1 = d_isDistributiveLattice_3132 (coe v0) in
      coe
        (coe
           du_'8743''45'absorbs'45''8744'_3014
           (coe d_isLattice_3048 (coe v1)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-assoc
  d_'8743''45'assoc_3160 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'assoc_3160 v0
    = coe
        d_'8743''45'assoc_2994
        (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-comm
  d_'8743''45'comm_3162 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'comm_3162 v0
    = coe
        d_'8743''45'comm_2992
        (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-cong
  d_'8743''45'cong_3164 ::
    T_IsBooleanAlgebra_3112 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong_3164 v0
    = coe
        d_'8743''45'cong_2996
        (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-congʳ
  d_'8743''45'cong'691'_3166 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong'691'_3166 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9
    = du_'8743''45'cong'691'_3166 v9
  du_'8743''45'cong'691'_3166 ::
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'cong'691'_3166 v0
    = let v1 = d_isDistributiveLattice_3132 (coe v0) in
      coe
        (coe du_'8743''45'cong'691'_3020 (coe d_isLattice_3048 (coe v1)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-congˡ
  d_'8743''45'cong'737'_3168 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'cong'737'_3168 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9
    = du_'8743''45'cong'737'_3168 v9
  du_'8743''45'cong'737'_3168 ::
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'cong'737'_3168 v0
    = let v1 = d_isDistributiveLattice_3132 (coe v0) in
      coe
        (coe du_'8743''45'cong'737'_3016 (coe d_isLattice_3048 (coe v1)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-distrib-∨
  d_'8743''45'distrib'45''8744'_3170 ::
    T_IsBooleanAlgebra_3112 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'distrib'45''8744'_3170 v0
    = coe
        d_'8743''45'distrib'45''8744'_3052
        (coe d_isDistributiveLattice_3132 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-distribʳ-∨
  d_'8743''45'distrib'691''45''8744'_3172 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'distrib'691''45''8744'_3172 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
                                          ~v7 ~v8 v9
    = du_'8743''45'distrib'691''45''8744'_3172 v9
  du_'8743''45'distrib'691''45''8744'_3172 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'distrib'691''45''8744'_3172 v0
    = coe
        du_'8743''45'distrib'691''45''8744'_3100
        (coe d_isDistributiveLattice_3132 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∧-distribˡ-∨
  d_'8743''45'distrib'737''45''8744'_3174 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8743''45'distrib'737''45''8744'_3174 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
                                          ~v7 ~v8 v9
    = du_'8743''45'distrib'737''45''8744'_3174 v9
  du_'8743''45'distrib'737''45''8744'_3174 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8743''45'distrib'737''45''8744'_3174 v0
    = coe
        du_'8743''45'distrib'737''45''8744'_3098
        (coe d_isDistributiveLattice_3132 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-absorbs-∧
  d_'8744''45'absorbs'45''8743'_3176 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny -> T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'absorbs'45''8743'_3176 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7
                                     ~v8 v9
    = du_'8744''45'absorbs'45''8743'_3176 v9
  du_'8744''45'absorbs'45''8743'_3176 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'absorbs'45''8743'_3176 v0
    = let v1 = d_isDistributiveLattice_3132 (coe v0) in
      coe
        (coe
           du_'8744''45'absorbs'45''8743'_3012
           (coe d_isLattice_3048 (coe v1)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-assoc
  d_'8744''45'assoc_3178 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'assoc_3178 v0
    = coe
        d_'8744''45'assoc_2988
        (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-comm
  d_'8744''45'comm_3180 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'comm_3180 v0
    = coe
        d_'8744''45'comm_2986
        (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-cong
  d_'8744''45'cong_3182 ::
    T_IsBooleanAlgebra_3112 ->
    AgdaAny ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong_3182 v0
    = coe
        d_'8744''45'cong_2990
        (coe d_isLattice_3048 (coe d_isDistributiveLattice_3132 (coe v0)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-congʳ
  d_'8744''45'cong'691'_3184 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong'691'_3184 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9
    = du_'8744''45'cong'691'_3184 v9
  du_'8744''45'cong'691'_3184 ::
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'cong'691'_3184 v0
    = let v1 = d_isDistributiveLattice_3132 (coe v0) in
      coe
        (coe du_'8744''45'cong'691'_3028 (coe d_isLattice_3048 (coe v1)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-congˡ
  d_'8744''45'cong'737'_3186 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'cong'737'_3186 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9
    = du_'8744''45'cong'737'_3186 v9
  du_'8744''45'cong'737'_3186 ::
    T_IsBooleanAlgebra_3112 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'cong'737'_3186 v0
    = let v1 = d_isDistributiveLattice_3132 (coe v0) in
      coe
        (coe du_'8744''45'cong'737'_3024 (coe d_isLattice_3048 (coe v1)))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-distrib-∧
  d_'8744''45'distrib'45''8743'_3188 ::
    T_IsBooleanAlgebra_3112 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'distrib'45''8743'_3188 v0
    = coe
        d_'8744''45'distrib'45''8743'_3050
        (coe d_isDistributiveLattice_3132 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-distribʳ-∧
  d_'8744''45'distrib'691''45''8743'_3190 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'distrib'691''45''8743'_3190 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
                                          ~v7 ~v8 v9
    = du_'8744''45'distrib'691''45''8743'_3190 v9
  du_'8744''45'distrib'691''45''8743'_3190 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'distrib'691''45''8743'_3190 v0
    = coe
        du_'8744''45'distrib'691''45''8743'_3096
        (coe d_isDistributiveLattice_3132 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra._.∨-distribˡ-∧
  d_'8744''45'distrib'737''45''8743'_3192 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_'8744''45'distrib'737''45''8743'_3192 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
                                          ~v7 ~v8 v9
    = du_'8744''45'distrib'737''45''8743'_3192 v9
  du_'8744''45'distrib'737''45''8743'_3192 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_'8744''45'distrib'737''45''8743'_3192 v0
    = coe
        du_'8744''45'distrib'737''45''8743'_3094
        (coe d_isDistributiveLattice_3132 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra.∨-complementˡ
  d_'8744''45'complement'737'_3194 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  d_'8744''45'complement'737'_3194 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7
                                   ~v8 v9
    = du_'8744''45'complement'737'_3194 v9
  du_'8744''45'complement'737'_3194 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  du_'8744''45'complement'737'_3194 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
        (coe d_'8744''45'complement_3134 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra.∨-complementʳ
  d_'8744''45'complement'691'_3196 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  d_'8744''45'complement'691'_3196 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7
                                   ~v8 v9
    = du_'8744''45'complement'691'_3196 v9
  du_'8744''45'complement'691'_3196 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  du_'8744''45'complement'691'_3196 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
        (coe d_'8744''45'complement_3134 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra.∧-complementˡ
  d_'8743''45'complement'737'_3198 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  d_'8743''45'complement'737'_3198 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7
                                   ~v8 v9
    = du_'8743''45'complement'737'_3198 v9
  du_'8743''45'complement'737'_3198 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  du_'8743''45'complement'737'_3198 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
        (coe d_'8743''45'complement_3136 (coe v0))
  -- Algebra.Lattice.Structures.IsBooleanAlgebra.∧-complementʳ
  d_'8743''45'complement'691'_3200 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  d_'8743''45'complement'691'_3200 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7
                                   ~v8 v9
    = du_'8743''45'complement'691'_3200 v9
  du_'8743''45'complement'691'_3200 ::
    T_IsBooleanAlgebra_3112 -> AgdaAny -> AgdaAny
  du_'8743''45'complement'691'_3200 v0
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
        (coe d_'8743''45'complement_3136 (coe v0))
  