{-# 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.Construct.Composition 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Structures
import qualified MAlonzo.Code.Relation.Binary.Bundles

-- Function.Construct.Composition._.congruent
d_congruent_50 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_congruent_50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_congruent_50 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
               AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18
du_congruent_50 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_congruent_50 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5)
-- Function.Construct.Composition._.injective
d_injective_56 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_injective_56 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
               AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_56 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18
du_injective_56 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_56 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_56 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v4 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4) AgdaAny
v5)
-- Function.Construct.Composition._.surjective
d_surjective_62 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14)
-> (AgdaAny -> T_Σ_14)
-> AgdaAny
-> T_Σ_14
d_surjective_62 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
                AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 AgdaAny -> T_Σ_14
v14 AgdaAny -> T_Σ_14
v15 AgdaAny
v16
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14
du_surjective_62 AgdaAny -> AgdaAny
v12 AgdaAny -> T_Σ_14
v14 AgdaAny -> T_Σ_14
v15 AgdaAny
v16
du_surjective_62 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_surjective_62 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14
du_surjective_62 AgdaAny -> AgdaAny
v0 AgdaAny -> T_Σ_14
v1 AgdaAny -> T_Σ_14
v2 AgdaAny
v3
  = let v4 :: t
v4 = (AgdaAny -> T_Σ_14) -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> T_Σ_14
v2 AgdaAny
v3 in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall {t}. t
v4 of
         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v5 AgdaAny
v6
           -> let v7 :: t
v7 = (AgdaAny -> T_Σ_14) -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> T_Σ_14
v1 AgdaAny
v5 in
              AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall {t}. t
v7 of
                   MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
                     -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)
                          ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v10 AgdaAny
v11 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v10) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9 AgdaAny
v10 AgdaAny
v11)))
                   T_Σ_14
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
         T_Σ_14
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
-- Function.Construct.Composition._.bijective
d_bijective_102 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_bijective_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_bijective_102 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
                AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13
  = (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_bijective_102 AgdaAny -> AgdaAny
v12
du_bijective_102 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_bijective_102 :: (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_bijective_102 AgdaAny -> AgdaAny
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip'8242'_312
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_56 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)) (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14
du_surjective_62 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0))
-- Function.Construct.Composition._.inverseˡ
d_inverse'737'_134 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'737'_134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_inverse'737'_134 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10
                   ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v17 AgdaAny
v18 AgdaAny
v19 AgdaAny
v20
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'737'_134 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v17 AgdaAny
v18 AgdaAny
v19 AgdaAny
v20
du_inverse'737'_134 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'737'_134 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'737'_134 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4) AgdaAny
v5 AgdaAny
v6)
-- Function.Construct.Composition._.inverseʳ
d_inverse'691'_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 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_inverse'691'_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 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10
                   ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v17 AgdaAny
v18 AgdaAny
v19 AgdaAny
v20
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'691'_140 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v17 AgdaAny
v18 AgdaAny
v19 AgdaAny
v20
du_inverse'691'_140 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'691'_140 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'691'_140 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v4 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4) AgdaAny
v5 AgdaAny
v6)
-- Function.Construct.Composition._.inverseᵇ
d_inverse'7495'_146 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_inverse'7495'_146 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
d_inverse'7495'_146 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10
                    ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_inverse'7495'_146 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15
du_inverse'7495'_146 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_inverse'7495'_146 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_inverse'7495'_146 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_zip'8242'_312
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'737'_134 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'691'_140 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
-- Function.Construct.Composition._.isCongruent
d_isCongruent_174 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsCongruent_22
-> T_IsCongruent_22
-> T_IsCongruent_22
d_isCongruent_174 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
                  AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 T_IsCongruent_22
v14 T_IsCongruent_22
v15
  = (AgdaAny -> AgdaAny)
-> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22
du_isCongruent_174 AgdaAny -> AgdaAny
v12 T_IsCongruent_22
v14 T_IsCongruent_22
v15
du_isCongruent_174 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
du_isCongruent_174 :: (AgdaAny -> AgdaAny)
-> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22
du_isCongruent_174 AgdaAny -> AgdaAny
v0 T_IsCongruent_22
v1 T_IsCongruent_22
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.C_IsCongruent'46'constructor_985
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
            (T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_cong_32 T_IsCongruent_22
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3)
              ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4)
              ((T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_cong_32 T_IsCongruent_22
v1 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5)))
      ((T_IsCongruent_22 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v1))
      ((T_IsCongruent_22 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8322'_36 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v2))
-- Function.Construct.Composition._.isInjection
d_isInjection_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 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92
d_isInjection_296 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsInjection_92
-> T_IsInjection_92
-> T_IsInjection_92
d_isInjection_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 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
                  AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 T_IsInjection_92
v14 T_IsInjection_92
v15
  = (AgdaAny -> AgdaAny)
-> T_IsInjection_92 -> T_IsInjection_92 -> T_IsInjection_92
du_isInjection_296 AgdaAny -> AgdaAny
v12 T_IsInjection_92
v14 T_IsInjection_92
v15
du_isInjection_296 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_92
du_isInjection_296 :: (AgdaAny -> AgdaAny)
-> T_IsInjection_92 -> T_IsInjection_92 -> T_IsInjection_92
du_isInjection_296 AgdaAny -> AgdaAny
v0 T_IsInjection_92
v1 T_IsInjection_92
v2
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_92)
-> AgdaAny -> AgdaAny -> T_IsInjection_92
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_92
MAlonzo.Code.Function.Structures.C_IsInjection'46'constructor_3997
      (((AgdaAny -> AgdaAny)
 -> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22
du_isCongruent_174 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsInjection_92 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92
v1))
         ((T_IsInjection_92 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_56 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_injective_102 (T_IsInjection_92 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92
v1))
         ((T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_injective_102 (T_IsInjection_92 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_92
v2)))
-- Function.Construct.Composition._.isSurjection
d_isSurjection_426 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_162 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_162 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_162
d_isSurjection_426 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsSurjection_162
-> T_IsSurjection_162
-> T_IsSurjection_162
d_isSurjection_426 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10
                   ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 T_IsSurjection_162
v14 T_IsSurjection_162
v15
  = (AgdaAny -> AgdaAny)
-> T_IsSurjection_162 -> T_IsSurjection_162 -> T_IsSurjection_162
du_isSurjection_426 AgdaAny -> AgdaAny
v12 T_IsSurjection_162
v14 T_IsSurjection_162
v15
du_isSurjection_426 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_162 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_162 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_162
du_isSurjection_426 :: (AgdaAny -> AgdaAny)
-> T_IsSurjection_162 -> T_IsSurjection_162 -> T_IsSurjection_162
du_isSurjection_426 AgdaAny -> AgdaAny
v0 T_IsSurjection_162
v1 T_IsSurjection_162
v2
  = (T_IsCongruent_22 -> (AgdaAny -> T_Σ_14) -> T_IsSurjection_162)
-> AgdaAny -> AgdaAny -> T_IsSurjection_162
forall a b. a -> b
coe
      T_IsCongruent_22 -> (AgdaAny -> T_Σ_14) -> T_IsSurjection_162
MAlonzo.Code.Function.Structures.C_IsSurjection'46'constructor_6463
      (((AgdaAny -> AgdaAny)
 -> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22
du_isCongruent_174 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsSurjection_162 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_170 (T_IsSurjection_162 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162
v1))
         ((T_IsSurjection_162 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_170 (T_IsSurjection_162 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14
du_surjective_62 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsSurjection_162 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_172 (T_IsSurjection_162 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162
v1))
         ((T_IsSurjection_162 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_172 (T_IsSurjection_162 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_162
v2)))
-- Function.Construct.Composition._.isBijection
d_isBijection_560 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238
d_isBijection_560 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsBijection_238
-> T_IsBijection_238
-> T_IsBijection_238
d_isBijection_560 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
                  AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 T_IsBijection_238
v14 T_IsBijection_238
v15
  = (AgdaAny -> AgdaAny)
-> T_IsBijection_238 -> T_IsBijection_238 -> T_IsBijection_238
du_isBijection_560 AgdaAny -> AgdaAny
v12 T_IsBijection_238
v14 T_IsBijection_238
v15
du_isBijection_560 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238
du_isBijection_560 :: (AgdaAny -> AgdaAny)
-> T_IsBijection_238 -> T_IsBijection_238 -> T_IsBijection_238
du_isBijection_560 AgdaAny -> AgdaAny
v0 T_IsBijection_238
v1 T_IsBijection_238
v2
  = (T_IsInjection_92 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> T_IsBijection_238
forall a b. a -> b
coe
      T_IsInjection_92 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_238
MAlonzo.Code.Function.Structures.C_IsBijection'46'constructor_10113
      (((AgdaAny -> AgdaAny)
 -> T_IsInjection_92 -> T_IsInjection_92 -> T_IsInjection_92)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsInjection_92 -> T_IsInjection_92 -> T_IsInjection_92
du_isInjection_296 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsBijection_238 -> T_IsInjection_92) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v1))
         ((T_IsBijection_238 -> T_IsInjection_92) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14
du_surjective_62 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsBijection_238 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_248 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v1))
         ((T_IsBijection_238 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_248 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v2)))
-- Function.Construct.Composition._.isLeftInverse
d_isLeftInverse_740 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322
d_isLeftInverse_740 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsLeftInverse_322
-> T_IsLeftInverse_322
-> T_IsLeftInverse_322
d_isLeftInverse_740 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10
                    ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 T_IsLeftInverse_322
v16 T_IsLeftInverse_322
v17
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsLeftInverse_322
-> T_IsLeftInverse_322
-> T_IsLeftInverse_322
du_isLeftInverse_740 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15 T_IsLeftInverse_322
v16 T_IsLeftInverse_322
v17
du_isLeftInverse_740 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322
du_isLeftInverse_740 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsLeftInverse_322
-> T_IsLeftInverse_322
-> T_IsLeftInverse_322
du_isLeftInverse_740 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_IsLeftInverse_322
v2 T_IsLeftInverse_322
v3
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLeftInverse_322)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLeftInverse_322
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLeftInverse_322
MAlonzo.Code.Function.Structures.C_IsLeftInverse'46'constructor_14363
      (((AgdaAny -> AgdaAny)
 -> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22
du_isCongruent_174 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsLeftInverse_322 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_334 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v2))
         ((T_IsLeftInverse_322 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_334 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v3)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_336 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v3))
         ((T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_336 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'737'_134 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_338 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v2))
         ((T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_338 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v3)))
-- Function.Construct.Composition._.isRightInverse
d_isRightInverse_882 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408
d_isRightInverse_882 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsRightInverse_408
-> T_IsRightInverse_408
-> T_IsRightInverse_408
d_isRightInverse_882 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10
                     ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 T_IsRightInverse_408
v16 T_IsRightInverse_408
v17
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsRightInverse_408
-> T_IsRightInverse_408
-> T_IsRightInverse_408
du_isRightInverse_882 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15 T_IsRightInverse_408
v16 T_IsRightInverse_408
v17
du_isRightInverse_882 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408
du_isRightInverse_882 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsRightInverse_408
-> T_IsRightInverse_408
-> T_IsRightInverse_408
du_isRightInverse_882 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_IsRightInverse_408
v2 T_IsRightInverse_408
v3
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsRightInverse_408)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsRightInverse_408
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsRightInverse_408
MAlonzo.Code.Function.Structures.C_IsRightInverse'46'constructor_18837
      (((AgdaAny -> AgdaAny)
 -> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22
du_isCongruent_174 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsRightInverse_408 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_420 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v2))
         ((T_IsRightInverse_408 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_420 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v3)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_422 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v3))
         ((T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_422 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'691'_140 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_424 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v2))
         ((T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_424 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v3)))
-- Function.Construct.Composition._.isInverse
d_isInverse_1020 ::
  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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490
d_isInverse_1020 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsInverse_490
-> T_IsInverse_490
-> T_IsInverse_490
d_isInverse_1020 ~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_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11
                 AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 T_IsInverse_490
v16 T_IsInverse_490
v17
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsInverse_490
-> T_IsInverse_490
-> T_IsInverse_490
du_isInverse_1020 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15 T_IsInverse_490
v16 T_IsInverse_490
v17
du_isInverse_1020 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490
du_isInverse_1020 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsInverse_490
-> T_IsInverse_490
-> T_IsInverse_490
du_isInverse_1020 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_IsInverse_490
v2 T_IsInverse_490
v3
  = (T_IsLeftInverse_322
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_490)
-> AgdaAny -> AgdaAny -> T_IsInverse_490
forall a b. a -> b
coe
      T_IsLeftInverse_322
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_490
MAlonzo.Code.Function.Structures.C_IsInverse'46'constructor_22449
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> T_IsLeftInverse_322
 -> T_IsLeftInverse_322
 -> T_IsLeftInverse_322)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsLeftInverse_322
-> T_IsLeftInverse_322
-> T_IsLeftInverse_322
du_isLeftInverse_740 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_IsInverse_490 -> T_IsLeftInverse_322) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490 -> T_IsLeftInverse_322
MAlonzo.Code.Function.Structures.d_isLeftInverse_500 (T_IsInverse_490 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490
v2))
         ((T_IsInverse_490 -> T_IsLeftInverse_322) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsInverse_490 -> T_IsLeftInverse_322
MAlonzo.Code.Function.Structures.d_isLeftInverse_500 (T_IsInverse_490 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490
v3)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'691'_140 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)
         ((T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_502 (T_IsInverse_490 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490
v2))
         ((T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_502 (T_IsInverse_490 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490
v3)))
-- Function.Construct.Composition._.function
d_function_1204 ::
  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 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_function_1204 :: 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_Func_714
-> T_Func_714
-> T_Func_714
d_function_1204 ~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_Func_714
v9 T_Func_714
v10
  = T_Func_714 -> T_Func_714 -> T_Func_714
du_function_1204 T_Func_714
v9 T_Func_714
v10
du_function_1204 ::
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du_function_1204 :: T_Func_714 -> T_Func_714 -> T_Func_714
du_function_1204 T_Func_714
v0 T_Func_714
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Func_714)
-> AgdaAny -> AgdaAny -> T_Func_714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Func_714
MAlonzo.Code.Function.Bundles.C_Func'46'constructor_6307
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Func_714 -> AgdaAny -> AgdaAny)
-> T_Func_714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Func_714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_720 T_Func_714
v1
              ((T_Func_714 -> AgdaAny -> AgdaAny)
-> T_Func_714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_720 T_Func_714
v0 AgdaAny
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_Func_714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_720 (T_Func_714 -> AgdaAny
forall a b. a -> b
coe T_Func_714
v0))
         ((T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_722 (T_Func_714 -> AgdaAny
forall a b. a -> b
coe T_Func_714
v0))
         ((T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_722 (T_Func_714 -> AgdaAny
forall a b. a -> b
coe T_Func_714
v1)))
-- Function.Construct.Composition._.injection
d_injection_1326 ::
  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 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
d_injection_1326 :: 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_Injection_776
-> T_Injection_776
-> T_Injection_776
d_injection_1326 ~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_Injection_776
v9 T_Injection_776
v10
  = T_Injection_776 -> T_Injection_776 -> T_Injection_776
du_injection_1326 T_Injection_776
v9 T_Injection_776
v10
du_injection_1326 ::
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
du_injection_1326 :: T_Injection_776 -> T_Injection_776 -> T_Injection_776
du_injection_1326 T_Injection_776
v0 T_Injection_776
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Injection_776
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Injection_776
MAlonzo.Code.Function.Bundles.C_Injection'46'constructor_8675
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Injection_776 -> AgdaAny -> AgdaAny)
-> T_Injection_776 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Injection_776 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_784 T_Injection_776
v1
              ((T_Injection_776 -> AgdaAny -> AgdaAny)
-> T_Injection_776 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_784 T_Injection_776
v0 AgdaAny
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_Injection_776 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_784 (T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
v0))
         ((T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_786 (T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
v0))
         ((T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_786 (T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_56
         ((T_Injection_776 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_784 (T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
v0))
         ((T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_injective_788 (T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
v0))
         ((T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_injective_788 (T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
v1)))
-- Function.Construct.Composition._.surjection
d_surjection_1460 ::
  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 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_surjection_1460 :: 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_Surjection_846
-> T_Surjection_846
-> T_Surjection_846
d_surjection_1460 ~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_Surjection_846
v9 T_Surjection_846
v10
  = T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du_surjection_1460 T_Surjection_846
v9 T_Surjection_846
v10
du_surjection_1460 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_surjection_1460 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du_surjection_1460 T_Surjection_846
v0 T_Surjection_846
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14)
 -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Surjection_846
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14)
-> T_Surjection_846
MAlonzo.Code.Function.Bundles.C_Surjection'46'constructor_11197
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v1
              ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> T_Surjection_846 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 T_Surjection_846
v0 AgdaAny
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
         ((T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_856 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
         ((T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_856 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14
du_surjective_62
         ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
         ((T_Surjection_846 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_surjective_858 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
         ((T_Surjection_846 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_surjective_858 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v1)))
-- Function.Construct.Composition._.bijection
d_bijection_1606 ::
  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 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_bijection_1606 :: 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_Bijection_926
-> T_Bijection_926
-> T_Bijection_926
d_bijection_1606 ~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_Bijection_926
v9 T_Bijection_926
v10
  = T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du_bijection_1606 T_Bijection_926
v9 T_Bijection_926
v10
du_bijection_1606 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_bijection_1606 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du_bijection_1606 T_Bijection_926
v0 T_Bijection_926
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Bijection_926)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_926
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Bijection_926
MAlonzo.Code.Function.Bundles.C_Bijection'46'constructor_15277
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Bijection_926 -> AgdaAny -> AgdaAny)
-> T_Bijection_926 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Bijection_926 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_934 T_Bijection_926
v1
              ((T_Bijection_926 -> AgdaAny -> AgdaAny)
-> T_Bijection_926 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_934 T_Bijection_926
v0 AgdaAny
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_Bijection_926 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_934 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v0))
         ((T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_936 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v0))
         ((T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_936 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v1)))
      (((AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14)
-> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_bijective_102 (T_Bijection_926 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_934 (T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926
v0))
         (T_Bijection_926 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_bijective_938 (T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926
v0))
         (T_Bijection_926 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_bijective_938 (T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926
v1)))
-- Function.Construct.Composition._.equivalence
d_equivalence_1764 ::
  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 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_equivalence_1764 :: 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_Equivalence_1714
-> T_Equivalence_1714
-> T_Equivalence_1714
d_equivalence_1764 ~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_Equivalence_1714
v9 T_Equivalence_1714
v10
  = T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du_equivalence_1764 T_Equivalence_1714
v9 T_Equivalence_1714
v10
du_equivalence_1764 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_equivalence_1764 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du_equivalence_1764 T_Equivalence_1714
v0 T_Equivalence_1714
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.C_Equivalence'46'constructor_25797
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 T_Equivalence_1714
v1
              ((T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 T_Equivalence_1714
v0 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726 T_Equivalence_1714
v0
              ((T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726 T_Equivalence_1714
v1 AgdaAny
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_Equivalence_1714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
         ((T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1728 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
         ((T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1728 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_Equivalence_1714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v1))
         ((T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1730 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v1))
         ((T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1730 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0)))
-- Function.Construct.Composition._.leftInverse
d_leftInverse_1906 ::
  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 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_leftInverse_1906 :: 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_1792
-> T_LeftInverse_1792
-> T_LeftInverse_1792
d_leftInverse_1906 ~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_1792
v9 T_LeftInverse_1792
v10
  = T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du_leftInverse_1906 T_LeftInverse_1792
v9 T_LeftInverse_1792
v10
du_leftInverse_1906 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_leftInverse_1906 :: T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du_leftInverse_1906 T_LeftInverse_1792
v0 T_LeftInverse_1792
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_LeftInverse_1792)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1792
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792
MAlonzo.Code.Function.Bundles.C_LeftInverse'46'constructor_29775
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_LeftInverse_1792 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1804 T_LeftInverse_1792
v1
              ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1804 T_LeftInverse_1792
v0 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_LeftInverse_1792 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1806 T_LeftInverse_1792
v0
              ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1806 T_LeftInverse_1792
v1 AgdaAny
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1804 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1808 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1808 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1806 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v1))
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1810 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v1))
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1810 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'737'_134
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1804 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1806 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v1))
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'737'_1812 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
         ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'737'_1812 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v1)))
-- Function.Construct.Composition._.rightInverse
d_rightInverse_2064 ::
  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 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_rightInverse_2064 :: 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_RightInverse_1880
-> T_RightInverse_1880
-> T_RightInverse_1880
d_rightInverse_2064 ~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_RightInverse_1880
v9 T_RightInverse_1880
v10
  = T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du_rightInverse_2064 T_RightInverse_1880
v9 T_RightInverse_1880
v10
du_rightInverse_2064 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_rightInverse_2064 :: T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du_rightInverse_2064 T_RightInverse_1880
v0 T_RightInverse_1880
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_1880)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_1880
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.C_RightInverse'46'constructor_34573
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_RightInverse_1880 -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 T_RightInverse_1880
v1
              ((T_RightInverse_1880 -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 T_RightInverse_1880
v0 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_RightInverse_1880 -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 T_RightInverse_1880
v0
              ((T_RightInverse_1880 -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 T_RightInverse_1880
v1 AgdaAny
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1896 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1896 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v1))
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1898 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v1))
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1898 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_inverse'691'_140
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v1))
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_1900 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
         ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_1900 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v1)))
-- Function.Construct.Composition._.inverse
d_inverse_2210 ::
  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 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_inverse_2210 :: 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_Inverse_1960
-> T_Inverse_1960
-> T_Inverse_1960
d_inverse_2210 ~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_Inverse_1960
v9 T_Inverse_1960
v10
  = T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_inverse_2210 T_Inverse_1960
v9 T_Inverse_1960
v10
du_inverse_2210 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_inverse_2210 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_inverse_2210 T_Inverse_1960
v0 T_Inverse_1960
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_1960)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_1960
MAlonzo.Code.Function.Bundles.C_Inverse'46'constructor_38621
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 T_Inverse_1960
v1
              ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 T_Inverse_1960
v0 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v0
              ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v1 AgdaAny
v2)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_Inverse_1960 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
         ((T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
         ((T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_congruent_50
         ((T_Inverse_1960 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1))
         ((T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1978 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1))
         ((T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1978 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
du_inverse'7495'_146
         (T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v0))
         (T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v1))
         (T_Inverse_1960 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_inverse_1980 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v0))
         (T_Inverse_1960 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_inverse_1980 (T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960
v1)))
-- Function.Construct.Composition._⟶-∘_
d__'10230''45''8728'__2376 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d__'10230''45''8728'__2376 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Func_714
-> T_Func_714
-> T_Func_714
d__'10230''45''8728'__2376 ~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_Func_714
v6 T_Func_714
v7
  = T_Func_714 -> T_Func_714 -> T_Func_714
du__'10230''45''8728'__2376 T_Func_714
v6 T_Func_714
v7
du__'10230''45''8728'__2376 ::
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du__'10230''45''8728'__2376 :: T_Func_714 -> T_Func_714 -> T_Func_714
du__'10230''45''8728'__2376 T_Func_714
v0 T_Func_714
v1
  = (T_Func_714 -> T_Func_714 -> T_Func_714)
-> AgdaAny -> AgdaAny -> T_Func_714
forall a b. a -> b
coe T_Func_714 -> T_Func_714 -> T_Func_714
du_function_1204 (T_Func_714 -> AgdaAny
forall a b. a -> b
coe T_Func_714
v1) (T_Func_714 -> AgdaAny
forall a b. a -> b
coe T_Func_714
v0)
-- Function.Construct.Composition._↣-∘_
d__'8611''45''8728'__2378 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
d__'8611''45''8728'__2378 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Injection_776
-> T_Injection_776
-> T_Injection_776
d__'8611''45''8728'__2378 ~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_Injection_776
v6 T_Injection_776
v7
  = T_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8611''45''8728'__2378 T_Injection_776
v6 T_Injection_776
v7
du__'8611''45''8728'__2378 ::
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
du__'8611''45''8728'__2378 :: T_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8611''45''8728'__2378 T_Injection_776
v0 T_Injection_776
v1
  = (T_Injection_776 -> T_Injection_776 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> T_Injection_776
forall a b. a -> b
coe T_Injection_776 -> T_Injection_776 -> T_Injection_776
du_injection_1326 (T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
v1) (T_Injection_776 -> AgdaAny
forall a b. a -> b
coe T_Injection_776
v0)
-- Function.Construct.Composition._↠-∘_
d__'8608''45''8728'__2380 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d__'8608''45''8728'__2380 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Surjection_846
-> T_Surjection_846
-> T_Surjection_846
d__'8608''45''8728'__2380 ~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_Surjection_846
v6 T_Surjection_846
v7
  = T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du__'8608''45''8728'__2380 T_Surjection_846
v6 T_Surjection_846
v7
du__'8608''45''8728'__2380 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du__'8608''45''8728'__2380 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du__'8608''45''8728'__2380 T_Surjection_846
v0 T_Surjection_846
v1
  = (T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> T_Surjection_846
forall a b. a -> b
coe T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du_surjection_1460 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v1) (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0)
-- Function.Construct.Composition._⤖-∘_
d__'10518''45''8728'__2382 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d__'10518''45''8728'__2382 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_926
-> T_Bijection_926
-> T_Bijection_926
d__'10518''45''8728'__2382 ~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_Bijection_926
v6 T_Bijection_926
v7
  = T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du__'10518''45''8728'__2382 T_Bijection_926
v6 T_Bijection_926
v7
du__'10518''45''8728'__2382 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du__'10518''45''8728'__2382 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du__'10518''45''8728'__2382 T_Bijection_926
v0 T_Bijection_926
v1
  = (T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926)
-> AgdaAny -> AgdaAny -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du_bijection_1606 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v1) (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v0)
-- Function.Construct.Composition._⇔-∘_
d__'8660''45''8728'__2384 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d__'8660''45''8728'__2384 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1714
-> T_Equivalence_1714
-> T_Equivalence_1714
d__'8660''45''8728'__2384 ~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_Equivalence_1714
v6 T_Equivalence_1714
v7
  = T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du__'8660''45''8728'__2384 T_Equivalence_1714
v6 T_Equivalence_1714
v7
du__'8660''45''8728'__2384 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du__'8660''45''8728'__2384 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du__'8660''45''8728'__2384 T_Equivalence_1714
v0 T_Equivalence_1714
v1
  = (T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du_equivalence_1764 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v1) (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0)
-- Function.Construct.Composition._↩-∘_
d__'8617''45''8728'__2386 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d__'8617''45''8728'__2386 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_LeftInverse_1792
-> T_LeftInverse_1792
-> T_LeftInverse_1792
d__'8617''45''8728'__2386 ~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_LeftInverse_1792
v6 T_LeftInverse_1792
v7
  = T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du__'8617''45''8728'__2386 T_LeftInverse_1792
v6 T_LeftInverse_1792
v7
du__'8617''45''8728'__2386 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du__'8617''45''8728'__2386 :: T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du__'8617''45''8728'__2386 T_LeftInverse_1792
v0 T_LeftInverse_1792
v1
  = (T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792)
-> AgdaAny -> AgdaAny -> T_LeftInverse_1792
forall a b. a -> b
coe T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du_leftInverse_1906 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v1) (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0)
-- Function.Construct.Composition._↪-∘_
d__'8618''45''8728'__2388 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d__'8618''45''8728'__2388 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_RightInverse_1880
-> T_RightInverse_1880
-> T_RightInverse_1880
d__'8618''45''8728'__2388 ~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_RightInverse_1880
v6 T_RightInverse_1880
v7
  = T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du__'8618''45''8728'__2388 T_RightInverse_1880
v6 T_RightInverse_1880
v7
du__'8618''45''8728'__2388 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du__'8618''45''8728'__2388 :: T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du__'8618''45''8728'__2388 T_RightInverse_1880
v0 T_RightInverse_1880
v1
  = (T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880)
-> AgdaAny -> AgdaAny -> T_RightInverse_1880
forall a b. a -> b
coe T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du_rightInverse_2064 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v1) (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0)
-- Function.Construct.Composition._↔-∘_
d__'8596''45''8728'__2390 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d__'8596''45''8728'__2390 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Inverse_1960
-> T_Inverse_1960
d__'8596''45''8728'__2390 ~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_Inverse_1960
v6 T_Inverse_1960
v7
  = T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du__'8596''45''8728'__2390 T_Inverse_1960
v6 T_Inverse_1960
v7
du__'8596''45''8728'__2390 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du__'8596''45''8728'__2390 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du__'8596''45''8728'__2390 T_Inverse_1960
v0 T_Inverse_1960
v1
  = (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_inverse_2210 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1) (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0)
-- Function.Construct.Composition._∘-⟶_
d__'8728''45''10230'__2392 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d__'8728''45''10230'__2392 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Func_714
-> T_Func_714
-> T_Func_714
d__'8728''45''10230'__2392 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_Func_714
v6 T_Func_714
v7
  = (T_Func_714 -> T_Func_714 -> T_Func_714)
-> T_Func_714 -> T_Func_714 -> T_Func_714
forall a b. a -> b
coe T_Func_714 -> T_Func_714 -> T_Func_714
du__'10230''45''8728'__2376 T_Func_714
v6 T_Func_714
v7
-- Function.Construct.Composition._∘-↣_
d__'8728''45''8611'__2394 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
d__'8728''45''8611'__2394 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Injection_776
-> T_Injection_776
-> T_Injection_776
d__'8728''45''8611'__2394 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_Injection_776
v6 T_Injection_776
v7
  = (T_Injection_776 -> T_Injection_776 -> T_Injection_776)
-> T_Injection_776 -> T_Injection_776 -> T_Injection_776
forall a b. a -> b
coe T_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8611''45''8728'__2378 T_Injection_776
v6 T_Injection_776
v7
-- Function.Construct.Composition._∘-↠_
d__'8728''45''8608'__2396 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d__'8728''45''8608'__2396 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Surjection_846
-> T_Surjection_846
-> T_Surjection_846
d__'8728''45''8608'__2396 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_Surjection_846
v6 T_Surjection_846
v7
  = (T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846)
-> T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
forall a b. a -> b
coe T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du__'8608''45''8728'__2380 T_Surjection_846
v6 T_Surjection_846
v7
-- Function.Construct.Composition._∘-⤖_
d__'8728''45''10518'__2398 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d__'8728''45''10518'__2398 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_926
-> T_Bijection_926
-> T_Bijection_926
d__'8728''45''10518'__2398 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_Bijection_926
v6 T_Bijection_926
v7
  = (T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926)
-> T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du__'10518''45''8728'__2382 T_Bijection_926
v6 T_Bijection_926
v7
-- Function.Construct.Composition._∘-⇔_
d__'8728''45''8660'__2400 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d__'8728''45''8660'__2400 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1714
-> T_Equivalence_1714
-> T_Equivalence_1714
d__'8728''45''8660'__2400 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_Equivalence_1714
v6 T_Equivalence_1714
v7
  = (T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714)
-> T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
forall a b. a -> b
coe T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du__'8660''45''8728'__2384 T_Equivalence_1714
v6 T_Equivalence_1714
v7
-- Function.Construct.Composition._∘-↩_
d__'8728''45''8617'__2402 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d__'8728''45''8617'__2402 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_LeftInverse_1792
-> T_LeftInverse_1792
-> T_LeftInverse_1792
d__'8728''45''8617'__2402 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_LeftInverse_1792
v6 T_LeftInverse_1792
v7
  = (T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792)
-> T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
forall a b. a -> b
coe T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du__'8617''45''8728'__2386 T_LeftInverse_1792
v6 T_LeftInverse_1792
v7
-- Function.Construct.Composition._∘-↪_
d__'8728''45''8618'__2404 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d__'8728''45''8618'__2404 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_RightInverse_1880
-> T_RightInverse_1880
-> T_RightInverse_1880
d__'8728''45''8618'__2404 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_RightInverse_1880
v6 T_RightInverse_1880
v7
  = (T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880)
-> T_RightInverse_1880
-> T_RightInverse_1880
-> T_RightInverse_1880
forall a b. a -> b
coe T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du__'8618''45''8728'__2388 T_RightInverse_1880
v6 T_RightInverse_1880
v7
-- Function.Construct.Composition._∘-↔_
d__'8728''45''8596'__2406 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d__'8728''45''8596'__2406 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Inverse_1960
-> T_Inverse_1960
d__'8728''45''8596'__2406 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_Inverse_1960
v6 T_Inverse_1960
v7
  = (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960)
-> T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du__'8596''45''8728'__2390 T_Inverse_1960
v6 T_Inverse_1960
v7