{-# 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.Propositional 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.Bundles
import qualified MAlonzo.Code.Function.Construct.Composition
import qualified MAlonzo.Code.Function.Construct.Identity
import qualified MAlonzo.Code.Function.Construct.Symmetry
import qualified MAlonzo.Code.Function.Properties.Bijection
import qualified MAlonzo.Code.Function.Properties.Inverse
import qualified MAlonzo.Code.Function.Properties.RightInverse
import qualified MAlonzo.Code.Function.Properties.Surjection
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Related.Propositional.Kind
d_Kind_6 :: ()
d_Kind_6 = ()
data T_Kind_6
  = C_implication_8 | C_reverseImplication_10 | C_equivalence_12 |
    C_injection_14 | C_reverseInjection_16 | C_leftInverse_18 |
    C_surjection_20 | C_bijection_22
-- Function.Related.Propositional._∼[_]_
d__'8764''91'_'93'__40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Kind_6 -> () -> ()
d__'8764''91'_'93'__40 :: () -> () -> () -> T_Kind_6 -> () -> ()
d__'8764''91'_'93'__40 = () -> () -> () -> T_Kind_6 -> () -> ()
forall a. a
erased
-- Function.Related.Propositional.Related
d_Related_74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Kind_6 -> () -> () -> ()
d_Related_74 :: () -> () -> T_Kind_6 -> () -> () -> ()
d_Related_74 = () -> () -> T_Kind_6 -> () -> () -> ()
forall a. a
erased
-- Function.Related.Propositional.↔⇒
d_'8596''8658'_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Kind_6 -> MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny
d_'8596''8658'_82 :: () -> () -> () -> () -> T_Kind_6 -> T_Inverse_1960 -> AgdaAny
d_'8596''8658'_82 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Kind_6
v4 = T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 T_Kind_6
v4
du_'8596''8658'_82 ::
  T_Kind_6 -> MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 :: T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 T_Kind_6
v0
  = case T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
v0 of
      T_Kind_6
C_implication_8
        -> (AgdaAny -> AgdaAny) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                ((AgdaAny -> AgdaAny) -> T_Func_714) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> T_Func_714
MAlonzo.Code.Function.Bundles.du_mk'10230'_2266
                  ((T_Inverse_1960 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_6
C_reverseImplication_10
        -> (AgdaAny -> AgdaAny) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                ((AgdaAny -> AgdaAny) -> T_Func_714) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> T_Func_714
MAlonzo.Code.Function.Bundles.du_mk'10230'_2266
                  ((T_Inverse_1960 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_6
C_equivalence_12
        -> (T_Inverse_1960 -> T_Equivalence_1714) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_1960 -> T_Equivalence_1714
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8660'_648
      T_Kind_6
C_injection_14
        -> (T_Inverse_1960 -> T_Injection_776) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_1960 -> T_Injection_776
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8611'_642
      T_Kind_6
C_reverseInjection_16
        -> (AgdaAny -> AgdaAny) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                (T_Inverse_1960 -> T_Injection_776) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Inverse_1960 -> T_Injection_776
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8611'_642
                  ((T_Inverse_1960 -> T_Inverse_1960) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Symmetry.du_inverse_1052 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_6
C_leftInverse_18
        -> (T_Inverse_1960 -> T_RightInverse_1880)
-> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.du_rightInverse_1988
      T_Kind_6
C_surjection_20
        -> (T_Inverse_1960 -> T_Surjection_846) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_1960 -> T_Surjection_846
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8608'_644
      T_Kind_6
C_bijection_22 -> (AgdaAny -> AgdaAny) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Kind_6
_ -> T_Inverse_1960 -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.≡⇒
d_'8801''8658'_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  T_Kind_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'8801''8658'_84 :: () -> () -> () -> T_Kind_6 -> T__'8801'__12 -> AgdaAny
d_'8801''8658'_84 ~()
v0 ~()
v1 ~()
v2 T_Kind_6
v3 ~T__'8801'__12
v4 = T_Kind_6 -> AgdaAny
du_'8801''8658'_84 T_Kind_6
v3
du_'8801''8658'_84 :: T_Kind_6 -> AgdaAny
du_'8801''8658'_84 :: T_Kind_6 -> AgdaAny
du_'8801''8658'_84 T_Kind_6
v0
  = (T_Kind_6 -> T_Inverse_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 T_Kind_6
v0
      (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
MAlonzo.Code.Function.Construct.Identity.du_'8596''45'id_820)
-- Function.Related.Propositional.SymmetricKind
d_SymmetricKind_86 :: ()
d_SymmetricKind_86 = ()
data T_SymmetricKind_86 = C_equivalence_88 | C_bijection_90
-- Function.Related.Propositional.⌊_⌋
d_'8970'_'8971'_92 :: T_SymmetricKind_86 -> T_Kind_6
d_'8970'_'8971'_92 :: T_SymmetricKind_86 -> T_Kind_6
d_'8970'_'8971'_92 T_SymmetricKind_86
v0
  = case T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0 of
      T_SymmetricKind_86
C_equivalence_88 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_equivalence_12
      T_SymmetricKind_86
C_bijection_90 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_bijection_22
      T_SymmetricKind_86
_ -> T_Kind_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.ForwardKind
d_ForwardKind_94 :: ()
d_ForwardKind_94 = ()
data T_ForwardKind_94
  = C_implication_96 | C_equivalence_98 | C_injection_100 |
    C_leftInverse_102 | C_surjection_104 | C_bijection_106
-- Function.Related.Propositional.⌊_⌋→
d_'8970'_'8971''8594'_108 :: T_ForwardKind_94 -> T_Kind_6
d_'8970'_'8971''8594'_108 :: T_ForwardKind_94 -> T_Kind_6
d_'8970'_'8971''8594'_108 T_ForwardKind_94
v0
  = case T_ForwardKind_94 -> T_ForwardKind_94
forall a b. a -> b
coe T_ForwardKind_94
v0 of
      T_ForwardKind_94
C_implication_96 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_implication_8
      T_ForwardKind_94
C_equivalence_98 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_equivalence_12
      T_ForwardKind_94
C_injection_100 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_injection_14
      T_ForwardKind_94
C_leftInverse_102 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_leftInverse_18
      T_ForwardKind_94
C_surjection_104 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_surjection_20
      T_ForwardKind_94
C_bijection_106 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_bijection_22
      T_ForwardKind_94
_ -> T_Kind_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.⇒→
d_'8658''8594'_112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_ForwardKind_94 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8658''8594'_112 :: ()
-> ()
-> ()
-> ()
-> T_ForwardKind_94
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8658''8594'_112 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_ForwardKind_94
v4 = T_ForwardKind_94 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8594'_112 T_ForwardKind_94
v4
du_'8658''8594'_112 ::
  T_ForwardKind_94 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8594'_112 :: T_ForwardKind_94 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8594'_112 T_ForwardKind_94
v0
  = case T_ForwardKind_94 -> T_ForwardKind_94
forall a b. a -> b
coe T_ForwardKind_94
v0 of
      T_ForwardKind_94
C_implication_96
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Func_714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_720 (AgdaAny -> T_Func_714
forall a b. a -> b
coe AgdaAny
v1))
      T_ForwardKind_94
C_equivalence_98
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 (AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe AgdaAny
v1))
      T_ForwardKind_94
C_injection_100
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Injection_776 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_784 (AgdaAny -> T_Injection_776
forall a b. a -> b
coe AgdaAny
v1))
      T_ForwardKind_94
C_leftInverse_102
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 (AgdaAny -> T_RightInverse_1880
forall a b. a -> b
coe AgdaAny
v1))
      T_ForwardKind_94
C_surjection_104
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 (AgdaAny -> T_Surjection_846
forall a b. a -> b
coe AgdaAny
v1))
      T_ForwardKind_94
C_bijection_106
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 (AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe AgdaAny
v1))
      T_ForwardKind_94
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.BackwardKind
d_BackwardKind_114 :: ()
d_BackwardKind_114 = ()
data T_BackwardKind_114
  = C_reverseImplication_116 | C_equivalence_118 |
    C_reverseInjection_120 | C_leftInverse_122 | C_surjection_124 |
    C_bijection_126
-- Function.Related.Propositional.⌊_⌋←
d_'8970'_'8971''8592'_128 :: T_BackwardKind_114 -> T_Kind_6
d_'8970'_'8971''8592'_128 :: T_BackwardKind_114 -> T_Kind_6
d_'8970'_'8971''8592'_128 T_BackwardKind_114
v0
  = case T_BackwardKind_114 -> T_BackwardKind_114
forall a b. a -> b
coe T_BackwardKind_114
v0 of
      T_BackwardKind_114
C_reverseImplication_116 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_reverseImplication_10
      T_BackwardKind_114
C_equivalence_118 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_equivalence_12
      T_BackwardKind_114
C_reverseInjection_120 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_reverseInjection_16
      T_BackwardKind_114
C_leftInverse_122 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_leftInverse_18
      T_BackwardKind_114
C_surjection_124 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_surjection_20
      T_BackwardKind_114
C_bijection_126 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_bijection_22
      T_BackwardKind_114
_ -> T_Kind_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.⇒←
d_'8658''8592'_132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_BackwardKind_114 -> AgdaAny -> AgdaAny -> AgdaAny
d_'8658''8592'_132 :: ()
-> ()
-> ()
-> ()
-> T_BackwardKind_114
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8658''8592'_132 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_BackwardKind_114
v4 = T_BackwardKind_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8592'_132 T_BackwardKind_114
v4
du_'8658''8592'_132 ::
  T_BackwardKind_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8592'_132 :: T_BackwardKind_114 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8592'_132 T_BackwardKind_114
v0
  = case T_BackwardKind_114 -> T_BackwardKind_114
forall a b. a -> b
coe T_BackwardKind_114
v0 of
      T_BackwardKind_114
C_reverseImplication_116
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Func_714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_720 (AgdaAny -> T_Func_714
forall a b. a -> b
coe AgdaAny
v1))
      T_BackwardKind_114
C_equivalence_118
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726 (AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe AgdaAny
v1))
      T_BackwardKind_114
C_reverseInjection_120
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Injection_776 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_784 (AgdaAny -> T_Injection_776
forall a b. a -> b
coe AgdaAny
v1))
      T_BackwardKind_114
C_leftInverse_122
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 (AgdaAny -> T_RightInverse_1880
forall a b. a -> b
coe AgdaAny
v1))
      T_BackwardKind_114
C_surjection_124
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892
                  ((T_Surjection_846 -> T_RightInverse_1880)
-> AgdaAny -> T_RightInverse_1880
forall a b. a -> b
coe
                     T_Surjection_846 -> T_RightInverse_1880
MAlonzo.Code.Function.Properties.Surjection.du_'8608''8658''8618'_152
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_BackwardKind_114
C_bijection_126
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 (AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe AgdaAny
v1))
      T_BackwardKind_114
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.EquivalenceKind
d_EquivalenceKind_134 :: ()
d_EquivalenceKind_134 = ()
data T_EquivalenceKind_134
  = C_equivalence_136 | C_leftInverse_138 | C_surjection_140 |
    C_bijection_142
-- Function.Related.Propositional.⌊_⌋⇔
d_'8970'_'8971''8660'_144 :: T_EquivalenceKind_134 -> T_Kind_6
d_'8970'_'8971''8660'_144 :: T_EquivalenceKind_134 -> T_Kind_6
d_'8970'_'8971''8660'_144 T_EquivalenceKind_134
v0
  = case T_EquivalenceKind_134 -> T_EquivalenceKind_134
forall a b. a -> b
coe T_EquivalenceKind_134
v0 of
      T_EquivalenceKind_134
C_equivalence_136 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_equivalence_12
      T_EquivalenceKind_134
C_leftInverse_138 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_leftInverse_18
      T_EquivalenceKind_134
C_surjection_140 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_surjection_20
      T_EquivalenceKind_134
C_bijection_142 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_bijection_22
      T_EquivalenceKind_134
_ -> T_Kind_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.⇒⇔
d_'8658''8660'_148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_EquivalenceKind_134 ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'8658''8660'_148 :: ()
-> ()
-> ()
-> ()
-> T_EquivalenceKind_134
-> AgdaAny
-> T_Equivalence_1714
d_'8658''8660'_148 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_EquivalenceKind_134
v4 = T_EquivalenceKind_134 -> AgdaAny -> T_Equivalence_1714
du_'8658''8660'_148 T_EquivalenceKind_134
v4
du_'8658''8660'_148 ::
  T_EquivalenceKind_134 ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'8658''8660'_148 :: T_EquivalenceKind_134 -> AgdaAny -> T_Equivalence_1714
du_'8658''8660'_148 T_EquivalenceKind_134
v0
  = case T_EquivalenceKind_134 -> T_EquivalenceKind_134
forall a b. a -> b
coe T_EquivalenceKind_134
v0 of
      T_EquivalenceKind_134
C_equivalence_136 -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_EquivalenceKind_134
C_leftInverse_138
        -> (T_RightInverse_1880 -> T_Equivalence_1714)
-> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe T_RightInverse_1880 -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_equivalence_1958
      T_EquivalenceKind_134
C_surjection_140
        -> (T_Surjection_846 -> T_Equivalence_1714)
-> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
             T_Surjection_846 -> T_Equivalence_1714
MAlonzo.Code.Function.Properties.Surjection.du_'8608''8658''8660'_230
      T_EquivalenceKind_134
C_bijection_142
        -> (T_Inverse_1960 -> T_Equivalence_1714)
-> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
             T_Inverse_1960 -> T_Equivalence_1714
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8660'_648
      T_EquivalenceKind_134
_ -> AgdaAny -> T_Equivalence_1714
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.⇔⌊_⌋
d_'8660''8970'_'8971'_150 ::
  T_SymmetricKind_86 -> T_EquivalenceKind_134
d_'8660''8970'_'8971'_150 :: T_SymmetricKind_86 -> T_EquivalenceKind_134
d_'8660''8970'_'8971'_150 T_SymmetricKind_86
v0
  = case T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0 of
      T_SymmetricKind_86
C_equivalence_88 -> T_EquivalenceKind_134 -> T_EquivalenceKind_134
forall a b. a -> b
coe T_EquivalenceKind_134
C_equivalence_136
      T_SymmetricKind_86
C_bijection_90 -> T_EquivalenceKind_134 -> T_EquivalenceKind_134
forall a b. a -> b
coe T_EquivalenceKind_134
C_bijection_142
      T_SymmetricKind_86
_ -> T_EquivalenceKind_134
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.→⌊_⌋
d_'8594''8970'_'8971'_152 ::
  T_EquivalenceKind_134 -> T_ForwardKind_94
d_'8594''8970'_'8971'_152 :: T_EquivalenceKind_134 -> T_ForwardKind_94
d_'8594''8970'_'8971'_152 T_EquivalenceKind_134
v0
  = case T_EquivalenceKind_134 -> T_EquivalenceKind_134
forall a b. a -> b
coe T_EquivalenceKind_134
v0 of
      T_EquivalenceKind_134
C_equivalence_136 -> T_ForwardKind_94 -> T_ForwardKind_94
forall a b. a -> b
coe T_ForwardKind_94
C_equivalence_98
      T_EquivalenceKind_134
C_leftInverse_138 -> T_ForwardKind_94 -> T_ForwardKind_94
forall a b. a -> b
coe T_ForwardKind_94
C_leftInverse_102
      T_EquivalenceKind_134
C_surjection_140 -> T_ForwardKind_94 -> T_ForwardKind_94
forall a b. a -> b
coe T_ForwardKind_94
C_surjection_104
      T_EquivalenceKind_134
C_bijection_142 -> T_ForwardKind_94 -> T_ForwardKind_94
forall a b. a -> b
coe T_ForwardKind_94
C_bijection_106
      T_EquivalenceKind_134
_ -> T_ForwardKind_94
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.←⌊_⌋
d_'8592''8970'_'8971'_154 ::
  T_EquivalenceKind_134 -> T_BackwardKind_114
d_'8592''8970'_'8971'_154 :: T_EquivalenceKind_134 -> T_BackwardKind_114
d_'8592''8970'_'8971'_154 T_EquivalenceKind_134
v0
  = case T_EquivalenceKind_134 -> T_EquivalenceKind_134
forall a b. a -> b
coe T_EquivalenceKind_134
v0 of
      T_EquivalenceKind_134
C_equivalence_136 -> T_BackwardKind_114 -> T_BackwardKind_114
forall a b. a -> b
coe T_BackwardKind_114
C_equivalence_118
      T_EquivalenceKind_134
C_leftInverse_138 -> T_BackwardKind_114 -> T_BackwardKind_114
forall a b. a -> b
coe T_BackwardKind_114
C_leftInverse_122
      T_EquivalenceKind_134
C_surjection_140 -> T_BackwardKind_114 -> T_BackwardKind_114
forall a b. a -> b
coe T_BackwardKind_114
C_surjection_124
      T_EquivalenceKind_134
C_bijection_142 -> T_BackwardKind_114 -> T_BackwardKind_114
forall a b. a -> b
coe T_BackwardKind_114
C_bijection_126
      T_EquivalenceKind_134
_ -> T_BackwardKind_114
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional._op
d__op_156 :: T_Kind_6 -> T_Kind_6
d__op_156 :: T_Kind_6 -> T_Kind_6
d__op_156 T_Kind_6
v0
  = case T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
v0 of
      T_Kind_6
C_implication_8 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_reverseImplication_10
      T_Kind_6
C_reverseImplication_10 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_implication_8
      T_Kind_6
C_equivalence_12 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
v0
      T_Kind_6
C_injection_14 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_reverseInjection_16
      T_Kind_6
C_reverseInjection_16 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_injection_14
      T_Kind_6
C_leftInverse_18 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_surjection_20
      T_Kind_6
C_surjection_20 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
C_leftInverse_18
      T_Kind_6
C_bijection_22 -> T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
v0
      T_Kind_6
_ -> T_Kind_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.reverse
d_reverse_158 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny -> AgdaAny
d_reverse_158 :: () -> () -> T_Kind_6 -> () -> () -> AgdaAny -> AgdaAny
d_reverse_158 ~()
v0 ~()
v1 T_Kind_6
v2 ~()
v3 ~()
v4 = T_Kind_6 -> AgdaAny -> AgdaAny
du_reverse_158 T_Kind_6
v2
du_reverse_158 :: T_Kind_6 -> AgdaAny -> AgdaAny
du_reverse_158 :: T_Kind_6 -> AgdaAny -> AgdaAny
du_reverse_158 T_Kind_6
v0
  = case T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
v0 of
      T_Kind_6
C_implication_8 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Kind_6
C_reverseImplication_10 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Kind_6
C_equivalence_12
        -> (T_Equivalence_1714 -> T_Equivalence_1714) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Equivalence_1714 -> T_Equivalence_1714
MAlonzo.Code.Function.Construct.Symmetry.du_'8660''45'sym_1142
      T_Kind_6
C_injection_14 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Kind_6
C_reverseInjection_16 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Kind_6
C_leftInverse_18
        -> (T_RightInverse_1880 -> T_Surjection_846) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_RightInverse_1880 -> T_Surjection_846
MAlonzo.Code.Function.Properties.RightInverse.du_'8618''8658''8608'_398
      T_Kind_6
C_surjection_20
        -> (T_Surjection_846 -> T_RightInverse_1880) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Surjection_846 -> T_RightInverse_1880
MAlonzo.Code.Function.Properties.Surjection.du_'8608''8658''8618'_152
      T_Kind_6
C_bijection_22
        -> (T_Inverse_1960 -> T_Inverse_1960) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Symmetry.du_'8596''45'sym_1148
      T_Kind_6
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.K-refl
d_K'45'refl_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> T_Kind_6 -> () -> AgdaAny
d_K'45'refl_160 :: () -> T_Kind_6 -> () -> AgdaAny
d_K'45'refl_160 ~()
v0 T_Kind_6
v1 ~()
v2 = T_Kind_6 -> AgdaAny
du_K'45'refl_160 T_Kind_6
v1
du_K'45'refl_160 :: T_Kind_6 -> AgdaAny
du_K'45'refl_160 :: T_Kind_6 -> AgdaAny
du_K'45'refl_160 T_Kind_6
v0
  = case T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
v0 of
      T_Kind_6
C_implication_8
        -> T_Func_714 -> AgdaAny
forall a b. a -> b
coe
             T_Func_714
MAlonzo.Code.Function.Construct.Identity.du_'10230''45'id_806
      T_Kind_6
C_reverseImplication_10
        -> T_Func_714 -> AgdaAny
forall a b. a -> b
coe
             T_Func_714
MAlonzo.Code.Function.Construct.Identity.du_'10230''45'id_806
      T_Kind_6
C_equivalence_12
        -> T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
MAlonzo.Code.Function.Construct.Identity.du_'8660''45'id_814
      T_Kind_6
C_injection_14
        -> T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
MAlonzo.Code.Function.Construct.Identity.du_'8611''45'id_808
      T_Kind_6
C_reverseInjection_16
        -> T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
MAlonzo.Code.Function.Construct.Identity.du_'8611''45'id_808
      T_Kind_6
C_leftInverse_18
        -> T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
MAlonzo.Code.Function.Construct.Identity.du_'8618''45'id_818
      T_Kind_6
C_surjection_20
        -> T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
MAlonzo.Code.Function.Construct.Identity.du_'8608''45'id_810
      T_Kind_6
C_bijection_22
        -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
MAlonzo.Code.Function.Construct.Identity.du_'8596''45'id_820
      T_Kind_6
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.K-reflexive
d_K'45'reflexive_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Kind_6 ->
  () ->
  () -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_K'45'reflexive_162 :: () -> T_Kind_6 -> () -> () -> T__'8801'__12 -> AgdaAny
d_K'45'reflexive_162 ~()
v0 T_Kind_6
v1 ~()
v2 ~()
v3 ~T__'8801'__12
v4 = T_Kind_6 -> AgdaAny
du_K'45'reflexive_162 T_Kind_6
v1
du_K'45'reflexive_162 :: T_Kind_6 -> AgdaAny
du_K'45'reflexive_162 :: T_Kind_6 -> AgdaAny
du_K'45'reflexive_162 T_Kind_6
v0 = (T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny
du_K'45'refl_160 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0)
-- Function.Related.Propositional.K-trans
d_K'45'trans_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_K'45'trans_164 :: ()
-> ()
-> T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_K'45'trans_164 ~()
v0 ~()
v1 T_Kind_6
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 = T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 T_Kind_6
v2
du_K'45'trans_164 :: T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 :: T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 T_Kind_6
v0
  = case T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
v0 of
      T_Kind_6
C_implication_8
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Func_714 -> T_Func_714 -> T_Func_714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Func_714 -> T_Func_714 -> T_Func_714
MAlonzo.Code.Function.Construct.Composition.du__'10230''45''8728'__2376
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_6
C_reverseImplication_10
        -> (T_Func_714 -> T_Func_714 -> T_Func_714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Func_714 -> T_Func_714 -> T_Func_714
MAlonzo.Code.Function.Construct.Composition.du__'10230''45''8728'__2376
      T_Kind_6
C_equivalence_12
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
MAlonzo.Code.Function.Construct.Composition.du__'8660''45''8728'__2384
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_6
C_injection_14
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Injection_776 -> T_Injection_776 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Injection_776 -> T_Injection_776 -> T_Injection_776
MAlonzo.Code.Function.Construct.Composition.du__'8611''45''8728'__2378
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_6
C_reverseInjection_16
        -> (T_Injection_776 -> T_Injection_776 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Injection_776 -> T_Injection_776 -> T_Injection_776
MAlonzo.Code.Function.Construct.Composition.du__'8611''45''8728'__2378
      T_Kind_6
C_leftInverse_18
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
MAlonzo.Code.Function.Construct.Composition.du__'8618''45''8728'__2388
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_6
C_surjection_20
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
MAlonzo.Code.Function.Construct.Composition.du__'8608''45''8728'__2380
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_6
C_bijection_22
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Composition.du__'8596''45''8728'__2390
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      T_Kind_6
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.SK-sym
d_SK'45'sym_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_SymmetricKind_86 -> () -> () -> AgdaAny -> AgdaAny
d_SK'45'sym_168 :: () -> () -> T_SymmetricKind_86 -> () -> () -> AgdaAny -> AgdaAny
d_SK'45'sym_168 ~()
v0 ~()
v1 T_SymmetricKind_86
v2 ~()
v3 ~()
v4 = T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_SK'45'sym_168 T_SymmetricKind_86
v2
du_SK'45'sym_168 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_SK'45'sym_168 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_SK'45'sym_168 T_SymmetricKind_86
v0
  = case T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0 of
      T_SymmetricKind_86
C_equivalence_88 -> (T_Kind_6 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny
du_reverse_158 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
C_equivalence_12)
      T_SymmetricKind_86
C_bijection_90 -> (T_Kind_6 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny
du_reverse_158 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
C_bijection_22)
      T_SymmetricKind_86
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.Propositional.SK-isEquivalence
d_SK'45'isEquivalence_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_SK'45'isEquivalence_172 :: () -> T_SymmetricKind_86 -> T_IsEquivalence_26
d_SK'45'isEquivalence_172 ~()
v0 T_SymmetricKind_86
v1 = T_SymmetricKind_86 -> T_IsEquivalence_26
du_SK'45'isEquivalence_172 T_SymmetricKind_86
v1
du_SK'45'isEquivalence_172 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_SK'45'isEquivalence_172 :: T_SymmetricKind_86 -> T_IsEquivalence_26
du_SK'45'isEquivalence_172 T_SymmetricKind_86
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_745
      (\ AgdaAny
v1 -> (T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny
du_K'45'refl_160 ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_Kind_6
d_'8970'_'8971'_92 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0)))
      (\ AgdaAny
v1 AgdaAny
v2 -> (T_SymmetricKind_86 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_SK'45'sym_168 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
         (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_Kind_6
d_'8970'_'8971'_92 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0)))
-- Function.Related.Propositional.SK-setoid
d_SK'45'setoid_178 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_SK'45'setoid_178 :: T_SymmetricKind_86 -> () -> T_Setoid_44
d_SK'45'setoid_178 T_SymmetricKind_86
v0 ~()
v1 = T_SymmetricKind_86 -> T_Setoid_44
du_SK'45'setoid_178 T_SymmetricKind_86
v0
du_SK'45'setoid_178 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_SK'45'setoid_178 :: T_SymmetricKind_86 -> T_Setoid_44
du_SK'45'setoid_178 T_SymmetricKind_86
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_733
      ((T_SymmetricKind_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsEquivalence_26
du_SK'45'isEquivalence_172 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.Propositional.K-isPreorder
d_K'45'isPreorder_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_K'45'isPreorder_186 :: () -> T_Kind_6 -> T_IsPreorder_70
d_K'45'isPreorder_186 ~()
v0 T_Kind_6
v1 = T_Kind_6 -> T_IsPreorder_70
du_K'45'isPreorder_186 T_Kind_6
v1
du_K'45'isPreorder_186 ::
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_K'45'isPreorder_186 :: T_Kind_6 -> T_IsPreorder_70
du_K'45'isPreorder_186 T_Kind_6
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> 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_4003
      ((T_SymmetricKind_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsEquivalence_26
du_SK'45'isEquivalence_172 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
C_bijection_90))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> (T_Kind_6 -> T_Inverse_1960 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0)))
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
-- Function.Related.Propositional.K-preorder
d_K'45'preorder_192 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_K'45'preorder_192 :: T_Kind_6 -> () -> T_Preorder_132
d_K'45'preorder_192 T_Kind_6
v0 ~()
v1 = T_Kind_6 -> T_Preorder_132
du_K'45'preorder_192 T_Kind_6
v0
du_K'45'preorder_192 ::
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_K'45'preorder_192 :: T_Kind_6 -> T_Preorder_132
du_K'45'preorder_192 T_Kind_6
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_2267
      ((T_Kind_6 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_IsPreorder_70
du_K'45'isPreorder_186 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
-- Function.Related.Propositional.EquationalReasoning._._.begin_
d_begin__212 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny
d_begin__212 :: T_Kind_6 -> () -> () -> () -> () -> AgdaAny -> AgdaAny
d_begin__212 ~T_Kind_6
v0 ~()
v1 ~()
v2 = () -> () -> AgdaAny -> AgdaAny
du_begin__212
du_begin__212 :: () -> () -> AgdaAny -> AgdaAny
du_begin__212 :: () -> () -> AgdaAny -> AgdaAny
du_begin__212
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> () -> () -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Related.Propositional.EquationalReasoning._._.step-≡
d_step'45''8801'_216 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_step'45''8801'_216 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_step'45''8801'_216 ~T_Kind_6
v0 ~()
v1 ~()
v2 = () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_step'45''8801'_216
du_step'45''8801'_216 ::
  () ->
  () ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_step'45''8801'_216 :: () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_step'45''8801'_216
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny -> () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny
 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801'_450
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Function.Related.Propositional.EquationalReasoning._._.step-≡-∣
d_step'45''8801''45''8739'_218 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny
d_step'45''8801''45''8739'_218 :: T_Kind_6 -> () -> () -> () -> () -> AgdaAny -> AgdaAny
d_step'45''8801''45''8739'_218 ~T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 AgdaAny
v5
  = AgdaAny -> AgdaAny
du_step'45''8801''45''8739'_218 AgdaAny
v5
du_step'45''8801''45''8739'_218 :: AgdaAny -> AgdaAny
du_step'45''8801''45''8739'_218 :: AgdaAny -> AgdaAny
du_step'45''8801''45''8739'_218 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Function.Related.Propositional.EquationalReasoning._._.step-≡-⟨
d_step'45''8801''45''10216'_220 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_step'45''8801''45''10216'_220 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_step'45''8801''45''10216'_220 ~T_Kind_6
v0 ~()
v1 ~()
v2
  = () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_step'45''8801''45''10216'_220
du_step'45''8801''45''10216'_220 ::
  () ->
  () ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_step'45''8801''45''10216'_220 :: () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_step'45''8801''45''10216'_220
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny -> () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny
 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Function.Related.Propositional.EquationalReasoning._._.step-≡-⟩
d_step'45''8801''45''10217'_222 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_step'45''8801''45''10217'_222 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_step'45''8801''45''10217'_222 ~T_Kind_6
v0 ~()
v1 ~()
v2
  = () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_step'45''8801''45''10217'_222
du_step'45''8801''45''10217'_222 ::
  () ->
  () ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_step'45''8801''45''10217'_222 :: () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_step'45''8801''45''10217'_222
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny -> () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny
 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Function.Related.Propositional.EquationalReasoning._._.step-≡˘
d_step'45''8801''728'_224 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_step'45''8801''728'_224 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_step'45''8801''728'_224 ~T_Kind_6
v0 ~()
v1 ~()
v2 = () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_step'45''8801''728'_224
du_step'45''8801''728'_224 ::
  () ->
  () ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_step'45''8801''728'_224 :: () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_step'45''8801''728'_224
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny -> () -> () -> () -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny
 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''728'_452
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Function.Related.Propositional.EquationalReasoning._.rel1
d_rel1_236 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> () -> ()
d_rel1_236 :: T_Kind_6 -> () -> () -> () -> () -> () -> ()
d_rel1_236 = T_Kind_6 -> () -> () -> () -> () -> () -> ()
forall a. a
erased
-- Function.Related.Propositional.EquationalReasoning._.rel2
d_rel2_238 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> () -> ()
d_rel2_238 :: T_Kind_6 -> () -> () -> () -> () -> () -> ()
d_rel2_238 = T_Kind_6 -> () -> () -> () -> () -> () -> ()
forall a. a
erased
-- Function.Related.Propositional.EquationalReasoning._._.step-∼
d_step'45''8764'_242 ::
  T_Kind_6 ->
  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_step'45''8764'_242 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_step'45''8764'_242 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3 = T_Kind_6 -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du_step'45''8764'_242 T_Kind_6
v0
du_step'45''8764'_242 ::
  T_Kind_6 -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du_step'45''8764'_242 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du_step'45''8764'_242 T_Kind_6
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> ()
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8764'_300
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
-- Function.Related.Propositional.EquationalReasoning._._.step-⤖
d_step'45''10518'_246 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Bijection_926 -> AgdaAny
d_step'45''10518'_246 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Bijection_926
-> AgdaAny
d_step'45''10518'_246 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3 = T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Bijection_926 -> AgdaAny
du_step'45''10518'_246 T_Kind_6
v0
du_step'45''10518'_246 ::
  T_Kind_6 ->
  () ->
  () ->
  () ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Bijection_926 -> AgdaAny
du_step'45''10518'_246 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Bijection_926 -> AgdaAny
du_step'45''10518'_246 T_Kind_6
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Bijection_926
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''10518'_404
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            ((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'__216
              ((T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
              (((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'__216
                 ((T_Kind_6 -> T_Inverse_1960 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
                 ((T_Bijection_926 -> T_Inverse_1960) -> AgdaAny
forall a b. a -> b
coe
                    T_Bijection_926 -> T_Inverse_1960
MAlonzo.Code.Function.Properties.Bijection.du_'10518''8658''8596'_126))))
-- Function.Related.Propositional.EquationalReasoning._._.step-⬻
d_step'45''11067'_248 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Bijection_926 -> AgdaAny
d_step'45''11067'_248 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Bijection_926
-> AgdaAny
d_step'45''11067'_248 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3 = T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Bijection_926 -> AgdaAny
du_step'45''11067'_248 T_Kind_6
v0
du_step'45''11067'_248 ::
  T_Kind_6 ->
  () ->
  () ->
  () ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Bijection_926 -> AgdaAny
du_step'45''11067'_248 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Bijection_926 -> AgdaAny
du_step'45''11067'_248 T_Kind_6
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Bijection_926
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''11067'_406
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            ((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'__216
              ((T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
              (((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'__216
                 ((T_Kind_6 -> T_Inverse_1960 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
                 ((T_Bijection_926 -> T_Inverse_1960) -> AgdaAny
forall a b. a -> b
coe
                    T_Bijection_926 -> T_Inverse_1960
MAlonzo.Code.Function.Properties.Bijection.du_'10518''8658''8596'_126))))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            (T_Bijection_926 -> T_Bijection_926) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Bijection_926 -> T_Bijection_926
MAlonzo.Code.Function.Construct.Symmetry.du_'10518''45'sym_1138
              AgdaAny
v3))
-- Function.Related.Propositional.EquationalReasoning._._.step-↔-⟨
d_step'45''8596''45''10216'_252 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny
d_step'45''8596''45''10216'_252 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Inverse_1960
-> AgdaAny
d_step'45''8596''45''10216'_252 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3
  = T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_1960 -> AgdaAny
du_step'45''8596''45''10216'_252 T_Kind_6
v0
du_step'45''8596''45''10216'_252 ::
  T_Kind_6 ->
  () ->
  () ->
  () ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny
du_step'45''8596''45''10216'_252 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_1960 -> AgdaAny
du_step'45''8596''45''10216'_252 T_Kind_6
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Inverse_1960
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8596''45''10216'_412
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            ((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'__216
              ((T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
              ((T_Kind_6 -> T_Inverse_1960 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            (T_Inverse_1960 -> T_Inverse_1960) -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Symmetry.du_'8596''45'sym_1148))
-- Function.Related.Propositional.EquationalReasoning._._.step-↔-⟩
d_step'45''8596''45''10217'_254 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny
d_step'45''8596''45''10217'_254 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Inverse_1960
-> AgdaAny
d_step'45''8596''45''10217'_254 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3
  = T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_1960 -> AgdaAny
du_step'45''8596''45''10217'_254 T_Kind_6
v0
du_step'45''8596''45''10217'_254 ::
  T_Kind_6 ->
  () ->
  () ->
  () ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny
du_step'45''8596''45''10217'_254 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_1960 -> AgdaAny
du_step'45''8596''45''10217'_254 T_Kind_6
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Inverse_1960
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8596''45''10217'_410
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            ((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'__216
              ((T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
              ((T_Kind_6 -> T_Inverse_1960 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))))
-- Function.Related.Propositional.EquationalReasoning._._._∎
d__'8718'_264 ::
  T_Kind_6 -> MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny
d__'8718'_264 :: T_Kind_6 -> () -> () -> AgdaAny
d__'8718'_264 T_Kind_6
v0 ~()
v1 = T_Kind_6 -> () -> AgdaAny
du__'8718'_264 T_Kind_6
v0
du__'8718'_264 :: T_Kind_6 -> () -> AgdaAny
du__'8718'_264 :: T_Kind_6 -> () -> AgdaAny
du__'8718'_264 T_Kind_6
v0
  = ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> () -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
      (\ AgdaAny
v1 -> (T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny
du_K'45'refl_160 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
-- Function.Related.Propositional.EquationalReasoning._↔⟨⟩_
d__'8596''10216''10217'__268 ::
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> AgdaAny -> AgdaAny
d__'8596''10216''10217'__268 :: T_Kind_6 -> () -> () -> () -> () -> AgdaAny -> AgdaAny
d__'8596''10216''10217'__268 ~T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 AgdaAny
v5
  = AgdaAny -> AgdaAny
du__'8596''10216''10217'__268 AgdaAny
v5
du__'8596''10216''10217'__268 :: AgdaAny -> AgdaAny
du__'8596''10216''10217'__268 :: AgdaAny -> AgdaAny
du__'8596''10216''10217'__268 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Function.Related.Propositional.InducedRelation₁
d_InducedRelation'8321'_276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Kind_6 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d_InducedRelation'8321'_276 :: ()
-> ()
-> ()
-> T_Kind_6
-> (AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
d_InducedRelation'8321'_276 = ()
-> ()
-> ()
-> T_Kind_6
-> (AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
-- Function.Related.Propositional.InducedPreorder₁
d_InducedPreorder'8321'_288 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Kind_6 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_InducedPreorder'8321'_288 :: () -> () -> () -> T_Kind_6 -> (AgdaAny -> ()) -> T_Preorder_132
d_InducedPreorder'8321'_288 ~()
v0 ~()
v1 ~()
v2 T_Kind_6
v3 ~AgdaAny -> ()
v4
  = T_Kind_6 -> T_Preorder_132
du_InducedPreorder'8321'_288 T_Kind_6
v3
du_InducedPreorder'8321'_288 ::
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_InducedPreorder'8321'_288 :: T_Kind_6 -> T_Preorder_132
du_InducedPreorder'8321'_288 T_Kind_6
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_2267
      ((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_4003
         (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
               (T_Kind_6 -> T_Inverse_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 T_Kind_6
v0
                 ((T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny
du_K'45'reflexive_162 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
C_bijection_22))))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))))
-- Function.Related.Propositional.InducedEquivalence₁
d_InducedEquivalence'8321'_362 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_SymmetricKind_86 ->
  (AgdaAny -> ()) -> MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence'8321'_362 :: ()
-> () -> () -> T_SymmetricKind_86 -> (AgdaAny -> ()) -> T_Setoid_44
d_InducedEquivalence'8321'_362 ~()
v0 ~()
v1 ~()
v2 T_SymmetricKind_86
v3 ~AgdaAny -> ()
v4
  = T_SymmetricKind_86 -> T_Setoid_44
du_InducedEquivalence'8321'_362 T_SymmetricKind_86
v3
du_InducedEquivalence'8321'_362 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence'8321'_362 :: T_SymmetricKind_86 -> T_Setoid_44
du_InducedEquivalence'8321'_362 T_SymmetricKind_86
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_733
      (((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_745
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 -> (T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny
du_K'45'refl_160 ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_Kind_6
d_'8970'_'8971'_92 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> (T_SymmetricKind_86 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_SK'45'sym_168 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0)))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
               (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_Kind_6
d_'8970'_'8971'_92 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0)))))
-- Function.Related.Propositional.InducedRelation₂
d_InducedRelation'8322'_370 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d_InducedRelation'8322'_370 :: ()
-> ()
-> ()
-> ()
-> T_Kind_6
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
d_InducedRelation'8322'_370 = ()
-> ()
-> ()
-> ()
-> T_Kind_6
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
-- Function.Related.Propositional.InducedPreorder₂
d_InducedPreorder'8322'_384 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Kind_6 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_InducedPreorder'8322'_384 :: ()
-> ()
-> ()
-> ()
-> T_Kind_6
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Preorder_132
d_InducedPreorder'8322'_384 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Kind_6
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6
  = T_Kind_6 -> T_Preorder_132
du_InducedPreorder'8322'_384 T_Kind_6
v4
du_InducedPreorder'8322'_384 ::
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_InducedPreorder'8322'_384 :: T_Kind_6 -> T_Preorder_132
du_InducedPreorder'8322'_384 T_Kind_6
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_2267
      ((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_4003
         (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
               (T_Kind_6 -> T_Inverse_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> AgdaAny
du_'8596''8658'_82 T_Kind_6
v0
                 ((T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny
du_K'45'reflexive_162 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
C_bijection_22))))
         ((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_6 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 T_Kind_6
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.Propositional.InducedEquivalence₂
d_InducedEquivalence'8322'_466 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence'8322'_466 :: ()
-> ()
-> ()
-> ()
-> T_SymmetricKind_86
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Setoid_44
d_InducedEquivalence'8322'_466 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_SymmetricKind_86
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6
  = T_SymmetricKind_86 -> T_Setoid_44
du_InducedEquivalence'8322'_466 T_SymmetricKind_86
v4
du_InducedEquivalence'8322'_466 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence'8322'_466 :: T_SymmetricKind_86 -> T_Setoid_44
du_InducedEquivalence'8322'_466 T_SymmetricKind_86
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_733
      (((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_745
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 ->
               (T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> AgdaAny
du_K'45'refl_160 ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_Kind_6
d_'8970'_'8971'_92 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> (T_SymmetricKind_86 -> AgdaAny -> AgdaAny)
-> T_SymmetricKind_86 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_SK'45'sym_168 T_SymmetricKind_86
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_6 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_164 (T_SymmetricKind_86 -> T_Kind_6
d_'8970'_'8971'_92 (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
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))))