{-# 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.Properties.DistributiveLattice where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Properties.Lattice
import qualified MAlonzo.Code.Algebra.Properties.Semilattice
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Lattice
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Setoid
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Algebra.Properties.DistributiveLattice._._DistributesOver_
d__DistributesOver__80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d__DistributesOver__80 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d__DistributesOver__80 = T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Properties.DistributiveLattice._._DistributesOverʳ_
d__DistributesOver'691'__82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d__DistributesOver'691'__82 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d__DistributesOver'691'__82 = T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Properties.DistributiveLattice._._DistributesOverˡ_
d__DistributesOver'737'__84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d__DistributesOver'737'__84 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d__DistributesOver'737'__84 = T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Properties.DistributiveLattice._.isOrderTheoreticLattice
d_isOrderTheoreticLattice_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsLattice_810
d_isOrderTheoreticLattice_174 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsLattice_810
d_isOrderTheoreticLattice_174 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsLattice_810
du_isOrderTheoreticLattice_174 T_DistributiveLattice_1228
v2
du_isOrderTheoreticLattice_174 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsLattice_810
du_isOrderTheoreticLattice_174 :: T_DistributiveLattice_1228 -> T_IsLattice_810
du_isOrderTheoreticLattice_174 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsLattice_810) -> AgdaAny -> T_IsLattice_810
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsLattice_810
MAlonzo.Code.Algebra.Properties.Lattice.du_isOrderTheoreticLattice_1712
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.orderTheoreticLattice
d_orderTheoreticLattice_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_Lattice_898
d_orderTheoreticLattice_176 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_Lattice_898
d_orderTheoreticLattice_176 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Lattice_898
du_orderTheoreticLattice_176 T_DistributiveLattice_1228
v2
du_orderTheoreticLattice_176 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_Lattice_898
du_orderTheoreticLattice_176 :: T_DistributiveLattice_1228 -> T_Lattice_898
du_orderTheoreticLattice_176 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_Lattice_898) -> AgdaAny -> T_Lattice_898
forall a b. a -> b
coe
      T_Lattice_1144 -> T_Lattice_898
MAlonzo.Code.Algebra.Properties.Lattice.du_orderTheoreticLattice_1714
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.poset
d_poset_178 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_poset_178 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_Poset_282
d_poset_178 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 = T_DistributiveLattice_1228 -> T_Poset_282
du_poset_178 T_DistributiveLattice_1228
v2
du_poset_178 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_poset_178 :: T_DistributiveLattice_1228 -> T_Poset_282
du_poset_178 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_Poset_282
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_Poset_282) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_Poset_282
MAlonzo.Code.Algebra.Properties.Semilattice.du_poset_162
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'semilattice_1600
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∧-idem
d_'8743''45'idem_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny
d_'8743''45'idem_180 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
d_'8743''45'idem_180 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 = T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
du_'8743''45'idem_180 T_DistributiveLattice_1228
v2
du_'8743''45'idem_180 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny
du_'8743''45'idem_180 :: T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
du_'8743''45'idem_180 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Lattice_1144 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'idem_1588
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-idempotent
d_'8743''45'idempotent_182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny
d_'8743''45'idempotent_182 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
d_'8743''45'idempotent_182 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
du_'8743''45'idempotent_182 T_DistributiveLattice_1228
v2
du_'8743''45'idempotent_182 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny
du_'8743''45'idempotent_182 :: T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
du_'8743''45'idempotent_182 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Lattice_1144 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'idempotent_1708
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-isBand
d_'8743''45'isBand_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
d_'8743''45'isBand_184 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsBand_230
d_'8743''45'isBand_184 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 = T_DistributiveLattice_1228 -> T_IsBand_230
du_'8743''45'isBand_184 T_DistributiveLattice_1228
v2
du_'8743''45'isBand_184 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
du_'8743''45'isBand_184 :: T_DistributiveLattice_1228 -> T_IsBand_230
du_'8743''45'isBand_184 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsBand_230) -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsBand_230
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'isBand_1596
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-isMagma
d_'8743''45'isMagma_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'8743''45'isMagma_186 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsMagma_86
d_'8743''45'isMagma_186 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 = T_DistributiveLattice_1228 -> T_IsMagma_86
du_'8743''45'isMagma_186 T_DistributiveLattice_1228
v2
du_'8743''45'isMagma_186 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'8743''45'isMagma_186 :: T_DistributiveLattice_1228 -> T_IsMagma_86
du_'8743''45'isMagma_186 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsMagma_86
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'isMagma_1592
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_188 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_188 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_188 T_DistributiveLattice_1228
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_188 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_188 :: T_DistributiveLattice_1228 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_188 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_IsJoinSemilattice_68
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_IsJoinSemilattice_68) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_IsJoinSemilattice_68
MAlonzo.Code.Algebra.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'semilattice_1600
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_190 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_190 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_190 T_DistributiveLattice_1228
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_190 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_190 :: T_DistributiveLattice_1228 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_190 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_IsMeetSemilattice_438
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_IsMeetSemilattice_438)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_IsMeetSemilattice_438
MAlonzo.Code.Algebra.Properties.Semilattice.du_'8743''45'isOrderTheoreticMeetSemilattice_176
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'semilattice_1600
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∧-isSemigroup
d_'8743''45'isSemigroup_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'8743''45'isSemigroup_192 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsSemigroup_194
d_'8743''45'isSemigroup_192 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsSemigroup_194
du_'8743''45'isSemigroup_192 T_DistributiveLattice_1228
v2
du_'8743''45'isSemigroup_192 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'8743''45'isSemigroup_192 :: T_DistributiveLattice_1228 -> T_IsSemigroup_194
du_'8743''45'isSemigroup_192 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsSemigroup_194)
-> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'isSemigroup_1594
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-isSemilattice
d_'8743''45'isSemilattice_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
d_'8743''45'isSemilattice_194 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsSemilattice_312
d_'8743''45'isSemilattice_194 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsSemilattice_312
du_'8743''45'isSemilattice_194 T_DistributiveLattice_1228
v2
du_'8743''45'isSemilattice_194 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
du_'8743''45'isSemilattice_194 :: T_DistributiveLattice_1228 -> T_IsSemilattice_312
du_'8743''45'isSemilattice_194 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsSemilattice_312)
-> AgdaAny -> T_IsSemilattice_312
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'isSemilattice_1598
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_196 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_196 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_196 T_DistributiveLattice_1228
v2
du_'8743''45'orderTheoreticJoinSemilattice_196 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_196 :: T_DistributiveLattice_1228 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_196 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_JoinSemilattice_170
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_JoinSemilattice_170) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_JoinSemilattice_170
MAlonzo.Code.Algebra.Properties.Semilattice.du_'8743''45'orderTheoreticJoinSemilattice_182
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'semilattice_1600
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_198 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_198 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_198 T_DistributiveLattice_1228
v2
du_'8743''45'orderTheoreticMeetSemilattice_198 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_198 :: T_DistributiveLattice_1228 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_198 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_MeetSemilattice_540
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_MeetSemilattice_540) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_MeetSemilattice_540
MAlonzo.Code.Algebra.Properties.Semilattice.du_'8743''45'orderTheoreticMeetSemilattice_180
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'semilattice_1600
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∧-semilattice
d_'8743''45'semilattice_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
d_'8743''45'semilattice_200 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_Semilattice_402
d_'8743''45'semilattice_200 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Semilattice_402
du_'8743''45'semilattice_200 T_DistributiveLattice_1228
v2
du_'8743''45'semilattice_200 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
du_'8743''45'semilattice_200 :: T_DistributiveLattice_1228 -> T_Semilattice_402
du_'8743''45'semilattice_200 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_Semilattice_402)
-> AgdaAny -> T_Semilattice_402
forall a b. a -> b
coe
      T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45'semilattice_1600
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-∨-isLattice
d_'8743''45''8744''45'isLattice_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsLattice_740
d_'8743''45''8744''45'isLattice_202 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsLattice_740
d_'8743''45''8744''45'isLattice_202 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsLattice_740
du_'8743''45''8744''45'isLattice_202 T_DistributiveLattice_1228
v2
du_'8743''45''8744''45'isLattice_202 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsLattice_740
du_'8743''45''8744''45'isLattice_202 :: T_DistributiveLattice_1228 -> T_IsLattice_740
du_'8743''45''8744''45'isLattice_202 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45''8744''45'isLattice_1636
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-∨-lattice
d_'8743''45''8744''45'lattice_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144
d_'8743''45''8744''45'lattice_204 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_Lattice_1144
d_'8743''45''8744''45'lattice_204 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Lattice_1144
du_'8743''45''8744''45'lattice_204 T_DistributiveLattice_1228
v2
du_'8743''45''8744''45'lattice_204 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144
du_'8743''45''8744''45'lattice_204 :: T_DistributiveLattice_1228 -> T_Lattice_1144
du_'8743''45''8744''45'lattice_204 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_Lattice_1144) -> AgdaAny -> T_Lattice_1144
forall a b. a -> b
coe
      T_Lattice_1144 -> T_Lattice_1144
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45''8744''45'lattice_1638
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∨-idem
d_'8744''45'idem_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny
d_'8744''45'idem_206 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
d_'8744''45'idem_206 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 = T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
du_'8744''45'idem_206 T_DistributiveLattice_1228
v2
du_'8744''45'idem_206 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny
du_'8744''45'idem_206 :: T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
du_'8744''45'idem_206 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Lattice_1144 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'idem_1612
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∨-idempotent
d_'8744''45'idempotent_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny
d_'8744''45'idempotent_208 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
d_'8744''45'idempotent_208 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
du_'8744''45'idempotent_208 T_DistributiveLattice_1228
v2
du_'8744''45'idempotent_208 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny
du_'8744''45'idempotent_208 :: T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
du_'8744''45'idempotent_208 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Lattice_1144 -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'idempotent_1710
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∨-isBand
d_'8744''45'isBand_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
d_'8744''45'isBand_210 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsBand_230
d_'8744''45'isBand_210 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 = T_DistributiveLattice_1228 -> T_IsBand_230
du_'8744''45'isBand_210 T_DistributiveLattice_1228
v2
du_'8744''45'isBand_210 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
du_'8744''45'isBand_210 :: T_DistributiveLattice_1228 -> T_IsBand_230
du_'8744''45'isBand_210 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsBand_230) -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsBand_230
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'isBand_1620
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∨-isMagma
d_'8744''45'isMagma_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'8744''45'isMagma_212 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsMagma_86
d_'8744''45'isMagma_212 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 = T_DistributiveLattice_1228 -> T_IsMagma_86
du_'8744''45'isMagma_212 T_DistributiveLattice_1228
v2
du_'8744''45'isMagma_212 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'8744''45'isMagma_212 :: T_DistributiveLattice_1228 -> T_IsMagma_86
du_'8744''45'isMagma_212 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsMagma_86) -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsMagma_86
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'isMagma_1616
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_214 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_214 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_214 T_DistributiveLattice_1228
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_214 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_214 :: T_DistributiveLattice_1228 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_214 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_IsJoinSemilattice_68
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_IsJoinSemilattice_68) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_IsJoinSemilattice_68
MAlonzo.Code.Algebra.Properties.Semilattice.du_'8743''45'isOrderTheoreticJoinSemilattice_178
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'semilattice_1624
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_216 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_216 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_216 T_DistributiveLattice_1228
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_216 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_216 :: T_DistributiveLattice_1228 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_216 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_IsMeetSemilattice_438
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_IsMeetSemilattice_438)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_IsMeetSemilattice_438
MAlonzo.Code.Algebra.Properties.Semilattice.du_'8743''45'isOrderTheoreticMeetSemilattice_176
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'semilattice_1624
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∨-isSemigroup
d_'8744''45'isSemigroup_218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'8744''45'isSemigroup_218 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsSemigroup_194
d_'8744''45'isSemigroup_218 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsSemigroup_194
du_'8744''45'isSemigroup_218 T_DistributiveLattice_1228
v2
du_'8744''45'isSemigroup_218 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'8744''45'isSemigroup_218 :: T_DistributiveLattice_1228 -> T_IsSemigroup_194
du_'8744''45'isSemigroup_218 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsSemigroup_194)
-> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'isSemigroup_1618
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∨-isSemilattice
d_'8744''45'isSemilattice_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
d_'8744''45'isSemilattice_220 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsSemilattice_312
d_'8744''45'isSemilattice_220 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsSemilattice_312
du_'8744''45'isSemilattice_220 T_DistributiveLattice_1228
v2
du_'8744''45'isSemilattice_220 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
du_'8744''45'isSemilattice_220 :: T_DistributiveLattice_1228 -> T_IsSemilattice_312
du_'8744''45'isSemilattice_220 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsSemilattice_312)
-> AgdaAny -> T_IsSemilattice_312
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'isSemilattice_1622
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_222 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_222 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_222 T_DistributiveLattice_1228
v2
du_'8743''45'orderTheoreticJoinSemilattice_222 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_222 :: T_DistributiveLattice_1228 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_222 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_JoinSemilattice_170
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_JoinSemilattice_170) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_JoinSemilattice_170
MAlonzo.Code.Algebra.Properties.Semilattice.du_'8743''45'orderTheoreticJoinSemilattice_182
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'semilattice_1624
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_224 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_224 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_224 T_DistributiveLattice_1228
v2
du_'8743''45'orderTheoreticMeetSemilattice_224 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_224 :: T_DistributiveLattice_1228 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_224 T_DistributiveLattice_1228
v0
  = let v1 :: t
v1
          = (T_DistributiveLattice_1228 -> T_Lattice_1144) -> AgdaAny -> t
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
    AgdaAny -> T_MeetSemilattice_540
forall a b. a -> b
coe
      ((T_Semilattice_402 -> T_MeetSemilattice_540) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Semilattice_402 -> T_MeetSemilattice_540
MAlonzo.Code.Algebra.Properties.Semilattice.du_'8743''45'orderTheoreticMeetSemilattice_180
         ((T_Lattice_1144 -> T_Semilattice_402) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'semilattice_1624
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Algebra.Properties.DistributiveLattice._.∨-semilattice
d_'8744''45'semilattice_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
d_'8744''45'semilattice_226 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_Semilattice_402
d_'8744''45'semilattice_226 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Semilattice_402
du_'8744''45'semilattice_226 T_DistributiveLattice_1228
v2
du_'8744''45'semilattice_226 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
du_'8744''45'semilattice_226 :: T_DistributiveLattice_1228 -> T_Semilattice_402
du_'8744''45'semilattice_226 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_Semilattice_402)
-> AgdaAny -> T_Semilattice_402
forall a b. a -> b
coe
      T_Lattice_1144 -> T_Semilattice_402
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45'semilattice_1624
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∨-∧-isOrderTheoreticLattice
d_'8744''45''8743''45'isOrderTheoreticLattice_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsLattice_810
d_'8744''45''8743''45'isOrderTheoreticLattice_228 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_IsLattice_810
d_'8744''45''8743''45'isOrderTheoreticLattice_228 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsLattice_810
du_'8744''45''8743''45'isOrderTheoreticLattice_228 T_DistributiveLattice_1228
v2
du_'8744''45''8743''45'isOrderTheoreticLattice_228 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsLattice_810
du_'8744''45''8743''45'isOrderTheoreticLattice_228 :: T_DistributiveLattice_1228 -> T_IsLattice_810
du_'8744''45''8743''45'isOrderTheoreticLattice_228 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_IsLattice_810) -> AgdaAny -> T_IsLattice_810
forall a b. a -> b
coe
      T_Lattice_1144 -> T_IsLattice_810
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45''8743''45'isOrderTheoreticLattice_1650
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice._.∨-∧-orderTheoreticLattice
d_'8744''45''8743''45'orderTheoreticLattice_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_Lattice_898
d_'8744''45''8743''45'orderTheoreticLattice_230 :: T_Level_18
-> T_Level_18 -> T_DistributiveLattice_1228 -> T_Lattice_898
d_'8744''45''8743''45'orderTheoreticLattice_230 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Lattice_898
du_'8744''45''8743''45'orderTheoreticLattice_230 T_DistributiveLattice_1228
v2
du_'8744''45''8743''45'orderTheoreticLattice_230 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_Lattice_898
du_'8744''45''8743''45'orderTheoreticLattice_230 :: T_DistributiveLattice_1228 -> T_Lattice_898
du_'8744''45''8743''45'orderTheoreticLattice_230 T_DistributiveLattice_1228
v0
  = (T_Lattice_1144 -> T_Lattice_898) -> AgdaAny -> T_Lattice_898
forall a b. a -> b
coe
      T_Lattice_1144 -> T_Lattice_898
MAlonzo.Code.Algebra.Properties.Lattice.du_'8744''45''8743''45'orderTheoreticLattice_1706
      ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice.∨-distribˡ-∧
d_'8744''45'distrib'737''45''8743'_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45'distrib'737''45''8743'_232 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8744''45'distrib'737''45''8743'_232 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45'distrib'737''45''8743'_232 T_DistributiveLattice_1228
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_'8744''45'distrib'737''45''8743'_232 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45'distrib'737''45''8743'_232 :: T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45'distrib'737''45''8743'_232 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
            ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v1)
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
               ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v1)
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
                  ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
               (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     ((T_IsLattice_740 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_740 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                        ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                           ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                              (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))))
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3)))
               ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'10216'_'10217'__250
                  ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'comm_764
                     (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                        ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                           (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     AgdaAny
v2 AgdaAny
v1)
                  ((T_IsLattice_740
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsLattice_740
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8743''45'cong_774
                     (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                        ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                           (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                  ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'comm_764
                     (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                        ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                           (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     AgdaAny
v3 AgdaAny
v1)))
            ((T_IsDistributiveLattice_814
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_814
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_IsDistributiveLattice_814
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'distrib'691''45''8743'_826
               (T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                  (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
               AgdaAny
v1 AgdaAny
v2 AgdaAny
v3))
         ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'comm_764
            (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
               ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                  (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
            AgdaAny
v1 ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3)))
-- Algebra.Properties.DistributiveLattice.∨-distrib-∧
d_'8744''45'distrib'45''8743'_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'distrib'45''8743'_240 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_1228 -> T_Σ_14
d_'8744''45'distrib'45''8743'_240 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Σ_14
du_'8744''45'distrib'45''8743'_240 T_DistributiveLattice_1228
v2
du_'8744''45'distrib'45''8743'_240 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8744''45'distrib'45''8743'_240 :: T_DistributiveLattice_1228 -> T_Σ_14
du_'8744''45'distrib'45''8743'_240 T_DistributiveLattice_1228
v0
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45'distrib'737''45''8743'_232 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
      ((T_IsDistributiveLattice_814
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDistributiveLattice_814
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'distrib'691''45''8743'_826
         ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
            (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
-- Algebra.Properties.DistributiveLattice.∧-distribˡ-∨
d_'8743''45'distrib'737''45''8744'_242 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'distrib'737''45''8744'_242 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8743''45'distrib'737''45''8744'_242 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'737''45''8744'_242 T_DistributiveLattice_1228
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_'8743''45'distrib'737''45''8744'_242 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'737''45''8744'_242 :: T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'737''45''8744'_242 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
            ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
               ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
                  ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1))
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3)))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
               ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
                  ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
                     ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3)))
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3)))
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                  ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
                     ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
                        ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3)))
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3)))
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                     ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
                        ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
                           ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3)))
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                        (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                           ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                              ((T_IsLattice_740 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsLattice_740 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                                 ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                                    ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                                       (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))))
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3)))
                        ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                           (T_IsLattice_740 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                              ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe
                                 T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                                 ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                                    (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))))
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1
                                 ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2
                                 ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3)))
                           ((T_IsDistributiveLattice_814
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_814
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                              T_IsDistributiveLattice_814
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'distrib'691''45''8743'_826
                              (T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                                 (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3) AgdaAny
v1
                              AgdaAny
v2)))
                     ((T_IsLattice_740
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_740
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8743''45'cong'691'_798
                        ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                           ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                              (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                        (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                        ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                           (T_IsLattice_740 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                              ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe
                                 T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                                 ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                                    (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))))
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1
                              ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                           AgdaAny
v1
                           (let v4 :: T_IsDistributiveLattice_814
v4
                                  = T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                                      (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8744''45'absorbs'45''8743'_790
                                 (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824 (T_IsDistributiveLattice_814 -> T_IsDistributiveLattice_814
forall a b. a -> b
coe T_IsDistributiveLattice_814
v4)) AgdaAny
v1
                                 AgdaAny
v3)))))
                  ((T_IsLattice_740
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8743''45'cong'737'_794
                     ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                        ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                           (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                     ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                        (T_IsLattice_740 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                           ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe
                              T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                              ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                                 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))))
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
                        ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                           ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
                        ((T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45'distrib'737''45''8743'_232 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)))))
               ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8743''45'assoc_772
                  (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                     ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                        (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                  AgdaAny
v1 ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3)))
            ((T_IsLattice_740
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsLattice_740
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8743''45'cong'691'_798
               ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                  ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                     (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3)
               (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1)
                  (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v4)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1))
               (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
                  (\ AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v5)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1))
               ((T_IsLattice_740
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsLattice_740
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8743''45'cong'737'_794
                  ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                     ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                        (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'comm_764
                     (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                        ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                           (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     AgdaAny
v1 AgdaAny
v2))))
         ((T_IsLattice_740
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_740
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8743''45'cong'691'_798
            ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
               ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                  (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3)
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2))
            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               (T_IsLattice_740 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                  ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe
                     T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                     ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                        (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2))
               AgdaAny
v1
               (let v4 :: T_IsDistributiveLattice_814
v4
                      = T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                          (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.du_'8743''45'absorbs'45''8744'_792
                     (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824 (T_IsDistributiveLattice_814 -> T_IsDistributiveLattice_814
forall a b. a -> b
coe T_IsDistributiveLattice_814
v4)) AgdaAny
v1
                     AgdaAny
v2)))))
-- Algebra.Properties.DistributiveLattice.∧-distribʳ-∨
d_'8743''45'distrib'691''45''8744'_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45'distrib'691''45''8744'_250 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8743''45'distrib'691''45''8744'_250 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'691''45''8744'_250 T_DistributiveLattice_1228
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_'8743''45'distrib'691''45''8744'_250 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'691''45''8744'_250 :: T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'691''45''8744'_250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
            ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v1)
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
         ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1))
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
               ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1))
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               ((T_Lattice_1144 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> T_Setoid_44
MAlonzo.Code.Algebra.Bundles.du_setoid_1218
                  ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1))
               ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1))
               (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     ((T_IsLattice_740 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsLattice_740 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                        ((T_IsDistributiveLattice_814 -> T_IsLattice_740)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                           ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                              (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))))
                  ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1)))
               ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'10216'_'10217'__250
                  ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8743''45'comm_770
                     (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                        ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                           (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     AgdaAny
v1 AgdaAny
v2)
                  ((T_IsLattice_740
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsLattice_740
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'cong_768
                     (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                        ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                           (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v2)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v1)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v1 AgdaAny
v3)
                     ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v1))
                  ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8743''45'comm_770
                     (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
                        ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                           T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                           (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
                     AgdaAny
v1 AgdaAny
v3)))
            ((T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'737''45''8744'_242 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)))
         ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8743''45'comm_770
            (T_IsDistributiveLattice_814 -> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.d_isLattice_824
               ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
                  T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                  (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
            ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v1))
-- Algebra.Properties.DistributiveLattice.∧-distrib-∨
d_'8743''45'distrib'45''8744'_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'distrib'45''8744'_258 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_1228 -> T_Σ_14
d_'8743''45'distrib'45''8744'_258 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Σ_14
du_'8743''45'distrib'45''8744'_258 T_DistributiveLattice_1228
v2
du_'8743''45'distrib'45''8744'_258 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8743''45'distrib'45''8744'_258 :: T_DistributiveLattice_1228 -> T_Σ_14
du_'8743''45'distrib'45''8744'_258 T_DistributiveLattice_1228
v0
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'737''45''8744'_242 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
      ((T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'691''45''8744'_250 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice.∧-∨-isDistributiveLattice
d_'8743''45''8744''45'isDistributiveLattice_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsDistributiveLattice_814
d_'8743''45''8744''45'isDistributiveLattice_260 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_IsDistributiveLattice_814
d_'8743''45''8744''45'isDistributiveLattice_260 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
du_'8743''45''8744''45'isDistributiveLattice_260 T_DistributiveLattice_1228
v2
du_'8743''45''8744''45'isDistributiveLattice_260 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Structures.T_IsDistributiveLattice_814
du_'8743''45''8744''45'isDistributiveLattice_260 :: T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
du_'8743''45''8744''45'isDistributiveLattice_260 T_DistributiveLattice_1228
v0
  = (T_IsLattice_740
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny -> T_IsDistributiveLattice_814
forall a b. a -> b
coe
      T_IsLattice_740
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Structures.C_IsDistributiveLattice'46'constructor_24097
      ((T_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Properties.Lattice.du_'8743''45''8744''45'isLattice_1636
         ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)))
      ((T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'691''45''8744'_250 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice.∧-∨-distributiveLattice
d_'8743''45''8744''45'distributiveLattice_262 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228
d_'8743''45''8744''45'distributiveLattice_262 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> T_DistributiveLattice_1228
d_'8743''45''8744''45'distributiveLattice_262 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
du_'8743''45''8744''45'distributiveLattice_262 T_DistributiveLattice_1228
v2
du_'8743''45''8744''45'distributiveLattice_262 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228
du_'8743''45''8744''45'distributiveLattice_262 :: T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
du_'8743''45''8744''45'distributiveLattice_262 T_DistributiveLattice_1228
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsDistributiveLattice_814
 -> T_DistributiveLattice_1228)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_DistributiveLattice_1228
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_814
-> T_DistributiveLattice_1228
MAlonzo.Code.Algebra.Bundles.C_DistributiveLattice'46'constructor_20939
      (T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
      (T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
      ((T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
du_'8743''45''8744''45'isDistributiveLattice_260 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
-- Algebra.Properties.DistributiveLattice.∨-∧-distribˡ
d_'8744''45''8743''45'distrib'737'_264 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8744''45''8743''45'distrib'737'_264 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8744''45''8743''45'distrib'737'_264 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45''8743''45'distrib'737'_264 T_DistributiveLattice_1228
v2
du_'8744''45''8743''45'distrib'737'_264 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45''8743''45'distrib'737'_264 :: T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45''8743''45'distrib'737'_264 T_DistributiveLattice_1228
v0
  = (T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8744''45'distrib'737''45''8743'_232 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)
-- Algebra.Properties.DistributiveLattice.∨-∧-distrib
d_'8744''45''8743''45'distrib_266 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45''8743''45'distrib_266 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_1228 -> T_Σ_14
d_'8744''45''8743''45'distrib_266 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Σ_14
du_'8744''45''8743''45'distrib_266 T_DistributiveLattice_1228
v2
du_'8744''45''8743''45'distrib_266 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8744''45''8743''45'distrib_266 :: T_DistributiveLattice_1228 -> T_Σ_14
du_'8744''45''8743''45'distrib_266 T_DistributiveLattice_1228
v0
  = (T_DistributiveLattice_1228 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Σ_14
du_'8744''45'distrib'45''8743'_240 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)
-- Algebra.Properties.DistributiveLattice.∧-∨-distribˡ
d_'8743''45''8744''45'distrib'737'_268 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45''8744''45'distrib'737'_268 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8743''45''8744''45'distrib'737'_268 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45''8744''45'distrib'737'_268 T_DistributiveLattice_1228
v2
du_'8743''45''8744''45'distrib'737'_268 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45''8744''45'distrib'737'_268 :: T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45''8744''45'distrib'737'_268 T_DistributiveLattice_1228
v0
  = (T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'737''45''8744'_242 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)
-- Algebra.Properties.DistributiveLattice.∧-∨-distribʳ
d_'8743''45''8744''45'distrib'691'_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8743''45''8744''45'distrib'691'_270 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8743''45''8744''45'distrib'691'_270 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45''8744''45'distrib'691'_270 T_DistributiveLattice_1228
v2
du_'8743''45''8744''45'distrib'691'_270 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45''8744''45'distrib'691'_270 :: T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45''8744''45'distrib'691'_270 T_DistributiveLattice_1228
v0
  = (T_DistributiveLattice_1228
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8743''45'distrib'691''45''8744'_250 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)
-- Algebra.Properties.DistributiveLattice.∧-∨-distrib
d_'8743''45''8744''45'distrib_272 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45''8744''45'distrib_272 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_1228 -> T_Σ_14
d_'8743''45''8744''45'distrib_272 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2
  = T_DistributiveLattice_1228 -> T_Σ_14
du_'8743''45''8744''45'distrib_272 T_DistributiveLattice_1228
v2
du_'8743''45''8744''45'distrib_272 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8743''45''8744''45'distrib_272 :: T_DistributiveLattice_1228 -> T_Σ_14
du_'8743''45''8744''45'distrib_272 T_DistributiveLattice_1228
v0
  = (T_DistributiveLattice_1228 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Σ_14
du_'8743''45'distrib'45''8744'_258 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0)
-- Algebra.Properties.DistributiveLattice.replace-equality
d_replace'45'equality_280 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16) ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228
d_replace'45'equality_280 :: T_Level_18
-> T_Level_18
-> T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Equivalence_16)
-> T_DistributiveLattice_1228
d_replace'45'equality_280 ~T_Level_18
v0 ~T_Level_18
v1 T_DistributiveLattice_1228
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Equivalence_16
v4
  = T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> T_Equivalence_16)
-> T_DistributiveLattice_1228
du_replace'45'equality_280 T_DistributiveLattice_1228
v2 AgdaAny -> AgdaAny -> T_Equivalence_16
v4
du_replace'45'equality_280 ::
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16) ->
  MAlonzo.Code.Algebra.Bundles.T_DistributiveLattice_1228
du_replace'45'equality_280 :: T_DistributiveLattice_1228
-> (AgdaAny -> AgdaAny -> T_Equivalence_16)
-> T_DistributiveLattice_1228
du_replace'45'equality_280 T_DistributiveLattice_1228
v0 AgdaAny -> AgdaAny -> T_Equivalence_16
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsDistributiveLattice_814
 -> T_DistributiveLattice_1228)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_DistributiveLattice_1228
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_814
-> T_DistributiveLattice_1228
MAlonzo.Code.Algebra.Bundles.C_DistributiveLattice'46'constructor_20939
      (T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
      (T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
      ((T_IsLattice_740
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsDistributiveLattice_814)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_740
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Structures.C_IsDistributiveLattice'46'constructor_24097
         ((T_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168
            ((T_Lattice_1144
 -> (AgdaAny -> AgdaAny -> T_Equivalence_16) -> T_Lattice_1144)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144
-> (AgdaAny -> AgdaAny -> T_Equivalence_16) -> T_Lattice_1144
MAlonzo.Code.Algebra.Properties.Lattice.du_replace'45'equality_1722
               ((T_DistributiveLattice_1228 -> T_Lattice_1144)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.du_lattice_1300 (T_DistributiveLattice_1228 -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
               ((AgdaAny -> AgdaAny -> T_Equivalence_16) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Equivalence_16
v1)))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
               (T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                 (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34
                    ((AgdaAny -> AgdaAny -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_Equivalence_16
v1
                       ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0
                          ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v4) AgdaAny
v2)
                       ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1250 T_DistributiveLattice_1228
v0
                          ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v3 AgdaAny
v2)
                          ((T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DistributiveLattice_1228 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1248 T_DistributiveLattice_1228
v0 AgdaAny
v4 AgdaAny
v2))))
                 ((T_IsDistributiveLattice_814
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsDistributiveLattice_814
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                    T_IsDistributiveLattice_814
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'distrib'691''45''8743'_826
                    (T_DistributiveLattice_1228 -> T_IsDistributiveLattice_814
MAlonzo.Code.Algebra.Bundles.d_isDistributiveLattice_1252
                       (T_DistributiveLattice_1228 -> T_DistributiveLattice_1228
forall a b. a -> b
coe T_DistributiveLattice_1228
v0))
                    AgdaAny
v2 AgdaAny
v3 AgdaAny
v4))))