{-# 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.Relation.Unary.Properties 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
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.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Relation.Unary.Properties.∅?
d_'8709''63'_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8709''63'_22 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T_Dec_20
d_'8709''63'_22 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny
v2 = T_Dec_20
du_'8709''63'_22
du_'8709''63'_22 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8709''63'_22 :: T_Dec_20
du_'8709''63'_22
  = (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
      (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
      (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
-- Relation.Unary.Properties.∅-Empty
d_'8709''45'Empty_24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8709''45'Empty_24 :: T_Level_18
-> T_Level_18 -> AgdaAny -> T_Irrelevant_20 -> T_Irrelevant_20
d_'8709''45'Empty_24 = T_Level_18
-> T_Level_18 -> AgdaAny -> T_Irrelevant_20 -> T_Irrelevant_20
forall a. a
erased
-- Relation.Unary.Properties.∁∅-Universal
d_'8705''8709''45'Universal_28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8705''8709''45'Universal_28 :: T_Level_18
-> T_Level_18 -> AgdaAny -> T_Irrelevant_20 -> T_Irrelevant_20
d_'8705''8709''45'Universal_28 = T_Level_18
-> T_Level_18 -> AgdaAny -> T_Irrelevant_20 -> T_Irrelevant_20
forall a. a
erased
-- Relation.Unary.Properties.U?
d_U'63'_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_U'63'_34 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T_Dec_20
d_U'63'_34 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny
v2 = T_Dec_20
du_U'63'_34
du_U'63'_34 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_U'63'_34 :: T_Dec_20
du_U'63'_34
  = (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
      (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
      ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
         (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Relation.Unary.Properties.U-Universal
d_U'45'Universal_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_U'45'Universal_36 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T_Level_18
d_U'45'Universal_36 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny
v2 = T_Level_18
du_U'45'Universal_36
du_U'45'Universal_36 :: MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
du_U'45'Universal_36 :: T_Level_18
du_U'45'Universal_36 = T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
-- Relation.Unary.Properties.∁U-Empty
d_'8705'U'45'Empty_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  (MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8705'U'45'Empty_40 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> (T_Level_18 -> T_Irrelevant_20)
-> T_Irrelevant_20
d_'8705'U'45'Empty_40 = T_Level_18
-> T_Level_18
-> AgdaAny
-> (T_Level_18 -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Unary.Properties.∅-⊆
d_'8709''45''8838'_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 -> AgdaAny
d_'8709''45''8838'_48 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
d_'8709''45''8838'_48 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~T_Irrelevant_20
v5
  = AgdaAny
du_'8709''45''8838'_48
du_'8709''45''8838'_48 :: AgdaAny
du_'8709''45''8838'_48 :: AgdaAny
du_'8709''45''8838'_48 = AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊆-U
d_'8838''45'U_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_'8838''45'U_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_'8838''45'U_54 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 = T_Level_18
du_'8838''45'U_54
du_'8838''45'U_54 :: MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
du_'8838''45'U_54 :: T_Level_18
du_'8838''45'U_54 = T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
-- Relation.Unary.Properties.⊆-refl
d_'8838''45'refl_58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8838''45'refl_58 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''45'refl_58 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 AgdaAny
v5
  = AgdaAny -> AgdaAny
du_'8838''45'refl_58 AgdaAny
v5
du_'8838''45'refl_58 :: AgdaAny -> AgdaAny
du_'8838''45'refl_58 :: AgdaAny -> AgdaAny
du_'8838''45'refl_58 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Unary.Properties.⊆-reflexive
d_'8838''45'reflexive_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8838''45'reflexive_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''45'reflexive_62 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 T_Σ_14
v6 AgdaAny
v7
  = T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'reflexive_62 T_Σ_14
v6 AgdaAny
v7
du_'8838''45'reflexive_62 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'reflexive_62 :: T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'reflexive_62 T_Σ_14
v0 AgdaAny
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v1
      T_Σ_14
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊆-trans
d_'8838''45'trans_68 ::
  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 -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8838''45'trans_68 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''45'trans_68 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'trans_68 AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_'8838''45'trans_68 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'trans_68 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'trans_68 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
-- Relation.Unary.Properties.⊆-antisym
d_'8838''45'antisym_76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8838''45'antisym_76 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
d_'8838''45'antisym_76 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Level_18
v4
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8838''45'antisym_76
du_'8838''45'antisym_76 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8838''45'antisym_76 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8838''45'antisym_76
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
-- Relation.Unary.Properties.⊆-min
d_'8838''45'min_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 -> AgdaAny
d_'8838''45'min_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
d_'8838''45'min_78 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 = (AgdaAny -> T_Level_18) -> AgdaAny -> T_Irrelevant_20 -> AgdaAny
du_'8838''45'min_78
du_'8838''45'min_78 ::
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 -> AgdaAny
du_'8838''45'min_78 :: (AgdaAny -> T_Level_18) -> AgdaAny -> T_Irrelevant_20 -> AgdaAny
du_'8838''45'min_78 AgdaAny -> T_Level_18
v0 AgdaAny
v1 T_Irrelevant_20
v2 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
du_'8709''45''8838'_48
-- Relation.Unary.Properties.⊆-max
d_'8838''45'max_80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_'8838''45'max_80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_'8838''45'max_80 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 = (AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny -> T_Level_18
du_'8838''45'max_80
du_'8838''45'max_80 ::
  (AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
du_'8838''45'max_80 :: (AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny -> T_Level_18
du_'8838''45'max_80 AgdaAny -> T_Level_18
v0 AgdaAny
v1 AgdaAny
v2 = T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
du_'8838''45'U_54
-- Relation.Unary.Properties.⊂⇒⊆
d_'8834''8658''8838'_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8834''8658''8838'_82 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8834''8658''8838'_82 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 T_Σ_14
v6
  = T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8834''8658''8838'_82 T_Σ_14
v6
du_'8834''8658''8838'_82 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8834''8658''8838'_82 :: T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8834''8658''8838'_82 T_Σ_14
v0
  = (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v0)
-- Relation.Unary.Properties.⊂-trans
d_'8834''45'trans_84 ::
  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 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''45'trans_84 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8834''45'trans_84 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Σ_14
v8 T_Σ_14
v9
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'trans_84 T_Σ_14
v8 T_Σ_14
v9
du_'8834''45'trans_84 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''45'trans_84 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'trans_84 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
               -> (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
v6 AgdaAny
v7 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4 AgdaAny
v6 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v6 AgdaAny
v7)))
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5 (\ AgdaAny
v7 AgdaAny
v8 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v7 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6 AgdaAny
v7 AgdaAny
v8))))
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂-⊆-trans
d_'8834''45''8838''45'trans_100 ::
  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 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''45''8838''45'trans_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
d_'8834''45''8838''45'trans_100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Σ_14
v8
                                AgdaAny -> AgdaAny -> AgdaAny
v9
  = T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8834''45''8838''45'trans_100 T_Σ_14
v8 AgdaAny -> AgdaAny -> AgdaAny
v9
du_'8834''45''8838''45'trans_100 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''45''8838''45'trans_100 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8834''45''8838''45'trans_100 T_Σ_14
v0 AgdaAny -> AgdaAny -> AgdaAny
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> (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
v4 AgdaAny
v5 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v4 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v4 AgdaAny
v5)))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 (\ AgdaAny
v5 AgdaAny
v6 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4 AgdaAny
v5 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v5 AgdaAny
v6))))
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊆-⊂-trans
d_'8838''45''8834''45'trans_114 ::
  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 -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8838''45''8834''45'trans_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
d_'8838''45''8834''45'trans_114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny
v8
                                T_Σ_14
v9
  = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'8838''45''8834''45'trans_114 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Σ_14
v9
du_'8838''45''8834''45'trans_114 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8838''45''8834''45'trans_114 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'8838''45''8834''45'trans_114 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> (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
v4 AgdaAny
v5 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v5)))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 (\ AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4 AgdaAny
v5 AgdaAny
v6))))
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂-respʳ-≐
d_'8834''45'resp'691''45''8784'_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''45'resp'691''45''8784'_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8834''45'resp'691''45''8784'_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 T_Σ_14
v7
                                    T_Σ_14
v8
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'resp'691''45''8784'_128 T_Σ_14
v7 T_Σ_14
v8
du_'8834''45'resp'691''45''8784'_128 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''45'resp'691''45''8784'_128 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'resp'691''45''8784'_128 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> (T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8834''45''8838''45'trans_100 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂-respˡ-≐
d_'8834''45'resp'737''45''8784'_134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''45'resp'737''45''8784'_134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8834''45'resp'737''45''8784'_134 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 T_Σ_14
v7
                                    T_Σ_14
v8
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'resp'737''45''8784'_134 T_Σ_14
v7 T_Σ_14
v8
du_'8834''45'resp'737''45''8784'_134 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''45'resp'737''45''8784'_134 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'resp'737''45''8784'_134 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> ((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'8838''45''8834''45'trans_114 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1)
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂-resp-≐
d_'8834''45'resp'45''8784'_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''45'resp'45''8784'_140 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Σ_14
d_'8834''45'resp'45''8784'_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2
  = T_Σ_14
du_'8834''45'resp'45''8784'_140
du_'8834''45'resp'45''8784'_140 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''45'resp'45''8784'_140 :: T_Σ_14
du_'8834''45'resp'45''8784'_140
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_Σ_14 -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'resp'691''45''8784'_128 AgdaAny
v3 AgdaAny
v4)
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_Σ_14 -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'resp'737''45''8784'_134 AgdaAny
v3 AgdaAny
v4)
-- Relation.Unary.Properties.⊂-irrefl
d_'8834''45'irrefl_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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.Data.Irrelevant.T_Irrelevant_20
d_'8834''45'irrefl_142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_'8834''45'irrefl_142 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Unary.Properties.⊂-antisym
d_'8834''45'antisym_148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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_'8834''45'antisym_148 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8834''45'antisym_148 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 T_Σ_14
v5 T_Σ_14
v6
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'antisym_148 T_Σ_14
v5 T_Σ_14
v6
du_'8834''45'antisym_148 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''45'antisym_148 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''45'antisym_148 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
               -> ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8838''45'antisym_76 AgdaAny
v2 AgdaAny
v4
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂-asym
d_'8834''45'asym_154 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Data.Irrelevant.T_Irrelevant_20
d_'8834''45'asym_154 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_'8834''45'asym_154 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Unary.Properties.∅-⊆′
d_'8709''45''8838''8242'_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 -> AgdaAny
d_'8709''45''8838''8242'_160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
d_'8709''45''8838''8242'_160 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
forall a. a
erased
-- Relation.Unary.Properties.⊆′-U
d_'8838''8242''45'U_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_'8838''8242''45'U_164 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_'8838''8242''45'U_164 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5
  = T_Level_18
du_'8838''8242''45'U_164
du_'8838''8242''45'U_164 ::
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
du_'8838''8242''45'U_164 :: T_Level_18
du_'8838''8242''45'U_164
  = T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
-- Relation.Unary.Properties.⊆′-refl
d_'8838''8242''45'refl_166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8838''8242''45'refl_166 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''8242''45'refl_166 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 AgdaAny
v5
  = AgdaAny -> AgdaAny
du_'8838''8242''45'refl_166 AgdaAny
v5
du_'8838''8242''45'refl_166 :: AgdaAny -> AgdaAny
du_'8838''8242''45'refl_166 :: AgdaAny -> AgdaAny
du_'8838''8242''45'refl_166 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Unary.Properties.⊆′-reflexive
d_'8838''8242''45'reflexive_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8838''8242''45'reflexive_172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''8242''45'reflexive_172 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 T_Σ_14
v6
  = T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'reflexive_172 T_Σ_14
v6
du_'8838''8242''45'reflexive_172 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'reflexive_172 :: T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'reflexive_172 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Σ_14
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊆′-trans
d_'8838''8242''45'trans_178 ::
  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 -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8838''8242''45'trans_178 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''8242''45'trans_178 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny
v9
                            AgdaAny
v10 AgdaAny
v11
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_'8838''8242''45'trans_178 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
-- Relation.Unary.Properties.⊆′-antisym
d_'8838''8242''45'antisym_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8838''8242''45'antisym_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
d_'8838''8242''45'antisym_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Level_18
v4
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8838''8242''45'antisym_188
du_'8838''8242''45'antisym_188 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8838''8242''45'antisym_188 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8838''8242''45'antisym_188
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
-- Relation.Unary.Properties.⊆′-min
d_'8838''8242''45'min_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 -> AgdaAny
d_'8838''8242''45'min_190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
d_'8838''8242''45'min_190 T_Level_18
v0 ~T_Level_18
v1 T_Level_18
v2
  = T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
du_'8838''8242''45'min_190 T_Level_18
v0 T_Level_18
v2
du_'8838''8242''45'min_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 -> AgdaAny
du_'8838''8242''45'min_190 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
du_'8838''8242''45'min_190 T_Level_18
v0 T_Level_18
v1
  = (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> (AgdaAny -> T_Level_18)
 -> AgdaAny
 -> T_Irrelevant_20
 -> AgdaAny)
-> T_Level_18
-> AgdaAny
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
forall a b. a -> b
coe T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Irrelevant_20
-> AgdaAny
d_'8709''45''8838''8242'_160 T_Level_18
v0 AgdaAny
forall a. a
erased T_Level_18
v1
-- Relation.Unary.Properties.⊆′-max
d_'8838''8242''45'max_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_'8838''8242''45'max_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_'8838''8242''45'max_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 = (AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny -> T_Level_18
du_'8838''8242''45'max_192
du_'8838''8242''45'max_192 ::
  (AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
du_'8838''8242''45'max_192 :: (AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny -> T_Level_18
du_'8838''8242''45'max_192 AgdaAny -> T_Level_18
v0 AgdaAny
v1 AgdaAny
v2 = T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
du_'8838''8242''45'U_164
-- Relation.Unary.Properties.⊂′⇒⊆′
d_'8834''8242''8658''8838''8242'_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_'8834''8242''8658''8838''8242'_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8834''8242''8658''8838''8242'_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 T_Σ_14
v6
  = T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8834''8242''8658''8838''8242'_194 T_Σ_14
v6
du_'8834''8242''8658''8838''8242'_194 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8834''8242''8658''8838''8242'_194 :: T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8834''8242''8658''8838''8242'_194 T_Σ_14
v0
  = (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v0)
-- Relation.Unary.Properties.⊂′-trans
d_'8834''8242''45'trans_196 ::
  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 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''8242''45'trans_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8834''8242''45'trans_196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Σ_14
v8 T_Σ_14
v9
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'trans_196 T_Σ_14
v8 T_Σ_14
v9
du_'8834''8242''45'trans_196 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''8242''45'trans_196 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'trans_196 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
               -> (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 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                       (\ AgdaAny
v6 ->
                          AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5 (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂′-⊆′-trans
d_'8834''8242''45''8838''8242''45'trans_208 ::
  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 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''8242''45''8838''8242''45'trans_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
d_'8834''8242''45''8838''8242''45'trans_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5
                                            ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Σ_14
v8 AgdaAny -> AgdaAny -> AgdaAny
v9
  = T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8834''8242''45''8838''8242''45'trans_208 T_Σ_14
v8 AgdaAny -> AgdaAny -> AgdaAny
v9
du_'8834''8242''45''8838''8242''45'trans_208 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''8242''45''8838''8242''45'trans_208 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8834''8242''45''8838''8242''45'trans_208 T_Σ_14
v0 AgdaAny -> AgdaAny -> AgdaAny
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> (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 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v4 ->
                   AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))))
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊆′-⊂′-trans
d_'8838''8242''45''8834''8242''45'trans_218 ::
  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 -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8838''8242''45''8834''8242''45'trans_218 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
d_'8838''8242''45''8834''8242''45'trans_218 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5
                                            ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Σ_14
v9
  = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'8838''8242''45''8834''8242''45'trans_218 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Σ_14
v9
du_'8838''8242''45''8834''8242''45'trans_218 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8838''8242''45''8834''8242''45'trans_218 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'8838''8242''45''8834''8242''45'trans_218 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> (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 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v4 ->
                   AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''45'trans_178 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0))))
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂′-respʳ-≐′
d_'8834''8242''45'resp'691''45''8784''8242'_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''8242''45'resp'691''45''8784''8242'_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8834''8242''45'resp'691''45''8784''8242'_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4
                                                ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 T_Σ_14
v7 T_Σ_14
v8
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'resp'691''45''8784''8242'_228 T_Σ_14
v7 T_Σ_14
v8
du_'8834''8242''45'resp'691''45''8784''8242'_228 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''8242''45'resp'691''45''8784''8242'_228 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'resp'691''45''8784''8242'_228 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> (T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8834''8242''45''8838''8242''45'trans_208 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂′-respˡ-≐′
d_'8834''8242''45'resp'737''45''8784''8242'_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''8242''45'resp'737''45''8784''8242'_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8834''8242''45'resp'737''45''8784''8242'_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4
                                                ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 T_Σ_14
v7 T_Σ_14
v8
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'resp'737''45''8784''8242'_234 T_Σ_14
v7 T_Σ_14
v8
du_'8834''8242''45'resp'737''45''8784''8242'_234 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''8242''45'resp'737''45''8784''8242'_234 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'resp'737''45''8784''8242'_234 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> ((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
du_'8838''8242''45''8834''8242''45'trans_218 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1)
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊂′-resp-≐′
d_'8834''8242''45'resp'45''8784''8242'_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''8242''45'resp'45''8784''8242'_240 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Σ_14
d_'8834''8242''45'resp'45''8784''8242'_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2
  = T_Σ_14
du_'8834''8242''45'resp'45''8784''8242'_240
du_'8834''8242''45'resp'45''8784''8242'_240 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''8242''45'resp'45''8784''8242'_240 :: T_Σ_14
du_'8834''8242''45'resp'45''8784''8242'_240
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_Σ_14 -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'resp'691''45''8784''8242'_228 AgdaAny
v3 AgdaAny
v4)
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_Σ_14 -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'resp'737''45''8784''8242'_234 AgdaAny
v3 AgdaAny
v4)
-- Relation.Unary.Properties.⊂′-irrefl
d_'8834''8242''45'irrefl_242 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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.Data.Irrelevant.T_Irrelevant_20
d_'8834''8242''45'irrefl_242 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
d_'8834''8242''45'irrefl_242 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Unary.Properties.⊂′-antisym
d_'8834''8242''45'antisym_248 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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_'8834''8242''45'antisym_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8834''8242''45'antisym_248 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 T_Σ_14
v5 T_Σ_14
v6
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'antisym_248 T_Σ_14
v5 T_Σ_14
v6
du_'8834''8242''45'antisym_248 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''8242''45'antisym_248 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8834''8242''45'antisym_248 T_Σ_14
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
               -> ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14
du_'8838''8242''45'antisym_188 AgdaAny
v2 AgdaAny
v4
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊆⇒⊆′
d_'8838''8658''8838''8242'_254 ::
  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 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8838''8658''8838''8242'_254 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''8658''8838''8242'_254 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8658''8838''8242'_254 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
du_'8838''8658''8838''8242'_254 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8658''8838''8242'_254 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8658''8838''8242'_254 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2
-- Relation.Unary.Properties.⊆′⇒⊆
d_'8838''8242''8658''8838'_260 ::
  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 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8838''8242''8658''8838'_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''8242''8658''8838'_260 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''8658''8838'_260 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
du_'8838''8242''8658''8838'_260 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''8658''8838'_260 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''8658''8838'_260 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2
-- Relation.Unary.Properties.⊂⇒⊂′
d_'8834''8658''8834''8242'_266 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''8658''8834''8242'_266 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_'8834''8658''8834''8242'_266 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5
  = T_Σ_14 -> T_Σ_14
du_'8834''8658''8834''8242'_266
du_'8834''8658''8834''8242'_266 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''8658''8834''8242'_266 :: T_Σ_14 -> T_Σ_14
du_'8834''8658''8834''8242'_266
  = ((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 -> AgdaAny -> AgdaAny
du_'8838''8658''8838''8242'_254)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 ->
            AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 (((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''8658''8838'_260 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
-- Relation.Unary.Properties.⊂′⇒⊂
d_'8834''8242''8658''8834'_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8834''8242''8658''8834'_270 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_'8834''8242''8658''8834'_270 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5
  = T_Σ_14 -> T_Σ_14
du_'8834''8242''8658''8834'_270
du_'8834''8242''8658''8834'_270 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8834''8242''8658''8834'_270 :: T_Σ_14 -> T_Σ_14
du_'8834''8242''8658''8834'_270
  = ((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 -> AgdaAny -> AgdaAny
du_'8838''8242''8658''8838'_260)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 ->
            AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 (((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8658''8838''8242'_254 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
-- Relation.Unary.Properties.≐-refl
d_'8784''45'refl_274 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8784''45'refl_274 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> (AgdaAny -> T_Level_18) -> T_Σ_14
d_'8784''45'refl_274 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 = T_Σ_14
du_'8784''45'refl_274
du_'8784''45'refl_274 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8784''45'refl_274 :: T_Σ_14
du_'8784''45'refl_274
  = (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
v0 AgdaAny
v1 -> AgdaAny
v1))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> AgdaAny
v1))
-- Relation.Unary.Properties.≐-sym
d_'8784''45'sym_276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8784''45'sym_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_'8784''45'sym_276 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 = T_Σ_14 -> T_Σ_14
du_'8784''45'sym_276
du_'8784''45'sym_276 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8784''45'sym_276 :: T_Σ_14 -> T_Σ_14
du_'8784''45'sym_276
  = (T_Σ_14 -> T_Σ_14) -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370
-- Relation.Unary.Properties.≐-trans
d_'8784''45'trans_278 ::
  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 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8784''45'trans_278 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8784''45'trans_278 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8784''45'trans_278
du_'8784''45'trans_278 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8784''45'trans_278 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8784''45'trans_278
  = ((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) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip'8242'_312
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 AgdaAny
v2 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0 AgdaAny
v2 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 AgdaAny
v2 AgdaAny
v3)))
-- Relation.Unary.Properties.≐′-refl
d_'8784''8242''45'refl_292 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8784''8242''45'refl_292 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> (AgdaAny -> T_Level_18) -> T_Σ_14
d_'8784''8242''45'refl_292 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3
  = T_Σ_14
du_'8784''8242''45'refl_292
du_'8784''8242''45'refl_292 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8784''8242''45'refl_292 :: T_Σ_14
du_'8784''8242''45'refl_292
  = (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
v0 AgdaAny
v1 -> AgdaAny
v1))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> AgdaAny
v1))
-- Relation.Unary.Properties.≐′-sym
d_'8784''8242''45'sym_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8784''8242''45'sym_298 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_'8784''8242''45'sym_298 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5
  = T_Σ_14 -> T_Σ_14
du_'8784''8242''45'sym_298
du_'8784''8242''45'sym_298 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8784''8242''45'sym_298 :: T_Σ_14 -> T_Σ_14
du_'8784''8242''45'sym_298
  = (T_Σ_14 -> T_Σ_14) -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370
-- Relation.Unary.Properties.≐′-trans
d_'8784''8242''45'trans_300 ::
  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 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8784''8242''45'trans_300 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_'8784''8242''45'trans_300 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7
  = T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8784''8242''45'trans_300
du_'8784''8242''45'trans_300 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8784''8242''45'trans_300 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_'8784''8242''45'trans_300
  = ((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) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip'8242'_312
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 AgdaAny
v2 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0 AgdaAny
v2 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 AgdaAny
v2 AgdaAny
v3)))
-- Relation.Unary.Properties.≐⇒≐′
d_'8784''8658''8784''8242'_318 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8784''8658''8784''8242'_318 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_'8784''8658''8784''8242'_318 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5
  = T_Σ_14 -> T_Σ_14
du_'8784''8658''8784''8242'_318
du_'8784''8658''8784''8242'_318 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8784''8658''8784''8242'_318 :: T_Σ_14 -> T_Σ_14
du_'8784''8658''8784''8242'_318
  = ((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 -> AgdaAny -> AgdaAny
du_'8838''8658''8838''8242'_254)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8658''8838''8242'_254))
-- Relation.Unary.Properties.≐′⇒≐
d_'8784''8242''8658''8784'_320 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8784''8242''8658''8784'_320 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_'8784''8242''8658''8784'_320 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5
  = T_Σ_14 -> T_Σ_14
du_'8784''8242''8658''8784'_320
du_'8784''8242''8658''8784'_320 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8784''8242''8658''8784'_320 :: T_Σ_14 -> T_Σ_14
du_'8784''8242''8658''8784'_320
  = ((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 -> AgdaAny -> AgdaAny
du_'8838''8242''8658''8838'_260)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''8242''8658''8838'_260))
-- Relation.Unary.Properties.∁?
d_'8705''63'_324 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8705''63'_324 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_20)
-> AgdaAny
-> T_Dec_20
d_'8705''63'_324 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 AgdaAny -> T_Dec_20
v4 AgdaAny
v5 = (AgdaAny -> T_Dec_20) -> AgdaAny -> T_Dec_20
du_'8705''63'_324 AgdaAny -> T_Dec_20
v4 AgdaAny
v5
du_'8705''63'_324 ::
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8705''63'_324 :: (AgdaAny -> T_Dec_20) -> AgdaAny -> T_Dec_20
du_'8705''63'_324 AgdaAny -> T_Dec_20
v0 AgdaAny
v1
  = (T_Dec_20 -> T_Dec_20) -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_'172''63'_70
      ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v1)
-- Relation.Unary.Properties._∪?_
d__'8746''63'__334 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8746''63'__334 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> AgdaAny
-> T_Dec_20
d__'8746''63'__334 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> T_Dec_20
v6 AgdaAny -> T_Dec_20
v7 AgdaAny
v8
  = (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> AgdaAny -> T_Dec_20
du__'8746''63'__334 AgdaAny -> T_Dec_20
v6 AgdaAny -> T_Dec_20
v7 AgdaAny
v8
du__'8746''63'__334 ::
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'8746''63'__334 :: (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> AgdaAny -> T_Dec_20
du__'8746''63'__334 AgdaAny -> T_Dec_20
v0 AgdaAny -> T_Dec_20
v1 AgdaAny
v2
  = (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__'8846''45'dec__86
      ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v2) ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1 AgdaAny
v2)
-- Relation.Unary.Properties._∩?_
d__'8745''63'__346 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8745''63'__346 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> AgdaAny
-> T_Dec_20
d__'8745''63'__346 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> T_Dec_20
v6 AgdaAny -> T_Dec_20
v7 AgdaAny
v8
  = (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> AgdaAny -> T_Dec_20
du__'8745''63'__346 AgdaAny -> T_Dec_20
v6 AgdaAny -> T_Dec_20
v7 AgdaAny
v8
du__'8745''63'__346 ::
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'8745''63'__346 :: (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> AgdaAny -> T_Dec_20
du__'8745''63'__346 AgdaAny -> T_Dec_20
v0 AgdaAny -> T_Dec_20
v1 AgdaAny
v2
  = (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__76
      ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v2) ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1 AgdaAny
v2)
-- Relation.Unary.Properties._×?_
d__'215''63'__358 ::
  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 ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'215''63'__358 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T_Σ_14
-> T_Dec_20
d__'215''63'__358 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 AgdaAny -> T_Dec_20
v8 AgdaAny -> T_Dec_20
v9 T_Σ_14
v10
  = (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Dec_20
du__'215''63'__358 AgdaAny -> T_Dec_20
v8 AgdaAny -> T_Dec_20
v9 T_Σ_14
v10
du__'215''63'__358 ::
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'215''63'__358 :: (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Dec_20
du__'215''63'__358 AgdaAny -> T_Dec_20
v0 AgdaAny -> T_Dec_20
v1 T_Σ_14
v2
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
        -> (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__76
             ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v3) ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1 AgdaAny
v4)
      T_Σ_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties._⊙?_
d__'8857''63'__372 ::
  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 ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8857''63'__372 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T_Σ_14
-> T_Dec_20
d__'8857''63'__372 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 AgdaAny -> T_Dec_20
v8 AgdaAny -> T_Dec_20
v9 T_Σ_14
v10
  = (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Dec_20
du__'8857''63'__372 AgdaAny -> T_Dec_20
v8 AgdaAny -> T_Dec_20
v9 T_Σ_14
v10
du__'8857''63'__372 ::
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'8857''63'__372 :: (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> T_Σ_14 -> T_Dec_20
du__'8857''63'__372 AgdaAny -> T_Dec_20
v0 AgdaAny -> T_Dec_20
v1 T_Σ_14
v2
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
        -> (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__'8846''45'dec__86
             ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v3) ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1 AgdaAny
v4)
      T_Σ_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties._⊎?_
d__'8846''63'__386 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8846''63'__386 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T__'8846'__30
-> T_Dec_20
d__'8846''63'__386 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 AgdaAny -> T_Dec_20
v7 AgdaAny -> T_Dec_20
v8 T__'8846'__30
v9
  = (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> T__'8846'__30 -> T_Dec_20
du__'8846''63'__386 AgdaAny -> T_Dec_20
v7 AgdaAny -> T_Dec_20
v8 T__'8846'__30
v9
du__'8846''63'__386 ::
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'8846''63'__386 :: (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> T__'8846'__30 -> T_Dec_20
du__'8846''63'__386 AgdaAny -> T_Dec_20
v0 AgdaAny -> T_Dec_20
v1 T__'8846'__30
v2
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v3 -> (AgdaAny -> T_Dec_20) -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v3
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v3 -> (AgdaAny -> T_Dec_20) -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1 AgdaAny
v3
      T__'8846'__30
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties._~?
d__'126''63'_402 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'126''63'_402 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (T_Σ_14 -> T_Level_18)
-> (T_Σ_14 -> T_Dec_20)
-> T_Σ_14
-> T_Dec_20
d__'126''63'_402 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Σ_14 -> T_Level_18
v5 T_Σ_14 -> T_Dec_20
v6 T_Σ_14
v7
  = (T_Σ_14 -> T_Dec_20) -> T_Σ_14 -> T_Dec_20
du__'126''63'_402 T_Σ_14 -> T_Dec_20
v6 T_Σ_14
v7
du__'126''63'_402 ::
  (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'126''63'_402 :: (T_Σ_14 -> T_Dec_20) -> T_Σ_14 -> T_Dec_20
du__'126''63'_402 T_Σ_14 -> T_Dec_20
v0 T_Σ_14
v1
  = (T_Σ_14 -> T_Dec_20) -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_Σ_14 -> T_Dec_20
v0 ((T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1))
-- Relation.Unary.Properties.U-irrelevant
d_U'45'irrelevant_406 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_U'45'irrelevant_406 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> T_Level_18
-> T_Level_18
-> T__'8801'__12
d_U'45'irrelevant_406 = T_Level_18
-> T_Level_18
-> AgdaAny
-> T_Level_18
-> T_Level_18
-> T__'8801'__12
forall a. a
erased
-- Relation.Unary.Properties.∁-irrelevant
d_'8705''45'irrelevant_414 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8705''45'irrelevant_414 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> T__'8801'__12
d_'8705''45'irrelevant_414 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> T__'8801'__12
forall a. a
erased