{-# 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.Lattice 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.Semilattice
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Product
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.Construct.NaturalOrder.Left
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.Lattice._.IsBand
d_IsBand_72 :: p -> p -> p -> p -> ()
d_IsBand_72 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Properties.Lattice._.IsLattice
d_IsLattice_98 :: p -> p -> p -> p -> p -> ()
d_IsLattice_98 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Algebra.Properties.Lattice._.IsMagma
d_IsMagma_100 :: p -> p -> p -> p -> ()
d_IsMagma_100 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Properties.Lattice._.IsSemigroup
d_IsSemigroup_110 :: p -> p -> p -> p -> ()
d_IsSemigroup_110 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Properties.Lattice._.IsSemilattice
d_IsSemilattice_112 :: p -> p -> p -> p -> ()
d_IsSemilattice_112 p
a0 p
a1 p
a2 p
a3 = ()
-- Algebra.Properties.Lattice._.Idempotent
d_Idempotent_1524 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Idempotent_1524 :: () -> () -> T_Lattice_1144 -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_Idempotent_1524 = () -> () -> T_Lattice_1144 -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
forall a. a
erased
-- Algebra.Properties.Lattice.∧-idem
d_'8743''45'idem_1588 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 -> AgdaAny -> AgdaAny
d_'8743''45'idem_1588 :: () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny
d_'8743''45'idem_1588 ~()
v0 ~()
v1 T_Lattice_1144
v2 AgdaAny
v3 = T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idem_1588 T_Lattice_1144
v2 AgdaAny
v3
du_'8743''45'idem_1588 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idem_1588 :: T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idem_1588 T_Lattice_1144
v0 AgdaAny
v1
  = (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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
         ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1)
         ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1)))
         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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1)))
            AgdaAny
v1 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_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
forall a b. a -> b
coe T_Lattice_1144
v0))))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe 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.du_'8743''45'absorbs'45''8744'_792
               (T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v1
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 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_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
forall a b. a -> b
coe T_Lattice_1144
v0))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1))
            ((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_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1))
               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.du_'8744''45'absorbs'45''8743'_790
                  (T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v1 AgdaAny
v1))))
-- Algebra.Properties.Lattice.∧-isMagma
d_'8743''45'isMagma_1592 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'8743''45'isMagma_1592 :: () -> () -> T_Lattice_1144 -> T_IsMagma_86
d_'8743''45'isMagma_1592 ~()
v0 ~()
v1 T_Lattice_1144
v2 = T_Lattice_1144 -> T_IsMagma_86
du_'8743''45'isMagma_1592 T_Lattice_1144
v2
du_'8743''45'isMagma_1592 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'8743''45'isMagma_1592 :: T_Lattice_1144 -> T_IsMagma_86
du_'8743''45'isMagma_1592 T_Lattice_1144
v0
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
      ((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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_IsLattice_740
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
-- Algebra.Properties.Lattice.∧-isSemigroup
d_'8743''45'isSemigroup_1594 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'8743''45'isSemigroup_1594 :: () -> () -> T_Lattice_1144 -> T_IsSemigroup_194
d_'8743''45'isSemigroup_1594 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsSemigroup_194
du_'8743''45'isSemigroup_1594 T_Lattice_1144
v2
du_'8743''45'isSemigroup_1594 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'8743''45'isSemigroup_1594 :: T_Lattice_1144 -> T_IsSemigroup_194
du_'8743''45'isSemigroup_1594 T_Lattice_1144
v0
  = (T_IsMagma_86
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
      ((T_Lattice_1144 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsMagma_86
du_'8743''45'isMagma_1592 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
-- Algebra.Properties.Lattice.∧-isBand
d_'8743''45'isBand_1596 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
d_'8743''45'isBand_1596 :: () -> () -> T_Lattice_1144 -> T_IsBand_230
d_'8743''45'isBand_1596 ~()
v0 ~()
v1 T_Lattice_1144
v2 = T_Lattice_1144 -> T_IsBand_230
du_'8743''45'isBand_1596 T_Lattice_1144
v2
du_'8743''45'isBand_1596 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
du_'8743''45'isBand_1596 :: T_Lattice_1144 -> T_IsBand_230
du_'8743''45'isBand_1596 T_Lattice_1144
v0
  = (T_IsSemigroup_194 -> (AgdaAny -> AgdaAny) -> T_IsBand_230)
-> AgdaAny -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe
      T_IsSemigroup_194 -> (AgdaAny -> AgdaAny) -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_4787
      ((T_Lattice_1144 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsSemigroup_194
du_'8743''45'isSemigroup_1594 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_Lattice_1144 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idem_1588 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice.∧-isSemilattice
d_'8743''45'isSemilattice_1598 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
d_'8743''45'isSemilattice_1598 :: () -> () -> T_Lattice_1144 -> T_IsSemilattice_312
d_'8743''45'isSemilattice_1598 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsSemilattice_312
du_'8743''45'isSemilattice_1598 T_Lattice_1144
v2
du_'8743''45'isSemilattice_1598 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
du_'8743''45'isSemilattice_1598 :: T_Lattice_1144 -> T_IsSemilattice_312
du_'8743''45'isSemilattice_1598 T_Lattice_1144
v0
  = (T_IsBand_230
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_312)
-> AgdaAny -> AgdaAny -> T_IsSemilattice_312
forall a b. a -> b
coe
      T_IsBand_230
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Structures.C_IsSemilattice'46'constructor_6687
      ((T_Lattice_1144 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsBand_230
du_'8743''45'isBand_1596 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
-- Algebra.Properties.Lattice.∧-semilattice
d_'8743''45'semilattice_1600 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
d_'8743''45'semilattice_1600 :: () -> () -> T_Lattice_1144 -> T_Semilattice_402
d_'8743''45'semilattice_1600 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_Semilattice_402
du_'8743''45'semilattice_1600 T_Lattice_1144
v2
du_'8743''45'semilattice_1600 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
du_'8743''45'semilattice_1600 :: T_Lattice_1144 -> T_Semilattice_402
du_'8743''45'semilattice_1600 T_Lattice_1144
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312 -> T_Semilattice_402)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Semilattice_402
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_Semilattice_402
MAlonzo.Code.Algebra.Bundles.C_Semilattice'46'constructor_7205
      (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_Lattice_1144 -> T_IsSemilattice_312) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsSemilattice_312
du_'8743''45'isSemilattice_1598 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_1604 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_1604 :: () -> () -> T_Lattice_1144 -> T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_1604 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_1604 T_Lattice_1144
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_1604 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_1604 :: T_Lattice_1144 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_1604 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_IsJoinSemilattice_68)
-> AgdaAny -> T_IsJoinSemilattice_68
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
du_'8743''45'semilattice_1600 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_1606 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_1606 :: () -> () -> T_Lattice_1144 -> T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_1606 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_1606 T_Lattice_1144
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_1606 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_1606 :: T_Lattice_1144 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_1606 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_IsMeetSemilattice_438)
-> AgdaAny -> T_IsMeetSemilattice_438
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
du_'8743''45'semilattice_1600 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_1608 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_1608 :: () -> () -> T_Lattice_1144 -> T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_1608 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_1608 T_Lattice_1144
v2
du_'8743''45'orderTheoreticJoinSemilattice_1608 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_1608 :: T_Lattice_1144 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_1608 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_JoinSemilattice_170)
-> AgdaAny -> T_JoinSemilattice_170
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
du_'8743''45'semilattice_1600 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_1610 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_1610 :: () -> () -> T_Lattice_1144 -> T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_1610 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_1610 T_Lattice_1144
v2
du_'8743''45'orderTheoreticMeetSemilattice_1610 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_1610 :: T_Lattice_1144 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_1610 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_MeetSemilattice_540)
-> AgdaAny -> T_MeetSemilattice_540
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
du_'8743''45'semilattice_1600 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice.∨-idem
d_'8744''45'idem_1612 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 -> AgdaAny -> AgdaAny
d_'8744''45'idem_1612 :: () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny
d_'8744''45'idem_1612 ~()
v0 ~()
v1 T_Lattice_1144
v2 AgdaAny
v3 = T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8744''45'idem_1612 T_Lattice_1144
v2 AgdaAny
v3
du_'8744''45'idem_1612 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8744''45'idem_1612 :: T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8744''45'idem_1612 T_Lattice_1144
v0 AgdaAny
v1
  = (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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
         ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1)
         ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1))
         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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1))
            AgdaAny
v1 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_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
forall a b. a -> b
coe T_Lattice_1144
v0))))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe 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.du_'8744''45'absorbs'45''8743'_790
               (T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v1 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_'8744''45'cong'737'_802
            ((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
forall a b. a -> b
coe T_Lattice_1144
v0))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1)
            ((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_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v1) AgdaAny
v1
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idem_1588 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))))
-- Algebra.Properties.Lattice.∨-isMagma
d_'8744''45'isMagma_1616 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'8744''45'isMagma_1616 :: () -> () -> T_Lattice_1144 -> T_IsMagma_86
d_'8744''45'isMagma_1616 ~()
v0 ~()
v1 T_Lattice_1144
v2 = T_Lattice_1144 -> T_IsMagma_86
du_'8744''45'isMagma_1616 T_Lattice_1144
v2
du_'8744''45'isMagma_1616 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'8744''45'isMagma_1616 :: T_Lattice_1144 -> T_IsMagma_86
du_'8744''45'isMagma_1616 T_Lattice_1144
v0
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
      ((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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_IsLattice_740
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
-- Algebra.Properties.Lattice.∨-isSemigroup
d_'8744''45'isSemigroup_1618 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'8744''45'isSemigroup_1618 :: () -> () -> T_Lattice_1144 -> T_IsSemigroup_194
d_'8744''45'isSemigroup_1618 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsSemigroup_194
du_'8744''45'isSemigroup_1618 T_Lattice_1144
v2
du_'8744''45'isSemigroup_1618 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'8744''45'isSemigroup_1618 :: T_Lattice_1144 -> T_IsSemigroup_194
du_'8744''45'isSemigroup_1618 T_Lattice_1144
v0
  = (T_IsMagma_86
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
      ((T_Lattice_1144 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsMagma_86
du_'8744''45'isMagma_1616 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'assoc_766
         ((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
forall a b. a -> b
coe T_Lattice_1144
v0)))
-- Algebra.Properties.Lattice.∨-isBand
d_'8744''45'isBand_1620 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
d_'8744''45'isBand_1620 :: () -> () -> T_Lattice_1144 -> T_IsBand_230
d_'8744''45'isBand_1620 ~()
v0 ~()
v1 T_Lattice_1144
v2 = T_Lattice_1144 -> T_IsBand_230
du_'8744''45'isBand_1620 T_Lattice_1144
v2
du_'8744''45'isBand_1620 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsBand_230
du_'8744''45'isBand_1620 :: T_Lattice_1144 -> T_IsBand_230
du_'8744''45'isBand_1620 T_Lattice_1144
v0
  = (T_IsSemigroup_194 -> (AgdaAny -> AgdaAny) -> T_IsBand_230)
-> AgdaAny -> AgdaAny -> T_IsBand_230
forall a b. a -> b
coe
      T_IsSemigroup_194 -> (AgdaAny -> AgdaAny) -> T_IsBand_230
MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_4787
      ((T_Lattice_1144 -> T_IsSemigroup_194) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsSemigroup_194
du_'8744''45'isSemigroup_1618 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_Lattice_1144 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8744''45'idem_1612 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice.∨-isSemilattice
d_'8744''45'isSemilattice_1622 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
d_'8744''45'isSemilattice_1622 :: () -> () -> T_Lattice_1144 -> T_IsSemilattice_312
d_'8744''45'isSemilattice_1622 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsSemilattice_312
du_'8744''45'isSemilattice_1622 T_Lattice_1144
v2
du_'8744''45'isSemilattice_1622 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemilattice_312
du_'8744''45'isSemilattice_1622 :: T_Lattice_1144 -> T_IsSemilattice_312
du_'8744''45'isSemilattice_1622 T_Lattice_1144
v0
  = (T_IsBand_230
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_312)
-> AgdaAny -> AgdaAny -> T_IsSemilattice_312
forall a b. a -> b
coe
      T_IsBand_230
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Structures.C_IsSemilattice'46'constructor_6687
      ((T_Lattice_1144 -> T_IsBand_230) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsBand_230
du_'8744''45'isBand_1620 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
-- Algebra.Properties.Lattice.∨-semilattice
d_'8744''45'semilattice_1624 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
d_'8744''45'semilattice_1624 :: () -> () -> T_Lattice_1144 -> T_Semilattice_402
d_'8744''45'semilattice_1624 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_Semilattice_402
du_'8744''45'semilattice_1624 T_Lattice_1144
v2
du_'8744''45'semilattice_1624 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402
du_'8744''45'semilattice_1624 :: T_Lattice_1144 -> T_Semilattice_402
du_'8744''45'semilattice_1624 T_Lattice_1144
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312 -> T_Semilattice_402)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Semilattice_402
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> T_Semilattice_402
MAlonzo.Code.Algebra.Bundles.C_Semilattice'46'constructor_7205
      (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_Lattice_1144 -> T_IsSemilattice_312) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsSemilattice_312
du_'8744''45'isSemilattice_1622 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_1628 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_1628 :: () -> () -> T_Lattice_1144 -> T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_1628 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_1628 T_Lattice_1144
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_1628 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_1628 :: T_Lattice_1144 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_1628 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_IsJoinSemilattice_68)
-> AgdaAny -> T_IsJoinSemilattice_68
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
du_'8744''45'semilattice_1624 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_1630 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_1630 :: () -> () -> T_Lattice_1144 -> T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_1630 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_1630 T_Lattice_1144
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_1630 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_1630 :: T_Lattice_1144 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_1630 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_IsMeetSemilattice_438)
-> AgdaAny -> T_IsMeetSemilattice_438
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
du_'8744''45'semilattice_1624 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_1632 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_1632 :: () -> () -> T_Lattice_1144 -> T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_1632 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_1632 T_Lattice_1144
v2
du_'8743''45'orderTheoreticJoinSemilattice_1632 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_1632 :: T_Lattice_1144 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_1632 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_JoinSemilattice_170)
-> AgdaAny -> T_JoinSemilattice_170
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
du_'8744''45'semilattice_1624 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_1634 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_1634 :: () -> () -> T_Lattice_1144 -> T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_1634 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_1634 T_Lattice_1144
v2
du_'8743''45'orderTheoreticMeetSemilattice_1634 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_1634 :: T_Lattice_1144 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_1634 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_MeetSemilattice_540)
-> AgdaAny -> T_MeetSemilattice_540
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
du_'8744''45'semilattice_1624 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice.∧-∨-isLattice
d_'8743''45''8744''45'isLattice_1636 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsLattice_740
d_'8743''45''8744''45'isLattice_1636 :: () -> () -> T_Lattice_1144 -> T_IsLattice_740
d_'8743''45''8744''45'isLattice_1636 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsLattice_740
du_'8743''45''8744''45'isLattice_1636 T_Lattice_1144
v2
du_'8743''45''8744''45'isLattice_1636 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Structures.T_IsLattice_740
du_'8743''45''8744''45'isLattice_1636 :: T_Lattice_1144 -> T_IsLattice_740
du_'8743''45''8744''45'isLattice_1636 T_Lattice_1144
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsLattice_740)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsLattice_740
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.C_IsLattice'46'constructor_20027
      ((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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_IsLattice_740
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsLattice_740 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Structures.d_'8744''45'assoc_766
         ((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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_IsLattice_740
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> 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_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
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_swap_386
         ((T_IsLattice_740 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLattice_740 -> T_Σ_14
MAlonzo.Code.Algebra.Structures.d_absorptive_776
            ((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
forall a b. a -> b
coe T_Lattice_1144
v0))))
-- Algebra.Properties.Lattice.∧-∨-lattice
d_'8743''45''8744''45'lattice_1638 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144
d_'8743''45''8744''45'lattice_1638 :: () -> () -> T_Lattice_1144 -> T_Lattice_1144
d_'8743''45''8744''45'lattice_1638 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_Lattice_1144
du_'8743''45''8744''45'lattice_1638 T_Lattice_1144
v2
du_'8743''45''8744''45'lattice_1638 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144
du_'8743''45''8744''45'lattice_1638 :: T_Lattice_1144 -> T_Lattice_1144
du_'8743''45''8744''45'lattice_1638 T_Lattice_1144
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_740
 -> T_Lattice_1144)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_1144
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740
-> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.C_Lattice'46'constructor_19309
      (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0))
      (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsLattice_740
du_'8743''45''8744''45'isLattice_1636 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._.poset
d_poset_1642 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_poset_1642 :: () -> () -> T_Lattice_1144 -> T_Poset_282
d_poset_1642 ~()
v0 ~()
v1 T_Lattice_1144
v2 = T_Lattice_1144 -> T_Poset_282
du_poset_1642 T_Lattice_1144
v2
du_poset_1642 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_poset_1642 :: T_Lattice_1144 -> T_Poset_282
du_poset_1642 T_Lattice_1144
v0
  = (T_Semilattice_402 -> T_Poset_282) -> AgdaAny -> T_Poset_282
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
du_'8743''45'semilattice_1600 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice._._≤_
d__'8804'__1646 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  AgdaAny -> AgdaAny -> ()
d__'8804'__1646 :: () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny -> ()
d__'8804'__1646 = () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Properties.Lattice.∨-∧-isOrderTheoreticLattice
d_'8744''45''8743''45'isOrderTheoreticLattice_1650 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsLattice_810
d_'8744''45''8743''45'isOrderTheoreticLattice_1650 :: () -> () -> T_Lattice_1144 -> T_IsLattice_810
d_'8744''45''8743''45'isOrderTheoreticLattice_1650 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsLattice_810
du_'8744''45''8743''45'isOrderTheoreticLattice_1650 T_Lattice_1144
v2
du_'8744''45''8743''45'isOrderTheoreticLattice_1650 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsLattice_810
du_'8744''45''8743''45'isOrderTheoreticLattice_1650 :: T_Lattice_1144 -> T_IsLattice_810
du_'8744''45''8743''45'isOrderTheoreticLattice_1650 T_Lattice_1144
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T_Σ_14)
 -> (AgdaAny -> AgdaAny -> T_Σ_14)
 -> T_IsLattice_810)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLattice_810
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> T_Σ_14)
-> T_IsLattice_810
MAlonzo.Code.Relation.Binary.Lattice.C_IsLattice'46'constructor_25911
      ((T_Poset_282 -> T_IsPartialOrder_162) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
         ((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
du_'8743''45'semilattice_1600 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))))
      ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_1694 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemilattice_312 -> AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_2002
         ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
         ((T_Lattice_1144 -> T_IsSemilattice_312) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsSemilattice_312
du_'8743''45'isSemilattice_1598 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
-- Algebra.Properties.Lattice._._._≤_
d__'8804'__1662 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  AgdaAny -> AgdaAny -> ()
d__'8804'__1662 :: () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny -> ()
d__'8804'__1662 = () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Properties.Lattice._.sound
d_sound_1674 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sound_1674 :: ()
-> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sound_1674 ~()
v0 ~()
v1 T_Lattice_1144
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 = T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_1674 T_Lattice_1144
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_sound_1674 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_1674 :: T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_1674 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2 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_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2) AgdaAny
v1
      (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
-> T__IsRelatedTo__26
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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2)
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v1))
            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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v1))
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2))
               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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1
                     ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2))
                  AgdaAny
v1 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_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
forall a b. a -> b
coe T_Lattice_1144
v0))))
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe 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.du_'8743''45'absorbs'45''8744'_792
                     (T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
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'737'_794
                  ((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
forall a b. a -> b
coe T_Lattice_1144
v0))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v1)
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2)
                  ((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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
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_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
forall a b. a -> b
coe T_Lattice_1144
v0))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v1)
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))
-- Algebra.Properties.Lattice._.complete
d_complete_1686 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_complete_1686 :: ()
-> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_complete_1686 ~()
v0 ~()
v1 T_Lattice_1144
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 = T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_1686 T_Lattice_1144
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_complete_1686 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_1686 :: T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_1686 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2 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_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
      ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v1) AgdaAny
v2
      (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
-> T__IsRelatedTo__26
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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v1)
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2))
            AgdaAny
v2
            ((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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2))
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v1))
               AgdaAny
v2
               ((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_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2
                     ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v1))
                  AgdaAny
v2 AgdaAny
v2
                  (((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_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
forall a b. a -> b
coe T_Lattice_1144
v0))))
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
                  ((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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
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_'8744''45'cong'737'_802
                  ((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
forall a b. a -> b
coe T_Lattice_1144
v0))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2)
                  ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
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_'8743''45'comm_770
                     (T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
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_'8744''45'cong'737'_802
               ((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
forall a b. a -> b
coe T_Lattice_1144
v0))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
               ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2)
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))
-- Algebra.Properties.Lattice._.supremum
d_supremum_1694 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_supremum_1694 :: () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny -> T_Σ_14
d_supremum_1694 ~()
v0 ~()
v1 T_Lattice_1144
v2 AgdaAny
v3 AgdaAny
v4 = T_Lattice_1144 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_1694 T_Lattice_1144
v2 AgdaAny
v3 AgdaAny
v4
du_supremum_1694 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_supremum_1694 :: T_Lattice_1144 -> AgdaAny -> AgdaAny -> T_Σ_14
du_supremum_1694 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2
  = (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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_1674 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
         ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2)
         ((T_IsJoinSemilattice_68 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsJoinSemilattice_68 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Lattice.du_x'8804'x'8744'y_96
            ((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
du_'8744''45'semilattice_1624 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
         ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_1674 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
            ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2)
            ((T_IsJoinSemilattice_68 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsJoinSemilattice_68 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Lattice.du_y'8804'x'8744'y_108
               ((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
du_'8744''45'semilattice_1624 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
               (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sound_1674 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)
                 ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v1 AgdaAny
v2)
                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                 ((T_IsJoinSemilattice_68
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                    T_IsJoinSemilattice_68
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Lattice.du_'8744''45'least_122
                    ((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
du_'8744''45'semilattice_1624 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
                    AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_1686 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                    ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_complete_1686 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))))))
-- Algebra.Properties.Lattice.∨-∧-orderTheoreticLattice
d_'8744''45''8743''45'orderTheoreticLattice_1706 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_Lattice_898
d_'8744''45''8743''45'orderTheoreticLattice_1706 :: () -> () -> T_Lattice_1144 -> T_Lattice_898
d_'8744''45''8743''45'orderTheoreticLattice_1706 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_Lattice_898
du_'8744''45''8743''45'orderTheoreticLattice_1706 T_Lattice_1144
v2
du_'8744''45''8743''45'orderTheoreticLattice_1706 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_Lattice_898
du_'8744''45''8743''45'orderTheoreticLattice_1706 :: T_Lattice_1144 -> T_Lattice_898
du_'8744''45''8743''45'orderTheoreticLattice_1706 T_Lattice_1144
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_810
 -> T_Lattice_898)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_898
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_810
-> T_Lattice_898
MAlonzo.Code.Relation.Binary.Lattice.C_Lattice'46'constructor_30305
      (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0))
      (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_Lattice_1144 -> T_IsLattice_810) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> T_IsLattice_810
du_'8744''45''8743''45'isOrderTheoreticLattice_1650 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0))
-- Algebra.Properties.Lattice.∧-idempotent
d_'8743''45'idempotent_1708 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 -> AgdaAny -> AgdaAny
d_'8743''45'idempotent_1708 :: () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny
d_'8743''45'idempotent_1708 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idempotent_1708 T_Lattice_1144
v2
du_'8743''45'idempotent_1708 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idempotent_1708 :: T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idempotent_1708 T_Lattice_1144
v0
  = (T_Lattice_1144 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8743''45'idem_1588 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)
-- Algebra.Properties.Lattice.∨-idempotent
d_'8744''45'idempotent_1710 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 -> AgdaAny -> AgdaAny
d_'8744''45'idempotent_1710 :: () -> () -> T_Lattice_1144 -> AgdaAny -> AgdaAny
d_'8744''45'idempotent_1710 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8744''45'idempotent_1710 T_Lattice_1144
v2
du_'8744''45'idempotent_1710 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8744''45'idempotent_1710 :: T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8744''45'idempotent_1710 T_Lattice_1144
v0
  = (T_Lattice_1144 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny
du_'8744''45'idem_1612 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)
-- Algebra.Properties.Lattice.isOrderTheoreticLattice
d_isOrderTheoreticLattice_1712 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsLattice_810
d_isOrderTheoreticLattice_1712 :: () -> () -> T_Lattice_1144 -> T_IsLattice_810
d_isOrderTheoreticLattice_1712 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_IsLattice_810
du_isOrderTheoreticLattice_1712 T_Lattice_1144
v2
du_isOrderTheoreticLattice_1712 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsLattice_810
du_isOrderTheoreticLattice_1712 :: T_Lattice_1144 -> T_IsLattice_810
du_isOrderTheoreticLattice_1712 T_Lattice_1144
v0
  = (T_Lattice_1144 -> T_IsLattice_810) -> AgdaAny -> T_IsLattice_810
forall a b. a -> b
coe T_Lattice_1144 -> T_IsLattice_810
du_'8744''45''8743''45'isOrderTheoreticLattice_1650 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)
-- Algebra.Properties.Lattice.orderTheoreticLattice
d_orderTheoreticLattice_1714 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_Lattice_898
d_orderTheoreticLattice_1714 :: () -> () -> T_Lattice_1144 -> T_Lattice_898
d_orderTheoreticLattice_1714 ~()
v0 ~()
v1 T_Lattice_1144
v2
  = T_Lattice_1144 -> T_Lattice_898
du_orderTheoreticLattice_1714 T_Lattice_1144
v2
du_orderTheoreticLattice_1714 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_Lattice_898
du_orderTheoreticLattice_1714 :: T_Lattice_1144 -> T_Lattice_898
du_orderTheoreticLattice_1714 T_Lattice_1144
v0
  = (T_Lattice_1144 -> T_Lattice_898) -> AgdaAny -> T_Lattice_898
forall a b. a -> b
coe T_Lattice_1144 -> T_Lattice_898
du_'8744''45''8743''45'orderTheoreticLattice_1706 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)
-- Algebra.Properties.Lattice.replace-equality
d_replace'45'equality_1722 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16) ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144
d_replace'45'equality_1722 :: ()
-> ()
-> T_Lattice_1144
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Equivalence_16)
-> T_Lattice_1144
d_replace'45'equality_1722 ~()
v0 ~()
v1 T_Lattice_1144
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny -> T_Equivalence_16
v4
  = T_Lattice_1144
-> (AgdaAny -> AgdaAny -> T_Equivalence_16) -> T_Lattice_1144
du_replace'45'equality_1722 T_Lattice_1144
v2 AgdaAny -> AgdaAny -> T_Equivalence_16
v4
du_replace'45'equality_1722 ::
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16) ->
  MAlonzo.Code.Algebra.Bundles.T_Lattice_1144
du_replace'45'equality_1722 :: T_Lattice_1144
-> (AgdaAny -> AgdaAny -> T_Equivalence_16) -> T_Lattice_1144
du_replace'45'equality_1722 T_Lattice_1144
v0 AgdaAny -> AgdaAny -> T_Equivalence_16
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLattice_740
 -> T_Lattice_1144)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Lattice_1144
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLattice_740
-> T_Lattice_1144
MAlonzo.Code.Algebra.Bundles.C_Lattice'46'constructor_19309
      (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0))
      (T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0))
      ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsLattice_740)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsLattice_740
MAlonzo.Code.Algebra.Structures.C_IsLattice'46'constructor_20027
         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
            ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
               (\ AgdaAny
v2 ->
                  (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 AgdaAny
v2 AgdaAny
v2))
                    ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> 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
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                          ((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.Bundles.d_isLattice_1168 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
                       AgdaAny
v2)))
            ((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 AgdaAny
v3 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_Lattice_1144 -> T_IsLattice_740) -> AgdaAny -> T_IsLattice_740
forall a b. a -> b
coe T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
                       AgdaAny
v2 AgdaAny
v3
                       ((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_from_36 ((AgdaAny -> AgdaAny -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Equivalence_16
v1 AgdaAny
v2 AgdaAny
v3)) AgdaAny
v4))))
            ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
               (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
                  (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 AgdaAny
v2 AgdaAny
v4))
                    ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                       T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                       (T_IsLattice_740 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_762
                          ((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.Bundles.d_isLattice_1168 (T_Lattice_1144 -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144
v0)))
                       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_from_36 ((AgdaAny -> AgdaAny -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Equivalence_16
v1 AgdaAny
v2 AgdaAny
v3)) AgdaAny
v5)
                       ((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_from_36 ((AgdaAny -> AgdaAny -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Equivalence_16
v1 AgdaAny
v3 AgdaAny
v4))
                          AgdaAny
v6)))))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 AgdaAny
v3 ->
               (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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v3)
                       ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v3 AgdaAny
v2)))
                 ((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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v2 AgdaAny
v3)))
         ((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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0
                          ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v4)
                       ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2
                          ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v3 AgdaAny
v4))))
                 ((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_'8744''45'assoc_766
                    (T_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v2 AgdaAny
v3
                    AgdaAny
v4)))
         ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 ->
               (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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v4)
                       ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v3 AgdaAny
v5)))
                 ((T_IsLattice_740
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsLattice_740
-> AgdaAny
-> AgdaAny
-> 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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                    AgdaAny
v5
                    ((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_from_36 ((AgdaAny -> AgdaAny -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Equivalence_16
v1 AgdaAny
v2 AgdaAny
v3)) AgdaAny
v6)
                    ((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_from_36 ((AgdaAny -> AgdaAny -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Equivalence_16
v1 AgdaAny
v4 AgdaAny
v5)) AgdaAny
v7))))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 AgdaAny
v3 ->
               (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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v3)
                       ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v3 AgdaAny
v2)))
                 ((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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v2 AgdaAny
v3)))
         ((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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0
                          ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v3) AgdaAny
v4)
                       ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v2
                          ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v3 AgdaAny
v4))))
                 ((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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v2 AgdaAny
v3
                    AgdaAny
v4)))
         ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 ->
               (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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v4)
                       ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v3 AgdaAny
v5)))
                 ((T_IsLattice_740
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsLattice_740
-> AgdaAny
-> AgdaAny
-> 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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                    AgdaAny
v5
                    ((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_from_36 ((AgdaAny -> AgdaAny -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Equivalence_16
v1 AgdaAny
v2 AgdaAny
v3)) AgdaAny
v6)
                    ((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_from_36 ((AgdaAny -> AgdaAny -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Equivalence_16
v1 AgdaAny
v4 AgdaAny
v5)) AgdaAny
v7))))
         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
               (\ AgdaAny
v2 AgdaAny
v3 ->
                  (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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2
                             ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v3))
                          AgdaAny
v2))
                    ((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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v2 AgdaAny
v3)))
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
               (\ AgdaAny
v2 AgdaAny
v3 ->
                  (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_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8743'__1166 T_Lattice_1144
v0 AgdaAny
v2
                             ((T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Lattice_1144 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Bundles.d__'8744'__1164 T_Lattice_1144
v0 AgdaAny
v2 AgdaAny
v3))
                          AgdaAny
v2))
                    ((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_Lattice_1144 -> T_IsLattice_740
MAlonzo.Code.Algebra.Bundles.d_isLattice_1168 (T_Lattice_1144 -> T_Lattice_1144
forall a b. a -> b
coe T_Lattice_1144
v0)) AgdaAny
v2 AgdaAny
v3)))))