{-# 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_2122 -> AgdaAny
d_'8596''8658'_82 :: () -> () -> () -> () -> T_Kind_6 -> T_Inverse_2122 -> AgdaAny
d_'8596''8658'_82 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Kind_6
v4 = T_Kind_6 -> T_Inverse_2122 -> AgdaAny
du_'8596''8658'_82 T_Kind_6
v4
du_'8596''8658'_82 ::
  T_Kind_6 -> MAlonzo.Code.Function.Bundles.T_Inverse_2122 -> AgdaAny
du_'8596''8658'_82 :: T_Kind_6 -> T_Inverse_2122 -> 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_2122 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                ((AgdaAny -> AgdaAny) -> T_Func_774) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> T_Func_774
MAlonzo.Code.Function.Bundles.du_mk'10230'_2442
                  ((T_Inverse_2122 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2134 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_6
C_reverseImplication_10
        -> (AgdaAny -> AgdaAny) -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                ((AgdaAny -> AgdaAny) -> T_Func_774) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> T_Func_774
MAlonzo.Code.Function.Bundles.du_mk'10230'_2442
                  ((T_Inverse_2122 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2136 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_6
C_equivalence_12
        -> (T_Inverse_2122 -> T_Equivalence_1858) -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_2122 -> T_Equivalence_1858
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8660'_630
      T_Kind_6
C_injection_14
        -> (T_Inverse_2122 -> T_Injection_842) -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_2122 -> T_Injection_842
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8611'_624
      T_Kind_6
C_reverseInjection_16
        -> (AgdaAny -> AgdaAny) -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 ->
                (T_Inverse_2122 -> T_Injection_842) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Inverse_2122 -> T_Injection_842
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8611'_624
                  ((T_Inverse_2122 -> T_Inverse_2122) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Inverse_2122 -> T_Inverse_2122
MAlonzo.Code.Function.Construct.Symmetry.du_inverse_1096 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Kind_6
C_leftInverse_18
        -> (T_Inverse_2122 -> T_RightInverse_2036)
-> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> T_RightInverse_2036
MAlonzo.Code.Function.Bundles.du_rightInverse_2150
      T_Kind_6
C_surjection_20
        -> (T_Inverse_2122 -> T_Surjection_918) -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_2122 -> T_Surjection_918
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8608'_626
      T_Kind_6
C_bijection_22 -> (AgdaAny -> AgdaAny) -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Kind_6
_ -> T_Inverse_2122 -> 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_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_6 -> T_Inverse_2122 -> AgdaAny
du_'8596''8658'_82 T_Kind_6
v0
      (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
MAlonzo.Code.Function.Construct.Identity.du_'8596''45'id_660)
-- 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_774 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_780 (AgdaAny -> T_Func_774
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_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1868 (AgdaAny -> T_Equivalence_1858
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_842 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_850 (AgdaAny -> T_Injection_842
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_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 (AgdaAny -> T_RightInverse_2036
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_918 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_926 (AgdaAny -> T_Surjection_918
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_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2134 (AgdaAny -> T_Inverse_2122
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_774 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_780 (AgdaAny -> T_Func_774
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_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1870 (AgdaAny -> T_Equivalence_1858
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_842 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_850 (AgdaAny -> T_Injection_842
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_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 (AgdaAny -> T_RightInverse_2036
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_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048
                  ((T_Surjection_918 -> T_RightInverse_2036)
-> AgdaAny -> T_RightInverse_2036
forall a b. a -> b
coe
                     T_Surjection_918 -> T_RightInverse_2036
MAlonzo.Code.Function.Properties.Surjection.du_'8608''8658''8618'_160
                     (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_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2136 (AgdaAny -> T_Inverse_2122
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_1858
d_'8658''8660'_148 :: ()
-> ()
-> ()
-> ()
-> T_EquivalenceKind_134
-> AgdaAny
-> T_Equivalence_1858
d_'8658''8660'_148 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_EquivalenceKind_134
v4 = T_EquivalenceKind_134 -> AgdaAny -> T_Equivalence_1858
du_'8658''8660'_148 T_EquivalenceKind_134
v4
du_'8658''8660'_148 ::
  T_EquivalenceKind_134 ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_'8658''8660'_148 :: T_EquivalenceKind_134 -> AgdaAny -> T_Equivalence_1858
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_1858
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_EquivalenceKind_134
C_leftInverse_138
        -> (T_RightInverse_2036 -> T_Equivalence_1858)
-> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe T_RightInverse_2036 -> T_Equivalence_1858
MAlonzo.Code.Function.Bundles.du_equivalence_2118
      T_EquivalenceKind_134
C_surjection_140
        -> (T_Surjection_918 -> T_Equivalence_1858)
-> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe
             T_Surjection_918 -> T_Equivalence_1858
MAlonzo.Code.Function.Properties.Surjection.du_'8608''8658''8660'_242
      T_EquivalenceKind_134
C_bijection_142
        -> (T_Inverse_2122 -> T_Equivalence_1858)
-> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe
             T_Inverse_2122 -> T_Equivalence_1858
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8660'_630
      T_EquivalenceKind_134
_ -> AgdaAny -> T_Equivalence_1858
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_1858 -> T_Equivalence_1858) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Equivalence_1858 -> T_Equivalence_1858
MAlonzo.Code.Function.Construct.Symmetry.du_'8660''45'sym_1190
      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_2036 -> T_Surjection_918) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_RightInverse_2036 -> T_Surjection_918
MAlonzo.Code.Function.Properties.RightInverse.du_'8618''8658''8608'_418
      T_Kind_6
C_surjection_20
        -> (T_Surjection_918 -> T_RightInverse_2036) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Surjection_918 -> T_RightInverse_2036
MAlonzo.Code.Function.Properties.Surjection.du_'8608''8658''8618'_160
      T_Kind_6
C_bijection_22
        -> (T_Inverse_2122 -> T_Inverse_2122) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_2122 -> T_Inverse_2122
MAlonzo.Code.Function.Construct.Symmetry.du_'8596''45'sym_1196
      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_774 -> AgdaAny
forall a b. a -> b
coe
             T_Func_774
MAlonzo.Code.Function.Construct.Identity.du_'10230''45'id_646
      T_Kind_6
C_reverseImplication_10
        -> T_Func_774 -> AgdaAny
forall a b. a -> b
coe
             T_Func_774
MAlonzo.Code.Function.Construct.Identity.du_'10230''45'id_646
      T_Kind_6
C_equivalence_12
        -> T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
MAlonzo.Code.Function.Construct.Identity.du_'8660''45'id_654
      T_Kind_6
C_injection_14
        -> T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
MAlonzo.Code.Function.Construct.Identity.du_'8611''45'id_648
      T_Kind_6
C_reverseInjection_16
        -> T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
MAlonzo.Code.Function.Construct.Identity.du_'8611''45'id_648
      T_Kind_6
C_leftInverse_18
        -> T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
MAlonzo.Code.Function.Construct.Identity.du_'8618''45'id_658
      T_Kind_6
C_surjection_20
        -> T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
MAlonzo.Code.Function.Construct.Identity.du_'8608''45'id_650
      T_Kind_6
C_bijection_22
        -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
MAlonzo.Code.Function.Construct.Identity.du_'8596''45'id_660
      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_774 -> T_Func_774 -> T_Func_774)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Func_774 -> T_Func_774 -> T_Func_774
MAlonzo.Code.Function.Construct.Composition.du__'10230''45''8728'__2496
                  (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_774 -> T_Func_774 -> T_Func_774)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Func_774 -> T_Func_774 -> T_Func_774
MAlonzo.Code.Function.Construct.Composition.du__'10230''45''8728'__2496
      T_Kind_6
C_equivalence_12
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
MAlonzo.Code.Function.Construct.Composition.du__'8660''45''8728'__2504
                  (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_842 -> T_Injection_842 -> T_Injection_842)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Injection_842 -> T_Injection_842 -> T_Injection_842
MAlonzo.Code.Function.Construct.Composition.du__'8611''45''8728'__2498
                  (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_842 -> T_Injection_842 -> T_Injection_842)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Injection_842 -> T_Injection_842 -> T_Injection_842
MAlonzo.Code.Function.Construct.Composition.du__'8611''45''8728'__2498
      T_Kind_6
C_leftInverse_18
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v1 AgdaAny
v2 ->
                (T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036
MAlonzo.Code.Function.Construct.Composition.du__'8618''45''8728'__2508
                  (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_918 -> T_Surjection_918 -> T_Surjection_918)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918
MAlonzo.Code.Function.Construct.Composition.du__'8608''45''8728'__2500
                  (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_2122 -> T_Inverse_2122 -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
MAlonzo.Code.Function.Construct.Composition.du__'8596''45''8728'__2510
                  (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_28
d_SK'45'isEquivalence_172 :: () -> T_SymmetricKind_86 -> T_IsEquivalence_28
d_SK'45'isEquivalence_172 ~()
v0 T_SymmetricKind_86
v1 = T_SymmetricKind_86 -> T_IsEquivalence_28
du_SK'45'isEquivalence_172 T_SymmetricKind_86
v1
du_SK'45'isEquivalence_172 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
du_SK'45'isEquivalence_172 :: T_SymmetricKind_86 -> T_IsEquivalence_28
du_SK'45'isEquivalence_172 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
      (\ AgdaAny
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_46
d_SK'45'setoid_178 :: T_SymmetricKind_86 -> () -> T_Setoid_46
d_SK'45'setoid_178 T_SymmetricKind_86
v0 ~()
v1 = T_SymmetricKind_86 -> T_Setoid_46
du_SK'45'setoid_178 T_SymmetricKind_86
v0
du_SK'45'setoid_178 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du_SK'45'setoid_178 :: T_SymmetricKind_86 -> T_Setoid_46
du_SK'45'setoid_178 T_SymmetricKind_86
v0
  = (T_IsEquivalence_28 -> T_Setoid_46) -> AgdaAny -> T_Setoid_46
forall a b. a -> b
coe
      T_IsEquivalence_28 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_84
      ((T_SymmetricKind_86 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsEquivalence_28
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_76
d_K'45'isPreorder_186 :: () -> T_Kind_6 -> T_IsPreorder_76
d_K'45'isPreorder_186 ~()
v0 T_Kind_6
v1 = T_Kind_6 -> T_IsPreorder_76
du_K'45'isPreorder_186 T_Kind_6
v1
du_K'45'isPreorder_186 ::
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_K'45'isPreorder_186 :: T_Kind_6 -> T_IsPreorder_76
du_K'45'isPreorder_186 T_Kind_6
v0
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      ((T_SymmetricKind_86 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsEquivalence_28
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_2122 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_2122 -> 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_142
d_K'45'preorder_192 :: T_Kind_6 -> () -> T_Preorder_142
d_K'45'preorder_192 T_Kind_6
v0 ~()
v1 = T_Kind_6 -> T_Preorder_142
du_K'45'preorder_192 T_Kind_6
v0
du_K'45'preorder_192 ::
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_K'45'preorder_192 :: T_Kind_6 -> T_Preorder_142
du_K'45'preorder_192 T_Kind_6
v0
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_Kind_6 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_IsPreorder_76
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'_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._._.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'_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''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'_438
      ((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'_454
      ((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'_302
      (\ 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_1004 -> AgdaAny
d_step'45''10518'_246 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Bijection_1004
-> AgdaAny
d_step'45''10518'_246 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3 = T_Kind_6
-> () -> () -> () -> AgdaAny -> T_Bijection_1004 -> 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_1004 -> AgdaAny
du_step'45''10518'_246 :: T_Kind_6
-> () -> () -> () -> AgdaAny -> T_Bijection_1004 -> 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_1004
-> 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'_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_2122 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_2122 -> AgdaAny
du_'8596''8658'_82 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
                 ((T_Bijection_1004 -> T_Inverse_2122) -> AgdaAny
forall a b. a -> b
coe
                    T_Bijection_1004 -> T_Inverse_2122
MAlonzo.Code.Function.Properties.Bijection.du_'10518''8658''8596'_130))))
-- 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_1004 -> AgdaAny
d_step'45''11067'_248 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Bijection_1004
-> AgdaAny
d_step'45''11067'_248 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3 = T_Kind_6
-> () -> () -> () -> AgdaAny -> T_Bijection_1004 -> 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_1004 -> AgdaAny
du_step'45''11067'_248 :: T_Kind_6
-> () -> () -> () -> AgdaAny -> T_Bijection_1004 -> 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_1004
-> 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'_408
      ((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_2122 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_2122 -> AgdaAny
du_'8596''8658'_82 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0))
                 ((T_Bijection_1004 -> T_Inverse_2122) -> AgdaAny
forall a b. a -> b
coe
                    T_Bijection_1004 -> T_Inverse_2122
MAlonzo.Code.Function.Properties.Bijection.du_'10518''8658''8596'_130))))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            (T_Bijection_1004 -> T_Bijection_1004) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Bijection_1004 -> T_Bijection_1004
MAlonzo.Code.Function.Construct.Symmetry.du_'10518''45'sym_1186
              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_2122 -> AgdaAny
d_step'45''8596''45''10216'_252 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Inverse_2122
-> AgdaAny
d_step'45''8596''45''10216'_252 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3
  = T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_2122 -> 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_2122 -> AgdaAny
du_step'45''8596''45''10216'_252 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_2122 -> 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_2122
-> 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'_414
      ((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_2122 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_2122 -> 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_2122 -> T_Inverse_2122) -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_2122 -> T_Inverse_2122
MAlonzo.Code.Function.Construct.Symmetry.du_'8596''45'sym_1196))
-- 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_2122 -> AgdaAny
d_step'45''8596''45''10217'_254 :: T_Kind_6
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> AgdaAny
-> T_Inverse_2122
-> AgdaAny
d_step'45''8596''45''10217'_254 T_Kind_6
v0 ~()
v1 ~()
v2 ~()
v3
  = T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_2122 -> 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_2122 -> AgdaAny
du_step'45''8596''45''10217'_254 :: T_Kind_6 -> () -> () -> () -> AgdaAny -> T_Inverse_2122 -> 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_2122
-> 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'_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_2122 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_6 -> T_Inverse_2122 -> 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'_494
      (\ 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_142
d_InducedPreorder'8321'_288 :: () -> () -> () -> T_Kind_6 -> (AgdaAny -> ()) -> T_Preorder_142
d_InducedPreorder'8321'_288 ~()
v0 ~()
v1 ~()
v2 T_Kind_6
v3 ~AgdaAny -> ()
v4
  = T_Kind_6 -> T_Preorder_142
du_InducedPreorder'8321'_288 T_Kind_6
v3
du_InducedPreorder'8321'_288 ::
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_InducedPreorder'8321'_288 :: T_Kind_6 -> T_Preorder_142
du_InducedPreorder'8321'_288 T_Kind_6
v0
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
         (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28
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_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_2122 -> 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'_370 ::
  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_46
d_InducedEquivalence'8321'_370 :: ()
-> () -> () -> T_SymmetricKind_86 -> (AgdaAny -> ()) -> T_Setoid_46
d_InducedEquivalence'8321'_370 ~()
v0 ~()
v1 ~()
v2 T_SymmetricKind_86
v3 ~AgdaAny -> ()
v4
  = T_SymmetricKind_86 -> T_Setoid_46
du_InducedEquivalence'8321'_370 T_SymmetricKind_86
v3
du_InducedEquivalence'8321'_370 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du_InducedEquivalence'8321'_370 :: T_SymmetricKind_86 -> T_Setoid_46
du_InducedEquivalence'8321'_370 T_SymmetricKind_86
v0
  = (T_IsEquivalence_28 -> T_Setoid_46) -> AgdaAny -> T_Setoid_46
forall a b. a -> b
coe
      T_IsEquivalence_28 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_84
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
         ((AgdaAny -> AgdaAny) -> AgdaAny
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'_378 ::
  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'_378 :: ()
-> ()
-> ()
-> ()
-> T_Kind_6
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
d_InducedRelation'8322'_378 = ()
-> ()
-> ()
-> ()
-> T_Kind_6
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
-- Function.Related.Propositional.InducedPreorder₂
d_InducedPreorder'8322'_392 ::
  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_142
d_InducedPreorder'8322'_392 :: ()
-> ()
-> ()
-> ()
-> T_Kind_6
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Preorder_142
d_InducedPreorder'8322'_392 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Kind_6
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6
  = T_Kind_6 -> T_Preorder_142
du_InducedPreorder'8322'_392 T_Kind_6
v4
du_InducedPreorder'8322'_392 ::
  T_Kind_6 -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_InducedPreorder'8322'_392 :: T_Kind_6 -> T_Preorder_142
du_InducedPreorder'8322'_392 T_Kind_6
v0
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
         (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28
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_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_2122 -> 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'_482 ::
  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_46
d_InducedEquivalence'8322'_482 :: ()
-> ()
-> ()
-> ()
-> T_SymmetricKind_86
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Setoid_46
d_InducedEquivalence'8322'_482 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_SymmetricKind_86
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6
  = T_SymmetricKind_86 -> T_Setoid_46
du_InducedEquivalence'8322'_482 T_SymmetricKind_86
v4
du_InducedEquivalence'8322'_482 ::
  T_SymmetricKind_86 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
du_InducedEquivalence'8322'_482 :: T_SymmetricKind_86 -> T_Setoid_46
du_InducedEquivalence'8322'_482 T_SymmetricKind_86
v0
  = (T_IsEquivalence_28 -> T_Setoid_46) -> AgdaAny -> T_Setoid_46
forall a b. a -> b
coe
      T_IsEquivalence_28 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_84
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
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))))