{-# 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.Function.Related 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.Primitive
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Function.Bijection
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Function.Injection
import qualified MAlonzo.Code.Function.Inverse
import qualified MAlonzo.Code.Function.LeftInverse
import qualified MAlonzo.Code.Function.Surjection
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Related._←_
d__'8592'__12 :: p -> p -> p -> p -> ()
d__'8592'__12 p
a0 p
a1 p
a2 p
a3 = ()
newtype T__'8592'__12 = C_lam_26 (AgdaAny -> AgdaAny)
-- Function.Related._←_.app-←
d_app'45''8592'_24 :: T__'8592'__12 -> AgdaAny -> AgdaAny
d_app'45''8592'_24 :: T__'8592'__12 -> AgdaAny -> AgdaAny
d_app'45''8592'_24 T__'8592'__12
v0
  = case T__'8592'__12 -> T__'8592'__12
forall a b. a -> b
coe T__'8592'__12
v0 of
      C_lam_26 AgdaAny -> AgdaAny
v1 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1
      T__'8592'__12
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related._↢_
d__'8610'__36 :: p -> p -> p -> p -> ()
d__'8610'__36 p
a0 p
a1 p
a2 p
a3 = ()
newtype T__'8610'__36
  = C_lam_50 MAlonzo.Code.Function.Injection.T_Injection_88
-- Function.Related._↢_.app-↢
d_app'45''8610'_48 ::
  T__'8610'__36 -> MAlonzo.Code.Function.Injection.T_Injection_88
d_app'45''8610'_48 :: T__'8610'__36 -> T_Injection_88
d_app'45''8610'_48 T__'8610'__36
v0
  = case T__'8610'__36 -> T__'8610'__36
forall a b. a -> b
coe T__'8610'__36
v0 of
      C_lam_50 T_Injection_88
v1 -> T_Injection_88 -> T_Injection_88
forall a b. a -> b
coe T_Injection_88
v1
      T__'8610'__36
_ -> T_Injection_88
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Kind
d_Kind_52 :: ()
d_Kind_52 = ()
data T_Kind_52
  = C_implication_54 | C_reverse'45'implication_56 |
    C_equivalence_58 | C_injection_60 | C_reverse'45'injection_62 |
    C_left'45'inverse_64 | C_surjection_66 | C_bijection_68
-- Function.Related._∼[_]_
d__'8764''91'_'93'__74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Kind_52 -> () -> ()
d__'8764''91'_'93'__74 :: () -> () -> () -> T_Kind_52 -> () -> ()
d__'8764''91'_'93'__74 = () -> () -> () -> T_Kind_52 -> () -> ()
forall a. a
erased
-- Function.Related.Related
d_Related_112 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> () -> ()
d_Related_112 :: T_Kind_52 -> () -> () -> () -> () -> ()
d_Related_112 = T_Kind_52 -> () -> () -> () -> () -> ()
forall a. a
erased
-- Function.Related.↔⇒
d_'8596''8658'_130 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny
d_'8596''8658'_130 :: T_Kind_52 -> () -> () -> () -> () -> T_Inverse_58 -> AgdaAny
d_'8596''8658'_130 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 = T_Kind_52 -> T_Inverse_58 -> AgdaAny
du_'8596''8658'_130 T_Kind_52
v0
du_'8596''8658'_130 ::
  T_Kind_52 -> MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny
du_'8596''8658'_130 :: T_Kind_52 -> T_Inverse_58 -> AgdaAny
du_'8596''8658'_130 T_Kind_52
v0
  = case T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0 of
      T_Kind_52
C_implication_54
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Inverse_58 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_to_78 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_52
C_reverse'45'implication_56
        -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226 (((AgdaAny -> AgdaAny) -> T__'8592'__12) -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8592'__12
C_lam_26)
             ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v1 ->
                   T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                     ((T_Inverse_58 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_from_80 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
      T_Kind_52
C_equivalence_58
        -> (AgdaAny -> AgdaAny) -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                let v2 :: t
v2
                      = (T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                          T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98
                          (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                             T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_Surjection_54 -> T_Equivalence_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Surjection_54 -> T_Equivalence_16
MAlonzo.Code.Function.Surjection.du_equivalence_92
                     ((T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Surjection_54
MAlonzo.Code.Function.Bijection.du_surjection_100 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
      T_Kind_52
C_injection_60
        -> (AgdaAny -> AgdaAny) -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                (T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88
MAlonzo.Code.Function.LeftInverse.du_injection_184
                  (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                  ((T_Inverse_58 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_LeftInverse_82
MAlonzo.Code.Function.Inverse.du_left'45'inverse_90 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_52
C_reverse'45'injection_62
        -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226 ((T_Injection_88 -> T__'8610'__36) -> AgdaAny
forall a b. a -> b
coe T_Injection_88 -> T__'8610'__36
C_lam_50)
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v1 ->
                   (T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88
MAlonzo.Code.Function.LeftInverse.du_injection_184
                     (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                     ((T_Inverse_58 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Inverse_58 -> T_LeftInverse_82
MAlonzo.Code.Function.Inverse.du_left'45'inverse_90
                        ((T_Inverse_58 -> T_Inverse_58) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_sym_226 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))))
      T_Kind_52
C_left'45'inverse_64
        -> (T_Inverse_58 -> T_LeftInverse_82) -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_LeftInverse_82
MAlonzo.Code.Function.Inverse.du_left'45'inverse_90
      T_Kind_52
C_surjection_66
        -> (AgdaAny -> AgdaAny) -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                (T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Bijection_64 -> T_Surjection_54
MAlonzo.Code.Function.Bijection.du_surjection_100
                  ((T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98
                     (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_52
C_bijection_68 -> (AgdaAny -> AgdaAny) -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Kind_52
_ -> T_Inverse_58 -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.≡⇒
d_'8801''8658'_140 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'8801''8658'_140 :: T_Kind_52 -> () -> () -> () -> T__'8801'__12 -> AgdaAny
d_'8801''8658'_140 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~T__'8801'__12
v4 = T_Kind_52 -> AgdaAny
du_'8801''8658'_140 T_Kind_52
v0
du_'8801''8658'_140 :: T_Kind_52 -> AgdaAny
du_'8801''8658'_140 :: T_Kind_52 -> AgdaAny
du_'8801''8658'_140 T_Kind_52
v0
  = (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_52 -> T_Inverse_58 -> AgdaAny
du_'8596''8658'_130 T_Kind_52
v0
      ((T_Setoid_44 -> T_Inverse_58) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_id_186
         (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250))
-- Function.Related.Symmetric-kind
d_Symmetric'45'kind_142 :: ()
d_Symmetric'45'kind_142 = ()
data T_Symmetric'45'kind_142 = C_equivalence_144 | C_bijection_146
-- Function.Related.⌊_⌋
d_'8970'_'8971'_148 :: T_Symmetric'45'kind_142 -> T_Kind_52
d_'8970'_'8971'_148 :: T_Symmetric'45'kind_142 -> T_Kind_52
d_'8970'_'8971'_148 T_Symmetric'45'kind_142
v0
  = case T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0 of
      T_Symmetric'45'kind_142
C_equivalence_144 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_equivalence_58
      T_Symmetric'45'kind_142
C_bijection_146 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_bijection_68
      T_Symmetric'45'kind_142
_ -> T_Kind_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Forward-kind
d_Forward'45'kind_150 :: ()
d_Forward'45'kind_150 = ()
data T_Forward'45'kind_150
  = C_implication_152 | C_equivalence_154 | C_injection_156 |
    C_left'45'inverse_158 | C_surjection_160 | C_bijection_162
-- Function.Related.⌊_⌋→
d_'8970'_'8971''8594'_164 :: T_Forward'45'kind_150 -> T_Kind_52
d_'8970'_'8971''8594'_164 :: T_Forward'45'kind_150 -> T_Kind_52
d_'8970'_'8971''8594'_164 T_Forward'45'kind_150
v0
  = case T_Forward'45'kind_150 -> T_Forward'45'kind_150
forall a b. a -> b
coe T_Forward'45'kind_150
v0 of
      T_Forward'45'kind_150
C_implication_152 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_implication_54
      T_Forward'45'kind_150
C_equivalence_154 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_equivalence_58
      T_Forward'45'kind_150
C_injection_156 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_injection_60
      T_Forward'45'kind_150
C_left'45'inverse_158 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_left'45'inverse_64
      T_Forward'45'kind_150
C_surjection_160 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_surjection_66
      T_Forward'45'kind_150
C_bijection_162 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_bijection_68
      T_Forward'45'kind_150
_ -> T_Kind_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.⇒→
d_'8658''8594'_176 ::
  T_Forward'45'kind_150 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_'8658''8594'_176 :: T_Forward'45'kind_150
-> () -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_'8658''8594'_176 T_Forward'45'kind_150
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 = T_Forward'45'kind_150 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8594'_176 T_Forward'45'kind_150
v0
du_'8658''8594'_176 ::
  T_Forward'45'kind_150 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8594'_176 :: T_Forward'45'kind_150 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8594'_176 T_Forward'45'kind_150
v0
  = case T_Forward'45'kind_150 -> T_Forward'45'kind_150
forall a b. a -> b
coe T_Forward'45'kind_150
v0 of
      T_Forward'45'kind_150
C_implication_152 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Forward'45'kind_150
C_equivalence_154
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Forward'45'kind_150
C_injection_156
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Injection_88 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Injection_88 -> T_Π_16
MAlonzo.Code.Function.Injection.d_to_106 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Forward'45'kind_150
C_left'45'inverse_158
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_to_102 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Forward'45'kind_150
C_surjection_160
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Surjection_54 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Surjection_54 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_to_72 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Forward'45'kind_150
C_bijection_162
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Inverse_58 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_to_78 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Forward'45'kind_150
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Backward-kind
d_Backward'45'kind_178 :: ()
d_Backward'45'kind_178 = ()
data T_Backward'45'kind_178
  = C_reverse'45'implication_180 | C_equivalence_182 |
    C_reverse'45'injection_184 | C_left'45'inverse_186 |
    C_surjection_188 | C_bijection_190
-- Function.Related.⌊_⌋←
d_'8970'_'8971''8592'_192 :: T_Backward'45'kind_178 -> T_Kind_52
d_'8970'_'8971''8592'_192 :: T_Backward'45'kind_178 -> T_Kind_52
d_'8970'_'8971''8592'_192 T_Backward'45'kind_178
v0
  = case T_Backward'45'kind_178 -> T_Backward'45'kind_178
forall a b. a -> b
coe T_Backward'45'kind_178
v0 of
      T_Backward'45'kind_178
C_reverse'45'implication_180 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_reverse'45'implication_56
      T_Backward'45'kind_178
C_equivalence_182 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_equivalence_58
      T_Backward'45'kind_178
C_reverse'45'injection_184 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_reverse'45'injection_62
      T_Backward'45'kind_178
C_left'45'inverse_186 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_left'45'inverse_64
      T_Backward'45'kind_178
C_surjection_188 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_surjection_66
      T_Backward'45'kind_178
C_bijection_190 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_bijection_68
      T_Backward'45'kind_178
_ -> T_Kind_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.⇒←
d_'8658''8592'_204 ::
  T_Backward'45'kind_178 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_'8658''8592'_204 :: T_Backward'45'kind_178
-> () -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_'8658''8592'_204 T_Backward'45'kind_178
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 = T_Backward'45'kind_178 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8592'_204 T_Backward'45'kind_178
v0
du_'8658''8592'_204 ::
  T_Backward'45'kind_178 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8592'_204 :: T_Backward'45'kind_178 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8592'_204 T_Backward'45'kind_178
v0
  = case T_Backward'45'kind_178 -> T_Backward'45'kind_178
forall a b. a -> b
coe T_Backward'45'kind_178
v0 of
      T_Backward'45'kind_178
C_reverse'45'implication_180
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T__'8592'__12 -> AgdaAny -> AgdaAny
d_app'45''8592'_24 (AgdaAny -> T__'8592'__12
forall a b. a -> b
coe AgdaAny
v1))
      T_Backward'45'kind_178
C_equivalence_182
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Backward'45'kind_178
C_reverse'45'injection_184
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Injection_88 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe
                     T_Injection_88 -> T_Π_16
MAlonzo.Code.Function.Injection.d_to_106
                     ((T__'8610'__36 -> T_Injection_88) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8610'__36 -> T_Injection_88
d_app'45''8610'_48 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
      T_Backward'45'kind_178
C_left'45'inverse_186
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_from_104 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Backward'45'kind_178
C_surjection_188
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Surjective_18 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe
                     T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
                     ((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
      T_Backward'45'kind_178
C_bijection_190
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  ((T_Inverse_58 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_from_80 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Backward'45'kind_178
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Equivalence-kind
d_Equivalence'45'kind_206 :: ()
d_Equivalence'45'kind_206 = ()
data T_Equivalence'45'kind_206
  = C_equivalence_208 | C_left'45'inverse_210 | C_surjection_212 |
    C_bijection_214
-- Function.Related.⌊_⌋⇔
d_'8970'_'8971''8660'_216 :: T_Equivalence'45'kind_206 -> T_Kind_52
d_'8970'_'8971''8660'_216 :: T_Equivalence'45'kind_206 -> T_Kind_52
d_'8970'_'8971''8660'_216 T_Equivalence'45'kind_206
v0
  = case T_Equivalence'45'kind_206 -> T_Equivalence'45'kind_206
forall a b. a -> b
coe T_Equivalence'45'kind_206
v0 of
      T_Equivalence'45'kind_206
C_equivalence_208 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_equivalence_58
      T_Equivalence'45'kind_206
C_left'45'inverse_210 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_left'45'inverse_64
      T_Equivalence'45'kind_206
C_surjection_212 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_surjection_66
      T_Equivalence'45'kind_206
C_bijection_214 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_bijection_68
      T_Equivalence'45'kind_206
_ -> T_Kind_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.⇒⇔
d_'8658''8660'_228 ::
  T_Equivalence'45'kind_206 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () -> AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_'8658''8660'_228 :: T_Equivalence'45'kind_206
-> () -> () -> () -> () -> AgdaAny -> T_Equivalence_16
d_'8658''8660'_228 T_Equivalence'45'kind_206
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 = T_Equivalence'45'kind_206 -> AgdaAny -> T_Equivalence_16
du_'8658''8660'_228 T_Equivalence'45'kind_206
v0
du_'8658''8660'_228 ::
  T_Equivalence'45'kind_206 ->
  AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_'8658''8660'_228 :: T_Equivalence'45'kind_206 -> AgdaAny -> T_Equivalence_16
du_'8658''8660'_228 T_Equivalence'45'kind_206
v0
  = case T_Equivalence'45'kind_206 -> T_Equivalence'45'kind_206
forall a b. a -> b
coe T_Equivalence'45'kind_206
v0 of
      T_Equivalence'45'kind_206
C_equivalence_208 -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Equivalence'45'kind_206
C_left'45'inverse_210
        -> (T_LeftInverse_82 -> T_Equivalence_16)
-> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe T_LeftInverse_82 -> T_Equivalence_16
MAlonzo.Code.Function.LeftInverse.du_equivalence_186
      T_Equivalence'45'kind_206
C_surjection_212
        -> (T_Surjection_54 -> T_Equivalence_16)
-> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe T_Surjection_54 -> T_Equivalence_16
MAlonzo.Code.Function.Surjection.du_equivalence_92
      T_Equivalence'45'kind_206
C_bijection_214
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                let v2 :: t
v2
                      = (T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                          T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98
                          (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                             T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                          (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_Surjection_54 -> T_Equivalence_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Surjection_54 -> T_Equivalence_16
MAlonzo.Code.Function.Surjection.du_equivalence_92
                     ((T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_64 -> T_Surjection_54
MAlonzo.Code.Function.Bijection.du_surjection_100 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
      T_Equivalence'45'kind_206
_ -> AgdaAny -> T_Equivalence_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.⇔⌊_⌋
d_'8660''8970'_'8971'_230 ::
  T_Symmetric'45'kind_142 -> T_Equivalence'45'kind_206
d_'8660''8970'_'8971'_230 :: T_Symmetric'45'kind_142 -> T_Equivalence'45'kind_206
d_'8660''8970'_'8971'_230 T_Symmetric'45'kind_142
v0
  = case T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0 of
      T_Symmetric'45'kind_142
C_equivalence_144 -> T_Equivalence'45'kind_206 -> T_Equivalence'45'kind_206
forall a b. a -> b
coe T_Equivalence'45'kind_206
C_equivalence_208
      T_Symmetric'45'kind_142
C_bijection_146 -> T_Equivalence'45'kind_206 -> T_Equivalence'45'kind_206
forall a b. a -> b
coe T_Equivalence'45'kind_206
C_bijection_214
      T_Symmetric'45'kind_142
_ -> T_Equivalence'45'kind_206
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.→⌊_⌋
d_'8594''8970'_'8971'_232 ::
  T_Equivalence'45'kind_206 -> T_Forward'45'kind_150
d_'8594''8970'_'8971'_232 :: T_Equivalence'45'kind_206 -> T_Forward'45'kind_150
d_'8594''8970'_'8971'_232 T_Equivalence'45'kind_206
v0
  = case T_Equivalence'45'kind_206 -> T_Equivalence'45'kind_206
forall a b. a -> b
coe T_Equivalence'45'kind_206
v0 of
      T_Equivalence'45'kind_206
C_equivalence_208 -> T_Forward'45'kind_150 -> T_Forward'45'kind_150
forall a b. a -> b
coe T_Forward'45'kind_150
C_equivalence_154
      T_Equivalence'45'kind_206
C_left'45'inverse_210 -> T_Forward'45'kind_150 -> T_Forward'45'kind_150
forall a b. a -> b
coe T_Forward'45'kind_150
C_left'45'inverse_158
      T_Equivalence'45'kind_206
C_surjection_212 -> T_Forward'45'kind_150 -> T_Forward'45'kind_150
forall a b. a -> b
coe T_Forward'45'kind_150
C_surjection_160
      T_Equivalence'45'kind_206
C_bijection_214 -> T_Forward'45'kind_150 -> T_Forward'45'kind_150
forall a b. a -> b
coe T_Forward'45'kind_150
C_bijection_162
      T_Equivalence'45'kind_206
_ -> T_Forward'45'kind_150
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.←⌊_⌋
d_'8592''8970'_'8971'_234 ::
  T_Equivalence'45'kind_206 -> T_Backward'45'kind_178
d_'8592''8970'_'8971'_234 :: T_Equivalence'45'kind_206 -> T_Backward'45'kind_178
d_'8592''8970'_'8971'_234 T_Equivalence'45'kind_206
v0
  = case T_Equivalence'45'kind_206 -> T_Equivalence'45'kind_206
forall a b. a -> b
coe T_Equivalence'45'kind_206
v0 of
      T_Equivalence'45'kind_206
C_equivalence_208 -> T_Backward'45'kind_178 -> T_Backward'45'kind_178
forall a b. a -> b
coe T_Backward'45'kind_178
C_equivalence_182
      T_Equivalence'45'kind_206
C_left'45'inverse_210 -> T_Backward'45'kind_178 -> T_Backward'45'kind_178
forall a b. a -> b
coe T_Backward'45'kind_178
C_left'45'inverse_186
      T_Equivalence'45'kind_206
C_surjection_212 -> T_Backward'45'kind_178 -> T_Backward'45'kind_178
forall a b. a -> b
coe T_Backward'45'kind_178
C_surjection_188
      T_Equivalence'45'kind_206
C_bijection_214 -> T_Backward'45'kind_178 -> T_Backward'45'kind_178
forall a b. a -> b
coe T_Backward'45'kind_178
C_bijection_190
      T_Equivalence'45'kind_206
_ -> T_Backward'45'kind_178
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related._op
d__op_236 :: T_Kind_52 -> T_Kind_52
d__op_236 :: T_Kind_52 -> T_Kind_52
d__op_236 T_Kind_52
v0
  = case T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0 of
      T_Kind_52
C_implication_54 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_reverse'45'implication_56
      T_Kind_52
C_reverse'45'implication_56 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_implication_54
      T_Kind_52
C_equivalence_58 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0
      T_Kind_52
C_injection_60 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_reverse'45'injection_62
      T_Kind_52
C_reverse'45'injection_62 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_injection_60
      T_Kind_52
C_left'45'inverse_64 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_surjection_66
      T_Kind_52
C_surjection_66 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
C_left'45'inverse_64
      T_Kind_52
C_bijection_68 -> T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0
      T_Kind_52
_ -> T_Kind_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.reverse
d_reverse_248 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny
d_reverse_248 :: T_Kind_52 -> () -> () -> () -> () -> AgdaAny -> AgdaAny
d_reverse_248 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 = T_Kind_52 -> AgdaAny -> AgdaAny
du_reverse_248 T_Kind_52
v0
du_reverse_248 :: T_Kind_52 -> AgdaAny -> AgdaAny
du_reverse_248 :: T_Kind_52 -> AgdaAny -> AgdaAny
du_reverse_248 T_Kind_52
v0
  = case T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0 of
      T_Kind_52
C_implication_54 -> ((AgdaAny -> AgdaAny) -> T__'8592'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8592'__12
C_lam_26
      T_Kind_52
C_reverse'45'implication_56
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T__'8592'__12 -> AgdaAny -> AgdaAny
d_app'45''8592'_24 (AgdaAny -> T__'8592'__12
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_52
C_equivalence_58
        -> (T_Equivalence_16 -> T_Equivalence_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_sym_100
      T_Kind_52
C_injection_60 -> (T_Injection_88 -> T__'8610'__36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_88 -> T__'8610'__36
C_lam_50
      T_Kind_52
C_reverse'45'injection_62
        -> (AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T__'8610'__36 -> T_Injection_88
d_app'45''8610'_48 (AgdaAny -> T__'8610'__36
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_52
C_left'45'inverse_64
        -> (T_LeftInverse_82 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.du_fromRightInverse_106
      T_Kind_52
C_surjection_66
        -> (T_Surjection_54 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_LeftInverse_82
MAlonzo.Code.Function.Surjection.du_right'45'inverse_82
      T_Kind_52
C_bijection_68 -> (T_Inverse_58 -> T_Inverse_58) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_sym_226
      T_Kind_52
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.K-refl
d_K'45'refl_254 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny
d_K'45'refl_254 :: T_Kind_52 -> () -> () -> AgdaAny
d_K'45'refl_254 T_Kind_52
v0 ~()
v1 ~()
v2 = T_Kind_52 -> AgdaAny
du_K'45'refl_254 T_Kind_52
v0
du_K'45'refl_254 :: T_Kind_52 -> AgdaAny
du_K'45'refl_254 :: T_Kind_52 -> AgdaAny
du_K'45'refl_254 T_Kind_52
v0
  = case T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0 of
      T_Kind_52
C_implication_54 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Kind_52
C_reverse'45'implication_56 -> ((AgdaAny -> AgdaAny) -> T__'8592'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8592'__12
C_lam_26 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
      T_Kind_52
C_equivalence_58 -> T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_id_66
      T_Kind_52
C_injection_60 -> T_Injection_88 -> AgdaAny
forall a b. a -> b
coe T_Injection_88
MAlonzo.Code.Function.Injection.du_id_152
      T_Kind_52
C_reverse'45'injection_62
        -> (T_Injection_88 -> T__'8610'__36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_88 -> T__'8610'__36
C_lam_50 (T_Injection_88 -> AgdaAny
forall a b. a -> b
coe T_Injection_88
MAlonzo.Code.Function.Injection.du_id_152)
      T_Kind_52
C_left'45'inverse_64
        -> (T_Setoid_44 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Setoid_44 -> T_LeftInverse_82
MAlonzo.Code.Function.LeftInverse.du_id_256
             (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
      T_Kind_52
C_surjection_66
        -> (T_Setoid_44 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Setoid_44 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.du_id_168
             (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
      T_Kind_52
C_bijection_68
        -> (T_Setoid_44 -> T_Inverse_58) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Setoid_44 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_id_186
             (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
      T_Kind_52
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.K-reflexive
d_K'45'reflexive_260 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_K'45'reflexive_260 :: T_Kind_52 -> () -> () -> () -> T__'8801'__12 -> AgdaAny
d_K'45'reflexive_260 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~T__'8801'__12
v4 = T_Kind_52 -> AgdaAny
du_K'45'reflexive_260 T_Kind_52
v0
du_K'45'reflexive_260 :: T_Kind_52 -> AgdaAny
du_K'45'reflexive_260 :: T_Kind_52 -> AgdaAny
du_K'45'reflexive_260 T_Kind_52
v0 = (T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
du_K'45'refl_254 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0)
-- Function.Related.K-trans
d_K'45'trans_270 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_K'45'trans_270 :: T_Kind_52
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_K'45'trans_270 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 = T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 T_Kind_52
v0
du_K'45'trans_270 :: T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 :: T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 T_Kind_52
v0
  = case T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0 of
      T_Kind_52
C_implication_54
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_52
C_reverse'45'implication_56
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                ((AgdaAny -> AgdaAny) -> T__'8592'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> T__'8592'__12
C_lam_26
                  ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                     (\ AgdaAny
v3 ->
                        (T__'8592'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8592'__12 -> AgdaAny -> AgdaAny
d_app'45''8592'_24 AgdaAny
v1 ((T__'8592'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8592'__12 -> AgdaAny -> AgdaAny
d_app'45''8592'_24 AgdaAny
v2 AgdaAny
v3))))
      T_Kind_52
C_equivalence_58
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du__'8728'__82 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_52
C_injection_60
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Injection_88 -> T_Injection_88 -> T_Injection_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Injection_88 -> T_Injection_88 -> T_Injection_88
MAlonzo.Code.Function.Injection.du__'8728'__172 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_52
C_reverse'45'injection_62
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Injection_88 -> T__'8610'__36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Injection_88 -> T__'8610'__36
C_lam_50
                  ((T_Injection_88 -> T_Injection_88 -> T_Injection_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Injection_88 -> T_Injection_88 -> T_Injection_88
MAlonzo.Code.Function.Injection.du__'8728'__172
                     ((T__'8610'__36 -> T_Injection_88) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8610'__36 -> T_Injection_88
d_app'45''8610'_48 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                     ((T__'8610'__36 -> T_Injection_88) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8610'__36 -> T_Injection_88
d_app'45''8610'_48 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
      T_Kind_52
C_left'45'inverse_64
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Setoid_44
 -> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44
-> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
MAlonzo.Code.Function.LeftInverse.du__'8728'__280
                  (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_52
C_surjection_66
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Setoid_44
 -> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44
-> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.du__'8728'__196
                  (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_52
C_bijection_68
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Setoid_44
 -> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Setoid_44
-> T_Setoid_44 -> T_Inverse_58 -> T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du__'8728'__208
                  (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                  (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_52
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.SK-sym
d_SK'45'sym_286 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny
d_SK'45'sym_286 :: T_Symmetric'45'kind_142
-> () -> () -> () -> () -> AgdaAny -> AgdaAny
d_SK'45'sym_286 T_Symmetric'45'kind_142
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 = T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_SK'45'sym_286 T_Symmetric'45'kind_142
v0
du_SK'45'sym_286 :: T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_SK'45'sym_286 :: T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_SK'45'sym_286 T_Symmetric'45'kind_142
v0
  = case T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0 of
      T_Symmetric'45'kind_142
C_equivalence_144
        -> (T_Equivalence_16 -> T_Equivalence_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_sym_100
      T_Symmetric'45'kind_142
C_bijection_146 -> (T_Inverse_58 -> T_Inverse_58) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_sym_226
      T_Symmetric'45'kind_142
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.SK-isEquivalence
d_SK'45'isEquivalence_292 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_SK'45'isEquivalence_292 :: T_Symmetric'45'kind_142 -> () -> T_IsEquivalence_26
d_SK'45'isEquivalence_292 T_Symmetric'45'kind_142
v0 ~()
v1 = T_Symmetric'45'kind_142 -> T_IsEquivalence_26
du_SK'45'isEquivalence_292 T_Symmetric'45'kind_142
v0
du_SK'45'isEquivalence_292 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_SK'45'isEquivalence_292 :: T_Symmetric'45'kind_142 -> T_IsEquivalence_26
du_SK'45'isEquivalence_292 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
      (\ AgdaAny
v1 -> (T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
du_K'45'refl_254 ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0)))
      (\ AgdaAny
v1 AgdaAny
v2 -> (T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_SK'45'sym_286 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
         (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0)))
-- Function.Related.SK-setoid
d_SK'45'setoid_300 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_SK'45'setoid_300 :: T_Symmetric'45'kind_142 -> () -> T_Setoid_44
d_SK'45'setoid_300 T_Symmetric'45'kind_142
v0 ~()
v1 = T_Symmetric'45'kind_142 -> T_Setoid_44
du_SK'45'setoid_300 T_Symmetric'45'kind_142
v0
du_SK'45'setoid_300 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_SK'45'setoid_300 :: T_Symmetric'45'kind_142 -> T_Setoid_44
du_SK'45'setoid_300 T_Symmetric'45'kind_142
v0
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      ((T_Symmetric'45'kind_142 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsEquivalence_26
du_SK'45'isEquivalence_292 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.K-isPreorder
d_K'45'isPreorder_310 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_K'45'isPreorder_310 :: T_Kind_52 -> () -> T_IsPreorder_70
d_K'45'isPreorder_310 T_Kind_52
v0 ~()
v1 = T_Kind_52 -> T_IsPreorder_70
du_K'45'isPreorder_310 T_Kind_52
v0
du_K'45'isPreorder_310 ::
  T_Kind_52 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_K'45'isPreorder_310 :: T_Kind_52 -> T_IsPreorder_70
du_K'45'isPreorder_310 T_Kind_52
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
      ((T_Symmetric'45'kind_142 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsEquivalence_26
du_SK'45'isEquivalence_292 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
C_bijection_146))
      (\ AgdaAny
v1 AgdaAny
v2 -> (T_Kind_52 -> T_Inverse_58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> T_Inverse_58 -> AgdaAny
du_'8596''8658'_130 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0))
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0))
-- Function.Related.K-preorder
d_K'45'preorder_318 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_K'45'preorder_318 :: T_Kind_52 -> () -> T_Preorder_132
d_K'45'preorder_318 T_Kind_52
v0 ~()
v1 = T_Kind_52 -> T_Preorder_132
du_K'45'preorder_318 T_Kind_52
v0
du_K'45'preorder_318 ::
  T_Kind_52 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_K'45'preorder_318 :: T_Kind_52 -> T_Preorder_132
du_K'45'preorder_318 T_Kind_52
v0
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
      ((T_Kind_52 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> T_IsPreorder_70
du_K'45'isPreorder_310 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0))
-- Function.Related.EquationalReasoning._∼⟨_⟩_
d__'8764''10216'_'10217'__340 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'8764''10216'_'10217'__340 :: T_Kind_52
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8764''10216'_'10217'__340 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 AgdaAny
v7 AgdaAny
v8
  = T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8764''10216'_'10217'__340 T_Kind_52
v0 AgdaAny
v7 AgdaAny
v8
du__'8764''10216'_'10217'__340 ::
  T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8764''10216'_'10217'__340 :: T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8764''10216'_'10217'__340 T_Kind_52
v0 AgdaAny
v1 AgdaAny
v2
  = (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 T_Kind_52
v0 AgdaAny
v1 AgdaAny
v2
-- Function.Related.EquationalReasoning._↔⟨_⟩_
d__'8596''10216'_'10217'__360 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny -> AgdaAny
d__'8596''10216'_'10217'__360 :: T_Kind_52
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> T_Inverse_58
-> AgdaAny
-> AgdaAny
d__'8596''10216'_'10217'__360 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 T_Inverse_58
v7 AgdaAny
v8
  = T_Kind_52 -> T_Inverse_58 -> AgdaAny -> AgdaAny
du__'8596''10216'_'10217'__360 T_Kind_52
v0 T_Inverse_58
v7 AgdaAny
v8
du__'8596''10216'_'10217'__360 ::
  T_Kind_52 ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny -> AgdaAny
du__'8596''10216'_'10217'__360 :: T_Kind_52 -> T_Inverse_58 -> AgdaAny -> AgdaAny
du__'8596''10216'_'10217'__360 T_Kind_52
v0 T_Inverse_58
v1 AgdaAny
v2
  = (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8764''10216'_'10217'__340 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0)
      ((T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> T_Inverse_58 -> AgdaAny
du_'8596''8658'_130 T_Kind_52
v0 T_Inverse_58
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
-- Function.Related.EquationalReasoning._↔⟨⟩_
d__'8596''10216''10217'__378 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny
d__'8596''10216''10217'__378 :: T_Kind_52 -> () -> () -> () -> () -> AgdaAny -> AgdaAny
d__'8596''10216''10217'__378 ~T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 AgdaAny
v5
  = AgdaAny -> AgdaAny
du__'8596''10216''10217'__378 AgdaAny
v5
du__'8596''10216''10217'__378 :: AgdaAny -> AgdaAny
du__'8596''10216''10217'__378 :: AgdaAny -> AgdaAny
du__'8596''10216''10217'__378 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Function.Related.EquationalReasoning._≡⟨_⟩_
d__'8801''10216'_'10217'__396 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> AgdaAny
d__'8801''10216'_'10217'__396 :: T_Kind_52
-> ()
-> ()
-> ()
-> ()
-> ()
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d__'8801''10216'_'10217'__396 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~T__'8801'__12
v6 AgdaAny
v7
  = T_Kind_52 -> AgdaAny -> AgdaAny
du__'8801''10216'_'10217'__396 T_Kind_52
v0 AgdaAny
v7
du__'8801''10216'_'10217'__396 :: T_Kind_52 -> AgdaAny -> AgdaAny
du__'8801''10216'_'10217'__396 :: T_Kind_52 -> AgdaAny -> AgdaAny
du__'8801''10216'_'10217'__396 T_Kind_52
v0 AgdaAny
v1
  = (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8764''10216'_'10217'__340 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0)
      ((T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
du_'8801''8658'_140 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Function.Related.EquationalReasoning._∎
d__'8718'_410 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny
d__'8718'_410 :: T_Kind_52 -> () -> () -> AgdaAny
d__'8718'_410 T_Kind_52
v0 ~()
v1 ~()
v2 = T_Kind_52 -> AgdaAny
du__'8718'_410 T_Kind_52
v0
du__'8718'_410 :: T_Kind_52 -> AgdaAny
du__'8718'_410 :: T_Kind_52 -> AgdaAny
du__'8718'_410 T_Kind_52
v0 = (T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
du_K'45'refl_254 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0)
-- Function.Related.EquationalReasoning.sym
d_sym_414 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny
d_sym_414 :: T_Symmetric'45'kind_142
-> () -> () -> () -> () -> AgdaAny -> AgdaAny
d_sym_414 T_Symmetric'45'kind_142
v0 ()
v1 ()
v2 ()
v3 ()
v4 = (T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny)
-> T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_SK'45'sym_286 T_Symmetric'45'kind_142
v0
-- Function.Related.InducedRelation₁
d_InducedRelation'8321'_422 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d_InducedRelation'8321'_422 :: T_Kind_52
-> () -> () -> () -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d_InducedRelation'8321'_422 = T_Kind_52
-> () -> () -> () -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Function.Related.InducedPreorder₁
d_InducedPreorder'8321'_438 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_InducedPreorder'8321'_438 :: T_Kind_52 -> () -> () -> () -> (AgdaAny -> ()) -> T_Preorder_132
d_InducedPreorder'8321'_438 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4
  = T_Kind_52 -> T_Preorder_132
du_InducedPreorder'8321'_438 T_Kind_52
v0
du_InducedPreorder'8321'_438 ::
  T_Kind_52 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_InducedPreorder'8321'_438 :: T_Kind_52 -> T_Preorder_132
du_InducedPreorder'8321'_438 T_Kind_52
v0
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
      ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
         (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
               (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> T_Inverse_58 -> AgdaAny
du_'8596''8658'_130 T_Kind_52
v0
                 ((T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
du_K'45'reflexive_260 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
C_bijection_68))))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0))))
-- Function.Related.InducedEquivalence₁
d_InducedEquivalence'8321'_502 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) -> MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence'8321'_502 :: T_Symmetric'45'kind_142
-> () -> () -> () -> (AgdaAny -> ()) -> T_Setoid_44
d_InducedEquivalence'8321'_502 T_Symmetric'45'kind_142
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4
  = T_Symmetric'45'kind_142 -> T_Setoid_44
du_InducedEquivalence'8321'_502 T_Symmetric'45'kind_142
v0
du_InducedEquivalence'8321'_502 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence'8321'_502 :: T_Symmetric'45'kind_142 -> T_Setoid_44
du_InducedEquivalence'8321'_502 T_Symmetric'45'kind_142
v0
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 -> (T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
du_K'45'refl_254 ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> (T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_SK'45'sym_286 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0)))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
               (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0)))))
-- Function.Related.InducedRelation₂
d_InducedRelation'8322'_518 ::
  T_Kind_52 ->
  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 -> ()
d_InducedRelation'8322'_518 :: T_Kind_52
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
d_InducedRelation'8322'_518 = T_Kind_52
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
-- Function.Related.InducedPreorder₂
d_InducedPreorder'8322'_540 ::
  T_Kind_52 ->
  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.Relation.Binary.Bundles.T_Preorder_132
d_InducedPreorder'8322'_540 :: T_Kind_52
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Preorder_132
d_InducedPreorder'8322'_540 T_Kind_52
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6
  = T_Kind_52 -> T_Preorder_132
du_InducedPreorder'8322'_540 T_Kind_52
v0
du_InducedPreorder'8322'_540 ::
  T_Kind_52 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_InducedPreorder'8322'_540 :: T_Kind_52 -> T_Preorder_132
du_InducedPreorder'8322'_540 T_Kind_52
v0
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
      ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
         (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
               (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> T_Inverse_58 -> AgdaAny
du_'8596''8658'_130 T_Kind_52
v0
                 ((T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
du_K'45'reflexive_260 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
C_bijection_68))))
         ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
               (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 T_Kind_52
v0 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4 AgdaAny
v6) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5 AgdaAny
v6))))
-- Function.Related.InducedEquivalence₂
d_InducedEquivalence'8322'_616 ::
  T_Symmetric'45'kind_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.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence'8322'_616 :: T_Symmetric'45'kind_142
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Setoid_44
d_InducedEquivalence'8322'_616 T_Symmetric'45'kind_142
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6
  = T_Symmetric'45'kind_142 -> T_Setoid_44
du_InducedEquivalence'8322'_616 T_Symmetric'45'kind_142
v0
du_InducedEquivalence'8322'_616 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence'8322'_616 :: T_Symmetric'45'kind_142 -> T_Setoid_44
du_InducedEquivalence'8322'_616 T_Symmetric'45'kind_142
v0
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 ->
               (T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
du_K'45'refl_254 ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> (T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny)
-> T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_SK'45'sym_286 T_Symmetric'45'kind_142
v0 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 AgdaAny
v4)))
         ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
               (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_270 (T_Symmetric'45'kind_142 -> T_Kind_52
d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0)) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4 AgdaAny
v6)
                 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5 AgdaAny
v6))))
-- Function.Related.preorder
d_preorder_654 ::
  T_Kind_52 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_preorder_654 :: T_Kind_52 -> () -> T_Preorder_132
d_preorder_654 T_Kind_52
v0 ()
v1 = (T_Kind_52 -> T_Preorder_132) -> T_Kind_52 -> T_Preorder_132
forall a b. a -> b
coe T_Kind_52 -> T_Preorder_132
du_K'45'preorder_318 T_Kind_52
v0
-- Function.Related.setoid
d_setoid_656 ::
  T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_setoid_656 :: T_Symmetric'45'kind_142 -> () -> T_Setoid_44
d_setoid_656 T_Symmetric'45'kind_142
v0 ()
v1 = (T_Symmetric'45'kind_142 -> T_Setoid_44)
-> T_Symmetric'45'kind_142 -> T_Setoid_44
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Setoid_44
du_SK'45'setoid_300 T_Symmetric'45'kind_142
v0