{-# 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.Data.Product.Relation.Binary.Pointwise.NonDependent 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise
d_Pointwise_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> ()
d_Pointwise_40 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Level_18
d_Pointwise_40 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Level_18
forall a. a
erased
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-reflexive
d_'215''45'reflexive_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'reflexive_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'215''45'reflexive_54 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9
                        ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T_Σ_14
v14 T_Σ_14
v15
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'reflexive_54 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T_Σ_14
v14 T_Σ_14
v15
du_'215''45'reflexive_54 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'reflexive_54 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'reflexive_54 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Σ_14
v2 T_Σ_14
v3
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v4 ->
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-refl
d_'215''45'refl_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'refl_60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
d_'215''45'refl_60 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny
v9 T_Σ_14
v10
  = (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'215''45'refl_60 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny
v9 T_Σ_14
v10
du_'215''45'refl_60 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'refl_60 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'215''45'refl_60 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_Σ_14
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
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-irreflexive₁
d_'215''45'irreflexive'8321'_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'215''45'irreflexive'8321'_66 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_'215''45'irreflexive'8321'_66 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-irreflexive₂
d_'215''45'irreflexive'8322'_74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'215''45'irreflexive'8322'_74 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_'215''45'irreflexive'8322'_74 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-symmetric
d_'215''45'symmetric_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'symmetric_82 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'215''45'symmetric_82 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T_Σ_14
v10
                        T_Σ_14
v11
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'symmetric_82 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T_Σ_14
v10 T_Σ_14
v11
du_'215''45'symmetric_82 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'symmetric_82 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'symmetric_82 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Σ_14
v2 T_Σ_14
v3
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v4 ->
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-transitive
d_'215''45'transitive_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'transitive_88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'215''45'transitive_88 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T_Σ_14
v10
                         T_Σ_14
v11 T_Σ_14
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'transitive_88 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T_Σ_14
v10 T_Σ_14
v11 T_Σ_14
v12
du_'215''45'transitive_88 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'transitive_88 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'transitive_88 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Σ_14
v2 T_Σ_14
v3 T_Σ_14
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip_198
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4)))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v5 AgdaAny
v6 ->
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4))))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-antisymmetric
d_'215''45'antisymmetric_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'antisymmetric_94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'215''45'antisymmetric_94 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9
                            ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T_Σ_14
v14 T_Σ_14
v15
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'antisymmetric_94 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T_Σ_14
v14 T_Σ_14
v15
du_'215''45'antisymmetric_94 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'antisymmetric_94 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'antisymmetric_94 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Σ_14
v2 T_Σ_14
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip_198
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3)))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v4 AgdaAny
v5 ->
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-asymmetric₁
d_'215''45'asymmetric'8321'_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'215''45'asymmetric'8321'_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_'215''45'asymmetric'8321'_100 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-asymmetric₂
d_'215''45'asymmetric'8322'_108 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'215''45'asymmetric'8322'_108 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_'215''45'asymmetric'8322'_108 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-respectsʳ
d_'215''45'respects'691'_116 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'respects'691'_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'215''45'respects'691'_116 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8
                             ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T_Σ_14
v14 T_Σ_14
v15 T_Σ_14
v16
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'respects'691'_116 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T_Σ_14
v14 T_Σ_14
v15 T_Σ_14
v16
du_'215''45'respects'691'_116 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'respects'691'_116 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'respects'691'_116 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Σ_14
v2 T_Σ_14
v3 T_Σ_14
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip_198
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4)))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v5 AgdaAny
v6 ->
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4))))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-respectsˡ
d_'215''45'respects'737'_122 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'respects'737'_122 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'215''45'respects'737'_122 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8
                             ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T_Σ_14
v14 T_Σ_14
v15 T_Σ_14
v16
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'respects'737'_122 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 T_Σ_14
v14 T_Σ_14
v15 T_Σ_14
v16
du_'215''45'respects'737'_122 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'respects'737'_122 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'respects'737'_122 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Σ_14
v2 T_Σ_14
v3 T_Σ_14
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip_198
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4)))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v5 AgdaAny
v6 ->
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3))
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4))))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-respects₂
d_'215''45'respects'8322'_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'respects'8322'_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'215''45'respects'8322'_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8
                              ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'215''45'respects'8322'_128
du_'215''45'respects'8322'_128 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'respects'8322'_128 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'215''45'respects'8322'_128
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip_198
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'respects'691'_116)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'respects'737'_122))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-total
d_'215''45'total_130 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'215''45'total_130 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_Σ_14
-> T_Σ_14
-> T__'8846'__30
d_'215''45'total_130 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8846'__30
v9 AgdaAny -> AgdaAny -> T__'8846'__30
v10 T_Σ_14
v11
                     T_Σ_14
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_Σ_14
-> T_Σ_14
-> T__'8846'__30
du_'215''45'total_130 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T__'8846'__30
v9 AgdaAny -> AgdaAny -> T__'8846'__30
v10 T_Σ_14
v11 T_Σ_14
v12
du_'215''45'total_130 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'215''45'total_130 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> T_Σ_14
-> T_Σ_14
-> T__'8846'__30
du_'215''45'total_130 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T__'8846'__30
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 T_Σ_14
v3 T_Σ_14
v4
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v5 AgdaAny
v6
        -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
               -> let v9 :: AgdaAny
v9 = (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v1 AgdaAny
v5 AgdaAny
v7 in
                  AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    (let v10 :: AgdaAny
v10 = (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny
v6 AgdaAny
v8 in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v9 of
                          MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v11
                            -> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v10 of
                                 MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v12
                                   -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                                        ((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
forall a b. a -> b
coe AgdaAny
v11)
                                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))
                                 MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v12
                                   -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                                        ((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)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v7 AgdaAny
v11) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))
                                 T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                          MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v11
                            -> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v10 of
                                 MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v12
                                   -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                                        ((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)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v7 AgdaAny
v5 AgdaAny
v11) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))
                                 MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v12
                                   -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                                        ((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
forall a b. a -> b
coe AgdaAny
v11)
                                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))
                                 T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                          T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
             T_Σ_14
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-decidable
d_'215''45'decidable_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'215''45'decidable_222 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_Σ_14
-> T_Σ_14
-> T_Dec_20
d_'215''45'decidable_222 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> T_Dec_20
v8 AgdaAny -> AgdaAny -> T_Dec_20
v9 T_Σ_14
v10
                         T_Σ_14
v11
  = (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Σ_14 -> T_Dec_20
du_'215''45'decidable_222 AgdaAny -> AgdaAny -> T_Dec_20
v8 AgdaAny -> AgdaAny -> T_Dec_20
v9 T_Σ_14
v10 T_Σ_14
v11
du_'215''45'decidable_222 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'215''45'decidable_222 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Σ_14 -> T_Dec_20
du_'215''45'decidable_222 AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 T_Σ_14
v2 T_Σ_14
v3
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
        -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
               -> (T_Dec_20 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84
                    ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v4 AgdaAny
v6) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v5 AgdaAny
v7)
             T_Σ_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-isEquivalence
d_'215''45'isEquivalence_236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_'215''45'isEquivalence_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_IsEquivalence_28
-> T_IsEquivalence_28
d_'215''45'isEquivalence_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 T_IsEquivalence_28
v8 T_IsEquivalence_28
v9
  = T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'215''45'isEquivalence_236 T_IsEquivalence_28
v8 T_IsEquivalence_28
v9
du_'215''45'isEquivalence_236 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
du_'215''45'isEquivalence_236 :: T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'215''45'isEquivalence_236 T_IsEquivalence_28
v0 T_IsEquivalence_28
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
      (((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'215''45'refl_60
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0))
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'symmetric_82
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0))
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'transitive_88
         ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0))
         ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-isDecEquivalence
d_'215''45'isDecEquivalence_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48
d_'215''45'isDecEquivalence_250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecEquivalence_48
-> T_IsDecEquivalence_48
-> T_IsDecEquivalence_48
d_'215''45'isDecEquivalence_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 T_IsDecEquivalence_48
v8
                                T_IsDecEquivalence_48
v9
  = T_IsDecEquivalence_48
-> T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_'215''45'isDecEquivalence_250 T_IsDecEquivalence_48
v8 T_IsDecEquivalence_48
v9
du_'215''45'isDecEquivalence_250 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48
du_'215''45'isDecEquivalence_250 :: T_IsDecEquivalence_48
-> T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_'215''45'isDecEquivalence_250 T_IsDecEquivalence_48
v0 T_IsDecEquivalence_48
v1
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_48)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_48
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Structures.C_constructor_70
      ((T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'215''45'isEquivalence_236
         ((T_IsDecEquivalence_48 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_54
            (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v0))
         ((T_IsDecEquivalence_48 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_54
            (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v1)))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Σ_14 -> T_Dec_20
du_'215''45'decidable_222
         ((T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__56 (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v0))
         ((T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__56 (T_IsDecEquivalence_48 -> AgdaAny
forall a b. a -> b
coe T_IsDecEquivalence_48
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-isPreorder
d_'215''45'isPreorder_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_'215''45'isPreorder_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPreorder_76
-> T_IsPreorder_76
-> T_IsPreorder_76
d_'215''45'isPreorder_260 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9
                          ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11 T_IsPreorder_76
v12 T_IsPreorder_76
v13
  = T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76
du_'215''45'isPreorder_260 T_IsPreorder_76
v12 T_IsPreorder_76
v13
du_'215''45'isPreorder_260 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_'215''45'isPreorder_260 :: T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76
du_'215''45'isPreorder_260 T_IsPreorder_76
v0 T_IsPreorder_76
v1
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      ((T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'215''45'isEquivalence_236
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0))
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'reflexive_54
         ((T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0))
         ((T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_88 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'transitive_88
         ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v0))
         ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90 (T_IsPreorder_76 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_76
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-isPartialOrder
d_'215''45'isPartialOrder_274 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
d_'215''45'isPartialOrder_274 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsPartialOrder_248
-> T_IsPartialOrder_248
-> T_IsPartialOrder_248
d_'215''45'isPartialOrder_274 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8
                              ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11 T_IsPartialOrder_248
v12 T_IsPartialOrder_248
v13
  = T_IsPartialOrder_248
-> T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_'215''45'isPartialOrder_274 T_IsPartialOrder_248
v12 T_IsPartialOrder_248
v13
du_'215''45'isPartialOrder_274 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
du_'215''45'isPartialOrder_274 :: T_IsPartialOrder_248
-> T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_'215''45'isPartialOrder_274 T_IsPartialOrder_248
v0 T_IsPartialOrder_248
v1
  = (T_IsPreorder_76
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
      T_IsPreorder_76
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.C_constructor_294
      ((T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76
du_'215''45'isPreorder_260
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v0))
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'antisymmetric_94
         ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v0))
         ((T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258 (T_IsPartialOrder_248 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_248
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-isStrictPartialOrder
d_'215''45'isStrictPartialOrder_288 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
d_'215''45'isStrictPartialOrder_288 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370
d_'215''45'isStrictPartialOrder_288 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7
                                    ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11 T_IsStrictPartialOrder_370
v12 T_IsStrictPartialOrder_370
v13
  = T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'215''45'isStrictPartialOrder_288 T_IsStrictPartialOrder_370
v12 T_IsStrictPartialOrder_370
v13
du_'215''45'isStrictPartialOrder_288 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
du_'215''45'isStrictPartialOrder_288 :: T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'215''45'isStrictPartialOrder_288 T_IsStrictPartialOrder_370
v0 T_IsStrictPartialOrder_370
v1
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.C_constructor_412
      ((T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'215''45'isEquivalence_236
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v1)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
du_'215''45'transitive_88
         ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386 (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386 (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v1)))
      ((T_Σ_14 -> T_Σ_14 -> T_Σ_14) -> T_Σ_14 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'215''45'respects'8322'_128
         (T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
            (T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         (T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
            (T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-setoid
d_'215''45'setoid_304 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_'215''45'setoid_304 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
d_'215''45'setoid_304 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_46
v4 T_Setoid_46
v5
  = T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du_'215''45'setoid_304 T_Setoid_46
v4 T_Setoid_46
v5
du_'215''45'setoid_304 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du_'215''45'setoid_304 :: T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du_'215''45'setoid_304 T_Setoid_46
v0 T_Setoid_46
v1
  = (T_IsEquivalence_28 -> T_Setoid_46) -> AgdaAny -> T_Setoid_46
forall a b. a -> b
coe
      T_IsEquivalence_28 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_84
      ((T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsEquivalence_28
du_'215''45'isEquivalence_236
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-decSetoid
d_'215''45'decSetoid_314 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
d_'215''45'decSetoid_314 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_DecSetoid_90
-> T_DecSetoid_90
-> T_DecSetoid_90
d_'215''45'decSetoid_314 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_DecSetoid_90
v4 T_DecSetoid_90
v5
  = T_DecSetoid_90 -> T_DecSetoid_90 -> T_DecSetoid_90
du_'215''45'decSetoid_314 T_DecSetoid_90
v4 T_DecSetoid_90
v5
du_'215''45'decSetoid_314 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
du_'215''45'decSetoid_314 :: T_DecSetoid_90 -> T_DecSetoid_90 -> T_DecSetoid_90
du_'215''45'decSetoid_314 T_DecSetoid_90
v0 T_DecSetoid_90
v1
  = (T_IsDecEquivalence_48 -> T_DecSetoid_90)
-> AgdaAny -> T_DecSetoid_90
forall a b. a -> b
coe
      T_IsDecEquivalence_48 -> T_DecSetoid_90
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_134
      ((T_IsDecEquivalence_48
 -> T_IsDecEquivalence_48 -> T_IsDecEquivalence_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecEquivalence_48
-> T_IsDecEquivalence_48 -> T_IsDecEquivalence_48
du_'215''45'isDecEquivalence_250
         ((T_DecSetoid_90 -> T_IsDecEquivalence_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_90 -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_106
            (T_DecSetoid_90 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90
v0))
         ((T_DecSetoid_90 -> T_IsDecEquivalence_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_90 -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_106
            (T_DecSetoid_90 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-preorder
d_'215''45'preorder_324 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_'215''45'preorder_324 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Preorder_142
-> T_Preorder_142
-> T_Preorder_142
d_'215''45'preorder_324 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 T_Preorder_142
v6 T_Preorder_142
v7
  = T_Preorder_142 -> T_Preorder_142 -> T_Preorder_142
du_'215''45'preorder_324 T_Preorder_142
v6 T_Preorder_142
v7
du_'215''45'preorder_324 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_'215''45'preorder_324 :: T_Preorder_142 -> T_Preorder_142 -> T_Preorder_142
du_'215''45'preorder_324 T_Preorder_142
v0 T_Preorder_142
v1
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> T_IsPreorder_76 -> T_IsPreorder_76
du_'215''45'isPreorder_260
         ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0))
         ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-poset
d_'215''45'poset_334 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_'215''45'poset_334 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Poset_492
-> T_Poset_492
-> T_Poset_492
d_'215''45'poset_334 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 T_Poset_492
v6 T_Poset_492
v7
  = T_Poset_492 -> T_Poset_492 -> T_Poset_492
du_'215''45'poset_334 T_Poset_492
v6 T_Poset_492
v7
du_'215''45'poset_334 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_'215''45'poset_334 :: T_Poset_492 -> T_Poset_492 -> T_Poset_492
du_'215''45'poset_334 T_Poset_492
v0 T_Poset_492
v1
  = (T_IsPartialOrder_248 -> T_Poset_492) -> AgdaAny -> T_Poset_492
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_588
      ((T_IsPartialOrder_248
 -> T_IsPartialOrder_248 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248
-> T_IsPartialOrder_248 -> T_IsPartialOrder_248
du_'215''45'isPartialOrder_274
         ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514 (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v0))
         ((T_Poset_492 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
            (T_Poset_492 -> AgdaAny
forall a b. a -> b
coe T_Poset_492
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent.×-strictPartialOrder
d_'215''45'strictPartialOrder_344 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
d_'215''45'strictPartialOrder_344 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_760
-> T_StrictPartialOrder_760
-> T_StrictPartialOrder_760
d_'215''45'strictPartialOrder_344 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 T_StrictPartialOrder_760
v6 T_StrictPartialOrder_760
v7
  = T_StrictPartialOrder_760
-> T_StrictPartialOrder_760 -> T_StrictPartialOrder_760
du_'215''45'strictPartialOrder_344 T_StrictPartialOrder_760
v6 T_StrictPartialOrder_760
v7
du_'215''45'strictPartialOrder_344 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
du_'215''45'strictPartialOrder_344 :: T_StrictPartialOrder_760
-> T_StrictPartialOrder_760 -> T_StrictPartialOrder_760
du_'215''45'strictPartialOrder_344 T_StrictPartialOrder_760
v0 T_StrictPartialOrder_760
v1
  = (T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760)
-> AgdaAny -> T_StrictPartialOrder_760
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_842
      ((T_IsStrictPartialOrder_370
 -> T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'215''45'isStrictPartialOrder_288
         ((T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_782
            (T_StrictPartialOrder_760 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_760
v0))
         ((T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_782
            (T_StrictPartialOrder_760 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_760
v1)))
-- Data.Product.Relation.Binary.Pointwise.NonDependent._×ₛ_
d__'215''8347'__354 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d__'215''8347'__354 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
d__'215''8347'__354 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du__'215''8347'__354
du__'215''8347'__354 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du__'215''8347'__354 :: T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du__'215''8347'__354 = (T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46)
-> T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46 -> T_Setoid_46 -> T_Setoid_46
du_'215''45'setoid_304
-- Data.Product.Relation.Binary.Pointwise.NonDependent.≡×≡⇒≡
d_'8801''215''8801''8658''8801'_356 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8801''215''8801''8658''8801'_356 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_'8801''215''8801''8658''8801'_356 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Relation.Binary.Pointwise.NonDependent.≡⇒≡×≡
d_'8801''8658''8801''215''8801'_358 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8801''8658''8801''215''8801'_358 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T_Σ_14
d_'8801''8658''8801''215''8801'_358 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5 ~T__'8801'__12
v6
  = T_Σ_14
du_'8801''8658''8801''215''8801'_358
du_'8801''8658''8801''215''8801'_358 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8801''8658''8801''215''8801'_358 :: T_Σ_14
du_'8801''8658''8801''215''8801'_358
  = (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 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise-≡↔≡
d_Pointwise'45''8801''8596''8801'_360 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_Pointwise'45''8801''8596''8801'_360 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_Pointwise'45''8801''8596''8801'_360 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122
du_Pointwise'45''8801''8596''8801'_360
du_Pointwise'45''8801''8596''8801'_360 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_Pointwise'45''8801''8596''8801'_360 :: T_Inverse_2122
du_Pointwise'45''8801''8596''8801'_360
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_2122)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_2122
MAlonzo.Code.Function.Bundles.C_constructor_2220 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'8801''8658''8801''215''8801'_358)
      ((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
forall a. a
erased
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'8801''8658''8801''215''8801'_358)))