{-# 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.Data.Product.Function.Dependent.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.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Function.Bijection
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Function.HalfAdjointEquivalence
import qualified MAlonzo.Code.Function.Injection
import qualified MAlonzo.Code.Function.Inverse
import qualified MAlonzo.Code.Function.LeftInverse
import qualified MAlonzo.Code.Function.Related
import qualified MAlonzo.Code.Function.Surjection
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
d_'8660'_36 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_'8660'_36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Equivalence_16
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_16
d_'8660'_36 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Equivalence_16
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny
v10
= T_Equivalence_16
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_16
du_'8660'_36 T_Equivalence_16
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny
v10
du_'8660'_36 ::
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_'8660'_36 :: T_Equivalence_16
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_16
du_'8660'_36 T_Equivalence_16
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny
v2
= ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_equivalence_56
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1))
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v2))
d_'8660''45''8608'_52 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16) ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_'8660''45''8608'_52 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Surjection_54
-> (AgdaAny -> T_Equivalence_16)
-> T_Equivalence_16
d_'8660''45''8608'_52 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_54
v8 AgdaAny -> T_Equivalence_16
v9
= T_Surjection_54
-> (AgdaAny -> T_Equivalence_16) -> T_Equivalence_16
du_'8660''45''8608'_52 T_Surjection_54
v8 AgdaAny -> T_Equivalence_16
v9
du_'8660''45''8608'_52 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16) ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_'8660''45''8608'_52 :: T_Surjection_54
-> (AgdaAny -> T_Equivalence_16) -> T_Equivalence_16
du_'8660''45''8608'_52 T_Surjection_54
v0 AgdaAny -> T_Equivalence_16
v1
= ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_equivalence_56
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Surjection_54 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_to_72 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v2 ->
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34 ((AgdaAny -> T_Equivalence_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Equivalence_16
v1 AgdaAny
v2)))))
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Surjective_18 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0))))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
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_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
((AgdaAny -> T_Equivalence_16) -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
AgdaAny -> T_Equivalence_16
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_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> T_Surjective_18
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0)))
AgdaAny
v2)))
AgdaAny
v3)))
d_'8611'_70 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
MAlonzo.Code.Function.Injection.T_Injection_88
d_'8611'_70 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> T_Injection_88
d_'8611'_70 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 AgdaAny -> T_Injection_88
v9
= T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Injection_88
du_'8611'_70 T_Inverse_58
v8 AgdaAny -> T_Injection_88
v9
du_'8611'_70 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
MAlonzo.Code.Function.Injection.T_Injection_88
du_'8611'_70 :: T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Injection_88
du_'8611'_70 T_Inverse_58
v0 AgdaAny -> T_Injection_88
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> T_Injection_88)
-> AgdaAny -> AgdaAny -> T_Injection_88
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> T_Injection_88
MAlonzo.Code.Function.Injection.du_injection_140
((T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Σ_14 -> T_Σ_14
du_to_172 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0) ((AgdaAny -> T_Injection_88) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Injection_88
v1)) AgdaAny
forall a. a
erased
d_A'8321''8771'A'8322'_80 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
MAlonzo.Code.Function.HalfAdjointEquivalence.T__'8771'__12
d_A'8321''8771'A'8322'_80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> T__'8771'__12
d_A'8321''8771'A'8322'_80 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 ~AgdaAny -> T_Injection_88
v9
= T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_80 T_Inverse_58
v8
du_A'8321''8771'A'8322'_80 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.HalfAdjointEquivalence.T__'8771'__12
du_A'8321''8771'A'8322'_80 :: T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_80 T_Inverse_58
v0
= (T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> T__'8771'__12
forall a b. a -> b
coe
T_Inverse_58 -> T__'8771'__12
MAlonzo.Code.Function.HalfAdjointEquivalence.du_'8596''8594''8771'_80
(T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0)
d_from_84 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
AgdaAny -> AgdaAny
d_from_84 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
d_from_84 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 ~AgdaAny -> T_Injection_88
v9 = T_Inverse_58 -> AgdaAny -> AgdaAny
du_from_84 T_Inverse_58
v8
du_from_84 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny -> AgdaAny
du_from_84 :: T_Inverse_58 -> AgdaAny -> AgdaAny
du_from_84 T_Inverse_58
v0
= (T__'8771'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8771'__12 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.HalfAdjointEquivalence.d_from_40
((T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_80 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0))
d_to_96 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
AgdaAny -> AgdaAny
d_to_96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
d_to_96 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 ~AgdaAny -> T_Injection_88
v9 = T_Inverse_58 -> AgdaAny -> AgdaAny
du_to_96 T_Inverse_58
v8
du_to_96 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny -> AgdaAny
du_to_96 :: T_Inverse_58 -> AgdaAny -> AgdaAny
du_to_96 T_Inverse_58
v0
= (T__'8771'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8771'__12 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.HalfAdjointEquivalence.d_to_38
((T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_80 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0))
d_subst'45'application'8242'_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 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'application'8242'_110 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_subst'45'application'8242'_110 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_from_128 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> AgdaAny
d_from_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d_from_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 ~AgdaAny -> T_Injection_88
v9 ~AgdaAny
v10 ~AgdaAny
v11 ~AgdaAny
v12
~AgdaAny -> AgdaAny -> AgdaAny
v13 ~T__'8801'__12
v14
= T_Inverse_58 -> AgdaAny -> AgdaAny
du_from_128 T_Inverse_58
v8
du_from_128 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny -> AgdaAny
du_from_128 :: T_Inverse_58 -> AgdaAny -> AgdaAny
du_from_128 T_Inverse_58
v0
= (T__'8771'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8771'__12 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.HalfAdjointEquivalence.d_from_40
((T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_80 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0))
d_to_140 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> AgdaAny
d_to_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d_to_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 ~AgdaAny -> T_Injection_88
v9 ~AgdaAny
v10 ~AgdaAny
v11 ~AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny
v13
~T__'8801'__12
v14
= T_Inverse_58 -> AgdaAny -> AgdaAny
du_to_140 T_Inverse_58
v8
du_to_140 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny -> AgdaAny
du_to_140 :: T_Inverse_58 -> AgdaAny -> AgdaAny
du_to_140 T_Inverse_58
v0
= (T__'8771'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8771'__12 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.HalfAdjointEquivalence.d_to_38
((T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_80 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0))
d_g'8242'_144 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> AgdaAny -> AgdaAny
d_g'8242'_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_g'8242'_144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 ~AgdaAny -> T_Injection_88
v9 ~AgdaAny
v10 ~AgdaAny
v11 ~AgdaAny
v12
AgdaAny -> AgdaAny -> AgdaAny
v13 ~T__'8801'__12
v14 AgdaAny
v15 AgdaAny
v16
= T_Inverse_58
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_g'8242'_144 T_Inverse_58
v8 AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v15 AgdaAny
v16
du_g'8242'_144 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_g'8242'_144 :: T_Inverse_58
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_g'8242'_144 T_Inverse_58
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
= (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
v1
((T__'8771'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8771'__12 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.HalfAdjointEquivalence.d_from_40
((T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_80 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0)) AgdaAny
v2)
AgdaAny
v3
d_g'8242''45'lemma_152 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_g'8242''45'lemma_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
d_g'8242''45'lemma_152 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_lemma_168 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemma_168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_lemma_168 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_to_172 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to_172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> T_Σ_14
-> T_Σ_14
d_to_172 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 AgdaAny -> T_Injection_88
v9 = T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Σ_14 -> T_Σ_14
du_to_172 T_Inverse_58
v8 AgdaAny -> T_Injection_88
v9
du_to_172 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to_172 :: T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Σ_14 -> T_Σ_14
du_to_172 T_Inverse_58
v0 AgdaAny -> T_Injection_88
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T__'8771'__12 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8771'__12 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.HalfAdjointEquivalence.d_to_38
((T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_80 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v2 ->
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Injection_88 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Injection_88 -> T_Π_16
MAlonzo.Code.Function.Injection.d_to_106 ((AgdaAny -> T_Injection_88) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Injection_88
v1 AgdaAny
v2))))
d_to'45'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 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Injection.T_Injection_88) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_to'45'injective_176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_to'45'injective_176 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Injection_88)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_'8606'_214 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
(AgdaAny -> MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82) ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
d_'8606'_214 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82)
-> T_LeftInverse_82
d_'8606'_214 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_LeftInverse_82
v8 AgdaAny -> T_LeftInverse_82
v9
= T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_LeftInverse_82
du_'8606'_214 T_LeftInverse_82
v8 AgdaAny -> T_LeftInverse_82
v9
du_'8606'_214 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
(AgdaAny -> MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82) ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82
du_'8606'_214 :: T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_LeftInverse_82
du_'8606'_214 T_LeftInverse_82
v0 AgdaAny -> T_LeftInverse_82
v1
= (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
MAlonzo.Code.Function.LeftInverse.C_LeftInverse'46'constructor_4555
((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> 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))
((T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14
du_to_230 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0) ((AgdaAny -> T_LeftInverse_82) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_LeftInverse_82
v1)))
((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> 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))
((T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14
du_from_224 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0) ((AgdaAny -> T_LeftInverse_82) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_LeftInverse_82
v1)))
AgdaAny
forall a. a
erased
d_from_224 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
(AgdaAny -> MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_from_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82)
-> T_Σ_14
-> T_Σ_14
d_from_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_LeftInverse_82
v8 AgdaAny -> T_LeftInverse_82
v9
= T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14
du_from_224 T_LeftInverse_82
v8 AgdaAny -> T_LeftInverse_82
v9
du_from_224 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
(AgdaAny -> MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_224 :: T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14
du_from_224 T_LeftInverse_82
v0 AgdaAny -> T_LeftInverse_82
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> 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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_from_104 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v2 ->
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_LeftInverse_82 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_from_104 ((AgdaAny -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_LeftInverse_82
v1 AgdaAny
v2))))
d_to_230 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
(AgdaAny -> MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82)
-> T_Σ_14
-> T_Σ_14
d_to_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_LeftInverse_82
v8 AgdaAny -> T_LeftInverse_82
v9 = T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14
du_to_230 T_LeftInverse_82
v8 AgdaAny -> T_LeftInverse_82
v9
du_to_230 ::
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
(AgdaAny -> MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to_230 :: T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_Σ_14 -> T_Σ_14
du_to_230 T_LeftInverse_82
v0 AgdaAny -> T_LeftInverse_82
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> 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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82 -> T_Π_16
MAlonzo.Code.Function.LeftInverse.d_to_102 (T_LeftInverse_82 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_82
v0)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
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
MAlonzo.Code.Function.LeftInverse.d_to_102
((AgdaAny -> T_LeftInverse_82) -> AgdaAny -> T_LeftInverse_82
forall a b. a -> b
coe
AgdaAny -> 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
MAlonzo.Code.Function.LeftInverse.d_to_102 (T_LeftInverse_82 -> T_LeftInverse_82
forall a b. a -> b
coe T_LeftInverse_82
v0)) AgdaAny
v2)))
AgdaAny
v3))
d_left'45'inverse'45'of_240 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82 ->
(AgdaAny -> MAlonzo.Code.Function.LeftInverse.T_LeftInverse_82) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_left'45'inverse'45'of_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82)
-> T_Σ_14
-> T__'8801'__12
d_left'45'inverse'45'of_240 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82)
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
d_'8608'_250 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Surjection.T_Surjection_54) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
d_'8608'_250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Surjection_54
-> (AgdaAny -> T_Surjection_54)
-> T_Surjection_54
d_'8608'_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_54
v8 AgdaAny -> T_Surjection_54
v9
= T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Surjection_54
du_'8608'_250 T_Surjection_54
v8 AgdaAny -> T_Surjection_54
v9
du_'8608'_250 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Surjection.T_Surjection_54) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
du_'8608'_250 :: T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Surjection_54
du_'8608'_250 T_Surjection_54
v0 AgdaAny -> T_Surjection_54
v1
= (T_Π_16 -> T_Surjective_18 -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> T_Surjection_54
forall a b. a -> b
coe
T_Π_16 -> T_Surjective_18 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.C_Surjection'46'constructor_2369
((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> 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))
((T_Surjection_54
-> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14
du_to_260 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0) ((AgdaAny -> T_Surjection_54) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Surjection_54
v1)))
((T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> (AgdaAny -> AgdaAny) -> T_Surjective_18
MAlonzo.Code.Function.Surjection.C_Surjective'46'constructor_1229
((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> 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))
((T_Surjection_54
-> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14
du_from_266 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0) ((AgdaAny -> T_Surjection_54) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Surjection_54
v1)))
AgdaAny
forall a. a
erased)
d_to_260 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Surjection.T_Surjection_54) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Surjection_54
-> (AgdaAny -> T_Surjection_54)
-> T_Σ_14
-> T_Σ_14
d_to_260 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_54
v8 AgdaAny -> T_Surjection_54
v9 = T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14
du_to_260 T_Surjection_54
v8 AgdaAny -> T_Surjection_54
v9
du_to_260 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Surjection.T_Surjection_54) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to_260 :: T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14
du_to_260 T_Surjection_54
v0 AgdaAny -> T_Surjection_54
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Surjection_54 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_to_72 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v2 ->
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Surjection_54 -> T_Π_16) -> AgdaAny -> T_Π_16
forall a b. a -> b
coe T_Surjection_54 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_to_72 ((AgdaAny -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Surjection_54
v1 AgdaAny
v2))))
d_from_266 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Surjection.T_Surjection_54) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_from_266 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Surjection_54
-> (AgdaAny -> T_Surjection_54)
-> T_Σ_14
-> T_Σ_14
d_from_266 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_54
v8 AgdaAny -> T_Surjection_54
v9
= T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14
du_from_266 T_Surjection_54
v8 AgdaAny -> T_Surjection_54
v9
du_from_266 ::
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Surjection.T_Surjection_54) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_266 :: T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Σ_14 -> T_Σ_14
du_from_266 T_Surjection_54
v0 AgdaAny -> T_Surjection_54
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Surjective_18 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0))))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
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_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> T_Surjective_18
forall a b. a -> b
coe
T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74
((AgdaAny -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Surjection_54
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_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> T_Surjective_18
forall a b. a -> b
coe T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74 (T_Surjection_54 -> AgdaAny
forall a b. a -> b
coe T_Surjection_54
v0)))
AgdaAny
v2))))
AgdaAny
v3))
d_right'45'inverse'45'of_276 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54 ->
(AgdaAny -> MAlonzo.Code.Function.Surjection.T_Surjection_54) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_right'45'inverse'45'of_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Surjection_54
-> (AgdaAny -> T_Surjection_54)
-> T_Σ_14
-> T__'8801'__12
d_right'45'inverse'45'of_276 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Surjection_54
-> (AgdaAny -> T_Surjection_54)
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
d_'8596'_286 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Inverse.T_Inverse_58) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'8596'_286 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Inverse_58)
-> T_Inverse_58
d_'8596'_286 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 AgdaAny -> T_Inverse_58
v9
= T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Inverse_58
du_'8596'_286 T_Inverse_58
v8 AgdaAny -> T_Inverse_58
v9
du_'8596'_286 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Inverse.T_Inverse_58) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'8596'_286 :: T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Inverse_58
du_'8596'_286 T_Inverse_58
v0 AgdaAny -> T_Inverse_58
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Surjection_54 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Surjection_54 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_to_72
((T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Surjection_54
du_surjection'8242'_298 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0) ((AgdaAny -> T_Inverse_58) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Inverse_58
v1))))
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Surjective_18 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Surjective_18 -> T_Π_16
MAlonzo.Code.Function.Surjection.d_from_38
((T_Surjection_54 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Surjection_54 -> T_Surjective_18
MAlonzo.Code.Function.Surjection.d_surjective_74
((T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Surjection_54
du_surjection'8242'_298 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0) ((AgdaAny -> T_Inverse_58) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Inverse_58
v1)))))
AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
d_A'8321''8771'A'8322'_296 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Inverse.T_Inverse_58) ->
MAlonzo.Code.Function.HalfAdjointEquivalence.T__'8771'__12
d_A'8321''8771'A'8322'_296 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Inverse_58)
-> T__'8771'__12
d_A'8321''8771'A'8322'_296 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 ~AgdaAny -> T_Inverse_58
v9
= T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_296 T_Inverse_58
v8
du_A'8321''8771'A'8322'_296 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
MAlonzo.Code.Function.HalfAdjointEquivalence.T__'8771'__12
du_A'8321''8771'A'8322'_296 :: T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_296 T_Inverse_58
v0
= (T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> T__'8771'__12
forall a b. a -> b
coe
T_Inverse_58 -> T__'8771'__12
MAlonzo.Code.Function.HalfAdjointEquivalence.du_'8596''8594''8771'_80
(T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0)
d_surjection'8242'_298 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Inverse.T_Inverse_58) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
d_surjection'8242'_298 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Inverse_58)
-> T_Surjection_54
d_surjection'8242'_298 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_58
v8 AgdaAny -> T_Inverse_58
v9
= T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Surjection_54
du_surjection'8242'_298 T_Inverse_58
v8 AgdaAny -> T_Inverse_58
v9
du_surjection'8242'_298 ::
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Inverse.T_Inverse_58) ->
MAlonzo.Code.Function.Surjection.T_Surjection_54
du_surjection'8242'_298 :: T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Surjection_54
du_surjection'8242'_298 T_Inverse_58
v0 AgdaAny -> T_Inverse_58
v1
= (T_Surjection_54
-> (AgdaAny -> T_Surjection_54) -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> T_Surjection_54
forall a b. a -> b
coe
T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Surjection_54
du_'8608'_250
((T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Bijection_64 -> T_Surjection_54
MAlonzo.Code.Function.Bijection.du_surjection_100
((T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98
(T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
((T__'8771'__12 -> T_Inverse_58) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8771'__12 -> T_Inverse_58
MAlonzo.Code.Function.HalfAdjointEquivalence.du_inverse_54
((T_Inverse_58 -> T__'8771'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T__'8771'__12
du_A'8321''8771'A'8322'_296 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
v0)))))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v2 ->
(T_Bijection_64 -> T_Surjection_54) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Bijection_64 -> T_Surjection_54
MAlonzo.Code.Function.Bijection.du_surjection_100
((T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98
(T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
((AgdaAny -> T_Inverse_58) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Inverse_58
v1 AgdaAny
v2))))
d_left'45'inverse'45'of_302 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> MAlonzo.Code.Function.Inverse.T_Inverse_58) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_left'45'inverse'45'of_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Inverse_58)
-> T_Σ_14
-> T__'8801'__12
d_left'45'inverse'45'of_302 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> T_Inverse_58)
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
d_swap'45'coercions_344 ::
MAlonzo.Code.Function.Related.T_Kind_52 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_swap'45'coercions_344 :: T_Kind_52
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_swap'45'coercions_344 T_Kind_52
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 ~AgdaAny -> T_Level_18
v8 T_Inverse_58
v9 AgdaAny -> AgdaAny
v10
AgdaAny
v11
= T_Kind_52
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_swap'45'coercions_344 T_Kind_52
v0 T_Inverse_58
v9 AgdaAny -> AgdaAny
v10 AgdaAny
v11
du_swap'45'coercions_344 ::
MAlonzo.Code.Function.Related.T_Kind_52 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_swap'45'coercions_344 :: T_Kind_52
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_swap'45'coercions_344 T_Kind_52
v0 T_Inverse_58
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3
= (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du__'8764''10216'_'10217'__340
(T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0)
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> 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_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_from_80 (T_Inverse_58 -> T_Inverse_58
forall a b. a -> b
coe T_Inverse_58
v1)) AgdaAny
v3))
((T_Kind_52 -> T_Inverse_58 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_52 -> T_Inverse_58 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du__'8596''10216'_'10217'__360
(T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0)
((T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Kind_52 -> AgdaAny
MAlonzo.Code.Function.Related.du_K'45'reflexive_260
(T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
MAlonzo.Code.Function.Related.C_bijection_68))
((T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52 -> AgdaAny
MAlonzo.Code.Function.Related.du__'8718'_410 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0)))
d_cong_384 ::
MAlonzo.Code.Function.Related.T_Kind_52 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> AgdaAny) -> AgdaAny
d_cong_384 :: T_Kind_52
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
-> (AgdaAny -> AgdaAny)
-> AgdaAny
d_cong_384 T_Kind_52
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 ~AgdaAny -> T_Level_18
v8 = T_Kind_52 -> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
du_cong_384 T_Kind_52
v0
du_cong_384 ::
MAlonzo.Code.Function.Related.T_Kind_52 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
(AgdaAny -> AgdaAny) -> AgdaAny
du_cong_384 :: T_Kind_52 -> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
du_cong_384 T_Kind_52
v0
= case T_Kind_52 -> T_Kind_52
forall a b. a -> b
coe T_Kind_52
v0 of
T_Kind_52
MAlonzo.Code.Function.Related.C_implication_54
-> (AgdaAny -> AgdaAny)
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 ->
((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Inverse_58 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_to_78 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
T_Kind_52
MAlonzo.Code.Function.Related.C_reverse'45'implication_56
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 AgdaAny
v2 ->
((AgdaAny -> AgdaAny) -> T__'8592'__12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T__'8592'__12
MAlonzo.Code.Function.Related.C_lam_26
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Inverse_58 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_from_80 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 ->
T__'8592'__12 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.d_app'45''8592'_24
((T_Kind_52
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8592'__12
forall a b. a -> b
coe
T_Kind_52
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_swap'45'coercions_344 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))))
T_Kind_52
MAlonzo.Code.Function.Related.C_equivalence_58
-> (AgdaAny -> AgdaAny)
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 ->
(T_Surjection_54
-> (AgdaAny -> T_Equivalence_16) -> T_Equivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Surjection_54
-> (AgdaAny -> T_Equivalence_16) -> T_Equivalence_16
du_'8660''45''8608'_52
((T_Π_16 -> T_Surjective_18 -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> T_Surjective_18 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.C_Surjection'46'constructor_2369
((T_Inverse_58 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_to_78 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Bijective_18 -> T_Surjective_18
MAlonzo.Code.Function.Bijection.d_surjective_40
((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Bijection_64 -> T_Bijective_18
MAlonzo.Code.Function.Bijection.d_bijective_84
((T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98
(T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))))
T_Kind_52
MAlonzo.Code.Function.Related.C_injection_60 -> (T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Injection_88)
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Injection_88
du_'8611'_70
T_Kind_52
MAlonzo.Code.Function.Related.C_reverse'45'injection_62
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 AgdaAny
v2 ->
(T_Injection_88 -> T__'8610'__36) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Injection_88 -> T__'8610'__36
MAlonzo.Code.Function.Related.C_lam_50
((T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Injection_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Inverse_58 -> (AgdaAny -> T_Injection_88) -> T_Injection_88
du_'8611'_70
((T_Inverse_58 -> T_Inverse_58) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_sym_226 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
((AgdaAny -> T_Injection_88) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 ->
T__'8610'__36 -> T_Injection_88
MAlonzo.Code.Function.Related.d_app'45''8610'_48
((T_Kind_52
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8610'__36
forall a b. a -> b
coe
T_Kind_52
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_swap'45'coercions_344 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))))))
T_Kind_52
MAlonzo.Code.Function.Related.C_left'45'inverse_64
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 AgdaAny
v2 ->
(T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_LeftInverse_82)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_LeftInverse_82
-> (AgdaAny -> T_LeftInverse_82) -> T_LeftInverse_82
du_'8606'_214
((T_Inverse_58 -> T_LeftInverse_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_LeftInverse_82
MAlonzo.Code.Function.Inverse.du_left'45'inverse_90 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
((T_Kind_52
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_52
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_swap'45'coercions_344 (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
T_Kind_52
MAlonzo.Code.Function.Related.C_surjection_66
-> (AgdaAny -> AgdaAny)
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 ->
(T_Surjection_54
-> (AgdaAny -> T_Surjection_54) -> T_Surjection_54)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Surjection_54 -> (AgdaAny -> T_Surjection_54) -> T_Surjection_54
du_'8608'_250
((T_Π_16 -> T_Surjective_18 -> T_Surjection_54)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> T_Surjective_18 -> T_Surjection_54
MAlonzo.Code.Function.Surjection.C_Surjection'46'constructor_2369
((T_Inverse_58 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Π_16
MAlonzo.Code.Function.Inverse.d_to_78 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
((T_Bijective_18 -> T_Surjective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Bijective_18 -> T_Surjective_18
MAlonzo.Code.Function.Bijection.d_surjective_40
((T_Bijection_64 -> T_Bijective_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Bijection_64 -> T_Bijective_18
MAlonzo.Code.Function.Bijection.d_bijective_84
((T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_Inverse_58 -> T_Bijection_64
MAlonzo.Code.Function.Inverse.du_bijection_98
(T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))))
T_Kind_52
MAlonzo.Code.Function.Related.C_bijection_68 -> (T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Inverse_58)
-> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> (AgdaAny -> T_Inverse_58) -> T_Inverse_58
du_'8596'_286
T_Kind_52
_ -> T_Inverse_58 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError