{-# 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.LeftInverse 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.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Function.Injection
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Setoid
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.LeftInverse._LeftInverseOf_
d__LeftInverseOf__16 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Equality.T_Π_16 ->
  MAlonzo.Code.Function.Equality.T_Π_16 -> ()
d__LeftInverseOf__16 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T_Level_18
d__LeftInverseOf__16 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T_Level_18
forall a. a
erased
-- Function.LeftInverse._RightInverseOf_
d__RightInverseOf__64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Equality.T_Π_16 ->
  MAlonzo.Code.Function.Equality.T_Π_16 -> ()
d__RightInverseOf__64 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T_Level_18
d__RightInverseOf__64 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T_Level_18
forall a. a
erased
-- Function.LeftInverse.LeftInverse
d_LeftInverse_82 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_LeftInverse_82 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_LeftInverse_82
  = C_LeftInverse'46'constructor_4555 MAlonzo.Code.Function.Equality.T_Π_16
                                      MAlonzo.Code.Function.Equality.T_Π_16 (AgdaAny -> AgdaAny)
-- Function.LeftInverse.LeftInverse.to
d_to_102 ::
  T_LeftInverse_82 -> MAlonzo.Code.Function.Equality.T_Π_16
d_to_102 :: T_LeftInverse_82 -> T_Π_16
d_to_102 T_LeftInverse_82
v0
  = case T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v0 of
      C_LeftInverse'46'constructor_4555 T_Π_16
v1 T_Π_16
v2 AgdaAny -> AgdaAny
v3 -> T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v1
      T_LeftInverse_82
_ -> T_Π_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.LeftInverse.LeftInverse.from
d_from_104 ::
  T_LeftInverse_82 -> MAlonzo.Code.Function.Equality.T_Π_16
d_from_104 :: T_LeftInverse_82 -> T_Π_16
d_from_104 T_LeftInverse_82
v0
  = case T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v0 of
      C_LeftInverse'46'constructor_4555 T_Π_16
v1 T_Π_16
v2 AgdaAny -> AgdaAny
v3 -> T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v2
      T_LeftInverse_82
_ -> T_Π_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.LeftInverse.LeftInverse.left-inverse-of
d_left'45'inverse'45'of_106 ::
  T_LeftInverse_82 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_106 :: T_LeftInverse_82 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_106 T_LeftInverse_82
v0
  = case T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v0 of
      C_LeftInverse'46'constructor_4555 T_Π_16
v1 T_Π_16
v2 AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v3
      T_LeftInverse_82
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.LeftInverse.LeftInverse.F._≈_
d__'8776'__110 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> AgdaAny -> AgdaAny -> ()
d__'8776'__110 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__110 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Function.LeftInverse.LeftInverse.T._≈_
d__'8776'__132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> AgdaAny -> AgdaAny -> ()
d__'8776'__132 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__132 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Function.LeftInverse.LeftInverse.injective
d_injective_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_injective_176 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_44
v4 ~T_Setoid_44
v5 T_LeftInverse_82
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_Setoid_44
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_176 T_Setoid_44
v4 T_LeftInverse_82
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_injective_176 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_176 :: T_Setoid_44
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_176 T_Setoid_44
v0 T_LeftInverse_82
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
  = (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         T_Setoid_44
v0 AgdaAny
v2
         ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
            (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
            ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
               (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1)) AgdaAny
v2))
         AgdaAny
v3
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            T_Setoid_44
v0
            ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
               (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
               ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1)) AgdaAny
v2))
            ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
               (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
               ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1)) AgdaAny
v3))
            AgdaAny
v3
            ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
               T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
               T_Setoid_44
v0
               ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
                  ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                     (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1)) AgdaAny
v3))
               AgdaAny
v3 AgdaAny
v3
               (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
               ((T_LeftInverse_82 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_106 T_LeftInverse_82
v1 AgdaAny
v3))
            ((T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d_cong_40 (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
               ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1)) AgdaAny
v2)
               ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1)) AgdaAny
v3)
               AgdaAny
v4))
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
            (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
            ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
               (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
               ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1)) AgdaAny
v2))
            AgdaAny
v2 ((T_LeftInverse_82 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_106 T_LeftInverse_82
v1 AgdaAny
v2)))
-- Function.LeftInverse.LeftInverse.injection
d_injection_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> MAlonzo.Code.Function.Injection.T_Injection_88
d_injection_184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> T_Injection_88
d_injection_184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_44
v4 ~T_Setoid_44
v5 T_LeftInverse_82
v6 = T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88
du_injection_184 T_Setoid_44
v4 T_LeftInverse_82
v6
du_injection_184 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> MAlonzo.Code.Function.Injection.T_Injection_88
du_injection_184 :: T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88
du_injection_184 T_Setoid_44
v0 T_LeftInverse_82
v1
  = (T_Π_16
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88)
-> AgdaAny -> AgdaAny -> T_Injection_88
forall a b. a -> b
coe
      T_Π_16
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88
MAlonzo.Code.Function.Injection.C_Injection'46'constructor_3057
      ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v1)) ((T_Setoid_44
 -> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_176 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0) (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v1))
-- Function.LeftInverse.LeftInverse.equivalence
d_equivalence_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_equivalence_186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> T_Equivalence_16
d_equivalence_186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_LeftInverse_82
v6
  = T_LeftInverse_82 -> T_Equivalence_16
du_equivalence_186 T_LeftInverse_82
v6
du_equivalence_186 ::
  T_LeftInverse_82 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_equivalence_186 :: T_LeftInverse_82 -> T_Equivalence_16
du_equivalence_186 T_LeftInverse_82
v0
  = (T_Π_16 -> T_Π_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.C_Equivalence'46'constructor_433
      ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0)) ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0))
-- Function.LeftInverse.LeftInverse.to-from
d_to'45'from_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_to'45'from_192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_to'45'from_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_44
v4 T_Setoid_44
v5 T_LeftInverse_82
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_192 T_Setoid_44
v4 T_Setoid_44
v5 T_LeftInverse_82
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_to'45'from_192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_to'45'from_192 :: T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_to'45'from_192 T_Setoid_44
v0 T_Setoid_44
v1 T_LeftInverse_82
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (T__IsRelatedTo__26 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
      ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
         T_Setoid_44
v0
         ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
            (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v4)
         ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
            (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2))
            ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
               (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3))
         AgdaAny
v3
         ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
            T_Setoid_44
v0
            ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
               (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2))
               ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3))
            AgdaAny
v3 AgdaAny
v3
            (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
            ((T_LeftInverse_82 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_106 T_LeftInverse_82
v2 AgdaAny
v3))
         ((T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d_cong_40 (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v4
            ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
               (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3)
            ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
               (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v1))
               ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                  (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3)
               AgdaAny
v4 AgdaAny
v5)))
-- Function.LeftInverse.RightInverse
d_RightInverse_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> ()
d_RightInverse_212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Level_18
d_RightInverse_212 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Level_18
forall a. a
erased
-- Function.LeftInverse._↞_
d__'8606'__222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> () -> ()
d__'8606'__222 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18
d__'8606'__222 = T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Function.LeftInverse.leftInverse
d_leftInverse_242 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  T_LeftInverse_82
d_leftInverse_242 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T_LeftInverse_82
d_leftInverse_242 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> T__'8801'__12
v6
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T_LeftInverse_82
du_leftInverse_242 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 AgdaAny -> T__'8801'__12
v6
du_leftInverse_242 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  T_LeftInverse_82
du_leftInverse_242 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T_LeftInverse_82
du_leftInverse_242 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> T__'8801'__12
v2
  = (T_Π_16 -> T_Π_16 -> (AgdaAny -> AgdaAny) -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_LeftInverse_82
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> (AgdaAny -> AgdaAny) -> T_LeftInverse_82
C_LeftInverse'46'constructor_4555
      ((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Relation.Binary.PropositionalEquality.du_'8594''45'to'45''10230'_68
         ((T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
            (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
               AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased))
         AgdaAny -> AgdaAny
v0)
      ((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Relation.Binary.PropositionalEquality.du_'8594''45'to'45''10230'_68
         ((T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
            (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
               AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased))
         AgdaAny -> AgdaAny
v1)
      ((AgdaAny -> T__'8801'__12) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8801'__12
v2)
-- Function.LeftInverse.id
d_id_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82
d_id_256 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_LeftInverse_82
d_id_256 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_LeftInverse_82
du_id_256 T_Setoid_44
v2
du_id_256 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82
du_id_256 :: T_Setoid_44 -> T_LeftInverse_82
du_id_256 T_Setoid_44
v0
  = (T_Π_16 -> T_Π_16 -> (AgdaAny -> AgdaAny) -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_LeftInverse_82
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> (AgdaAny -> AgdaAny) -> T_LeftInverse_82
C_LeftInverse'46'constructor_4555
      (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62)
      (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
              (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
              ((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                 (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62)
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                    (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62) AgdaAny
v1))))
-- Function.LeftInverse._∘_
d__'8728'__280 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
d__'8728'__280 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_82
-> T_LeftInverse_82
-> T_LeftInverse_82
d__'8728'__280 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 T_Setoid_44
v6 ~T_Setoid_44
v7 ~T_Setoid_44
v8 T_LeftInverse_82
v9 T_LeftInverse_82
v10
  = T_Setoid_44
-> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8728'__280 T_Setoid_44
v6 T_LeftInverse_82
v9 T_LeftInverse_82
v10
du__'8728'__280 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8728'__280 :: T_Setoid_44
-> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82
du__'8728'__280 T_Setoid_44
v0 T_LeftInverse_82
v1 T_LeftInverse_82
v2
  = (T_Π_16 -> T_Π_16 -> (AgdaAny -> AgdaAny) -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_LeftInverse_82
forall a b. a -> b
coe
      T_Π_16 -> T_Π_16 -> (AgdaAny -> AgdaAny) -> T_LeftInverse_82
C_LeftInverse'46'constructor_4555
      ((T_Π_16 -> T_Π_16 -> T_Π_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> T_Π_16 -> T_Π_16
MAlonzo.Code.Function.Equality.du__'8728'__82
         ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v1)) ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v2)))
      ((T_Π_16 -> T_Π_16 -> T_Π_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> T_Π_16 -> T_Π_16
MAlonzo.Code.Function.Equality.du__'8728'__82
         ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v2)) ((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v1)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 ->
            T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
              ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
forall a b. a -> b
coe
                 T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
                 T_Setoid_44
v0
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                    (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2))
                    ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                       (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
                       ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                          (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
                          ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                             (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3))))
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                    (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2))
                    ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                       (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3))
                 AgdaAny
v3
                 ((T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__26
 -> AgdaAny
 -> T__IsRelatedTo__26)
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                    T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Setoid.du_step'45''8776'_58
                    T_Setoid_44
v0
                    ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                       (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2))
                       ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                          (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3))
                    AgdaAny
v3 AgdaAny
v3
                    (((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
                       ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                          ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
                       (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
                    ((T_LeftInverse_82 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_106 T_LeftInverse_82
v2 AgdaAny
v3))
                 ((T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d_cong_40 (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2))
                    ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                       (T_LeftInverse_82 -> T_Π_16
d_from_104 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
                       ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                          (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v1))
                          ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                             (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3)))
                    ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                       (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3)
                    ((T_LeftInverse_82 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_82 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_LeftInverse_82 -> AgdaAny -> AgdaAny
d_left'45'inverse'45'of_106 T_LeftInverse_82
v1
                       ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                          (T_LeftInverse_82 -> T_Π_16
d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v2)) AgdaAny
v3))))))