{-# 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 :: AgdaAny
v4 = (AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
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
v4 of
         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v5 AgdaAny
v6
           -> let v7 :: AgdaAny
v7 = (AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
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
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 a. a
MAlonzo.RTE.mazUnreachableError)
         T_Σ_14
_ -> AgdaAny
forall a. a
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_28 -> T_IsEquivalence_28 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.C_constructor_94
      ((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_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> T_IsEquivalence_28
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_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> T_IsEquivalence_28
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_304 ::
  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_98 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_98 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_98
d_isInjection_304 :: 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_98
-> T_IsInjection_98
-> T_IsInjection_98
d_isInjection_304 ~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_98
v14 T_IsInjection_98
v15
  = (AgdaAny -> AgdaAny)
-> T_IsInjection_98 -> T_IsInjection_98 -> T_IsInjection_98
du_isInjection_304 AgdaAny -> AgdaAny
v12 T_IsInjection_98
v14 T_IsInjection_98
v15
du_isInjection_304 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsInjection_98 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_98 ->
  MAlonzo.Code.Function.Structures.T_IsInjection_98
du_isInjection_304 :: (AgdaAny -> AgdaAny)
-> T_IsInjection_98 -> T_IsInjection_98 -> T_IsInjection_98
du_isInjection_304 AgdaAny -> AgdaAny
v0 T_IsInjection_98
v1 T_IsInjection_98
v2
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_98)
-> AgdaAny -> AgdaAny -> T_IsInjection_98
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_98
MAlonzo.Code.Function.Structures.C_constructor_170
      (((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_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106 (T_IsInjection_98 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98
v1))
         ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106 (T_IsInjection_98 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98
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_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_injective_108 (T_IsInjection_98 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98
v1))
         ((T_IsInjection_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_injective_108 (T_IsInjection_98 -> AgdaAny
forall a b. a -> b
coe T_IsInjection_98
v2)))
-- Function.Construct.Composition._.isSurjection
d_isSurjection_442 ::
  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_174 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_174 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_174
d_isSurjection_442 :: 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_174
-> T_IsSurjection_174
-> T_IsSurjection_174
d_isSurjection_442 ~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_174
v14 T_IsSurjection_174
v15
  = (AgdaAny -> AgdaAny)
-> T_IsSurjection_174 -> T_IsSurjection_174 -> T_IsSurjection_174
du_isSurjection_442 AgdaAny -> AgdaAny
v12 T_IsSurjection_174
v14 T_IsSurjection_174
v15
du_isSurjection_442 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_174 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_174 ->
  MAlonzo.Code.Function.Structures.T_IsSurjection_174
du_isSurjection_442 :: (AgdaAny -> AgdaAny)
-> T_IsSurjection_174 -> T_IsSurjection_174 -> T_IsSurjection_174
du_isSurjection_442 AgdaAny -> AgdaAny
v0 T_IsSurjection_174
v1 T_IsSurjection_174
v2
  = (T_IsCongruent_22 -> (AgdaAny -> T_Σ_14) -> T_IsSurjection_174)
-> AgdaAny -> AgdaAny -> T_IsSurjection_174
forall a b. a -> b
coe
      T_IsCongruent_22 -> (AgdaAny -> T_Σ_14) -> T_IsSurjection_174
MAlonzo.Code.Function.Structures.C_constructor_252
      (((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_174 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_182 (T_IsSurjection_174 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174
v1))
         ((T_IsSurjection_174 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_182 (T_IsSurjection_174 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174
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_174 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_184 (T_IsSurjection_174 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174
v1))
         ((T_IsSurjection_174 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_184 (T_IsSurjection_174 -> AgdaAny
forall a b. a -> b
coe T_IsSurjection_174
v2)))
-- Function.Construct.Composition._.isBijection
d_isBijection_584 ::
  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_256 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256
d_isBijection_584 :: 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_256
-> T_IsBijection_256
-> T_IsBijection_256
d_isBijection_584 ~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_256
v14 T_IsBijection_256
v15
  = (AgdaAny -> AgdaAny)
-> T_IsBijection_256 -> T_IsBijection_256 -> T_IsBijection_256
du_isBijection_584 AgdaAny -> AgdaAny
v12 T_IsBijection_256
v14 T_IsBijection_256
v15
du_isBijection_584 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256
du_isBijection_584 :: (AgdaAny -> AgdaAny)
-> T_IsBijection_256 -> T_IsBijection_256 -> T_IsBijection_256
du_isBijection_584 AgdaAny -> AgdaAny
v0 T_IsBijection_256
v1 T_IsBijection_256
v2
  = (T_IsInjection_98 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_256)
-> AgdaAny -> AgdaAny -> T_IsBijection_256
forall a b. a -> b
coe
      T_IsInjection_98 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_256
MAlonzo.Code.Function.Structures.C_constructor_340
      (((AgdaAny -> AgdaAny)
 -> T_IsInjection_98 -> T_IsInjection_98 -> T_IsInjection_98)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_IsInjection_98 -> T_IsInjection_98 -> T_IsInjection_98
du_isInjection_304 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1))
         ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
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_256 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_266 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1))
         ((T_IsBijection_256 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_266 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v2)))
-- Function.Construct.Composition._.isLeftInverse
d_isLeftInverse_772 ::
  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_346 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346
d_isLeftInverse_772 :: 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_346
-> T_IsLeftInverse_346
-> T_IsLeftInverse_346
d_isLeftInverse_772 ~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_346
v16 T_IsLeftInverse_346
v17
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsLeftInverse_346
-> T_IsLeftInverse_346
-> T_IsLeftInverse_346
du_isLeftInverse_772 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15 T_IsLeftInverse_346
v16 T_IsLeftInverse_346
v17
du_isLeftInverse_772 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346
du_isLeftInverse_772 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsLeftInverse_346
-> T_IsLeftInverse_346
-> T_IsLeftInverse_346
du_isLeftInverse_772 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_IsLeftInverse_346
v2 T_IsLeftInverse_346
v3
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLeftInverse_346)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLeftInverse_346
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLeftInverse_346
MAlonzo.Code.Function.Structures.C_constructor_432
      (((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_346 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_358 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v2))
         ((T_IsLeftInverse_346 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_358 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
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_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_360 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v3))
         ((T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_360 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
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_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_362 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v2))
         ((T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_362 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v3)))
-- Function.Construct.Composition._.isRightInverse
d_isRightInverse_922 ::
  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_438 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438
d_isRightInverse_922 :: 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_438
-> T_IsRightInverse_438
-> T_IsRightInverse_438
d_isRightInverse_922 ~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_438
v16 T_IsRightInverse_438
v17
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsRightInverse_438
-> T_IsRightInverse_438
-> T_IsRightInverse_438
du_isRightInverse_922 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15 T_IsRightInverse_438
v16 T_IsRightInverse_438
v17
du_isRightInverse_922 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438
du_isRightInverse_922 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsRightInverse_438
-> T_IsRightInverse_438
-> T_IsRightInverse_438
du_isRightInverse_922 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_IsRightInverse_438
v2 T_IsRightInverse_438
v3
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsRightInverse_438)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsRightInverse_438
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsRightInverse_438
MAlonzo.Code.Function.Structures.C_constructor_520
      (((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_438 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_450 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v2))
         ((T_IsRightInverse_438 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_450 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
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_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_452 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v3))
         ((T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_452 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
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_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_454 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v2))
         ((T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_454 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v3)))
-- Function.Construct.Composition._.isInverse
d_isInverse_1068 ::
  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_526 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526
d_isInverse_1068 :: 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_526
-> T_IsInverse_526
-> T_IsInverse_526
d_isInverse_1068 ~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_526
v16 T_IsInverse_526
v17
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsInverse_526
-> T_IsInverse_526
-> T_IsInverse_526
du_isInverse_1068 AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny
v15 T_IsInverse_526
v16 T_IsInverse_526
v17
du_isInverse_1068 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526
du_isInverse_1068 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsInverse_526
-> T_IsInverse_526
-> T_IsInverse_526
du_isInverse_1068 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_IsInverse_526
v2 T_IsInverse_526
v3
  = (T_IsLeftInverse_346
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_526)
-> AgdaAny -> AgdaAny -> T_IsInverse_526
forall a b. a -> b
coe
      T_IsLeftInverse_346
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_526
MAlonzo.Code.Function.Structures.C_constructor_618
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> T_IsLeftInverse_346
 -> T_IsLeftInverse_346
 -> T_IsLeftInverse_346)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsLeftInverse_346
-> T_IsLeftInverse_346
-> T_IsLeftInverse_346
du_isLeftInverse_772 ((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_526 -> T_IsLeftInverse_346) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526 -> T_IsLeftInverse_346
MAlonzo.Code.Function.Structures.d_isLeftInverse_536 (T_IsInverse_526 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526
v2))
         ((T_IsInverse_526 -> T_IsLeftInverse_346) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsInverse_526 -> T_IsLeftInverse_346
MAlonzo.Code.Function.Structures.d_isLeftInverse_536 (T_IsInverse_526 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526
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_526 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_538 (T_IsInverse_526 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526
v2))
         ((T_IsInverse_526 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_538 (T_IsInverse_526 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526
v3)))
-- Function.Construct.Composition._.function
d_function_1260 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Func_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
d_function_1260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> T_Func_774
-> T_Func_774
-> T_Func_774
d_function_1260 ~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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 T_Func_774
v9 T_Func_774
v10
  = T_Func_774 -> T_Func_774 -> T_Func_774
du_function_1260 T_Func_774
v9 T_Func_774
v10
du_function_1260 ::
  MAlonzo.Code.Function.Bundles.T_Func_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
du_function_1260 :: T_Func_774 -> T_Func_774 -> T_Func_774
du_function_1260 T_Func_774
v0 T_Func_774
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Func_774)
-> AgdaAny -> AgdaAny -> T_Func_774
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Func_774
MAlonzo.Code.Function.Bundles.C_constructor_840
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Func_774 -> AgdaAny -> AgdaAny)
-> T_Func_774 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Func_774 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_780 T_Func_774
v1
              ((T_Func_774 -> AgdaAny -> AgdaAny)
-> T_Func_774 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_774 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_780 T_Func_774
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_774 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_774 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_780 (T_Func_774 -> AgdaAny
forall a b. a -> b
coe T_Func_774
v0))
         ((T_Func_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_782 (T_Func_774 -> AgdaAny
forall a b. a -> b
coe T_Func_774
v0))
         ((T_Func_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_774 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_782 (T_Func_774 -> AgdaAny
forall a b. a -> b
coe T_Func_774
v1)))
-- Function.Construct.Composition._.injection
d_injection_1390 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
d_injection_1390 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> T_Injection_842
-> T_Injection_842
-> T_Injection_842
d_injection_1390 ~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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 T_Injection_842
v9 T_Injection_842
v10
  = T_Injection_842 -> T_Injection_842 -> T_Injection_842
du_injection_1390 T_Injection_842
v9 T_Injection_842
v10
du_injection_1390 ::
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
du_injection_1390 :: T_Injection_842 -> T_Injection_842 -> T_Injection_842
du_injection_1390 T_Injection_842
v0 T_Injection_842
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Injection_842)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Injection_842
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Injection_842
MAlonzo.Code.Function.Bundles.C_constructor_916
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Injection_842 -> AgdaAny -> AgdaAny)
-> T_Injection_842 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Injection_842 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_850 T_Injection_842
v1
              ((T_Injection_842 -> AgdaAny -> AgdaAny)
-> T_Injection_842 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_842 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_850 T_Injection_842
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_842 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_842 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_850 (T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
v0))
         ((T_Injection_842 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_842 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_852 (T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
v0))
         ((T_Injection_842 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_842 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_852 (T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
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_842 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_842 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_850 (T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
v0))
         ((T_Injection_842 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_842 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_injective_854 (T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
v0))
         ((T_Injection_842 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_842 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_injective_854 (T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
v1)))
-- Function.Construct.Composition._.surjection
d_surjection_1532 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
d_surjection_1532 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> T_Surjection_918
-> T_Surjection_918
-> T_Surjection_918
d_surjection_1532 ~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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 T_Surjection_918
v9 T_Surjection_918
v10
  = T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918
du_surjection_1532 T_Surjection_918
v9 T_Surjection_918
v10
du_surjection_1532 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
du_surjection_1532 :: T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918
du_surjection_1532 T_Surjection_918
v0 T_Surjection_918
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Σ_14)
 -> T_Surjection_918)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Surjection_918
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Σ_14)
-> T_Surjection_918
MAlonzo.Code.Function.Bundles.C_constructor_1002
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Surjection_918 -> AgdaAny -> AgdaAny)
-> T_Surjection_918 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Surjection_918 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_926 T_Surjection_918
v1
              ((T_Surjection_918 -> AgdaAny -> AgdaAny)
-> T_Surjection_918 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_918 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_926 T_Surjection_918
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_918 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_918 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_926 (T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
v0))
         ((T_Surjection_918 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_918 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_928 (T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
v0))
         ((T_Surjection_918 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_918 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_928 (T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
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_918 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_918 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_926 (T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
v0))
         ((T_Surjection_918 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_918 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_surjective_930 (T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
v0))
         ((T_Surjection_918 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_918 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_surjective_930 (T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
v1)))
-- Function.Construct.Composition._.bijection
d_bijection_1686 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_bijection_1686 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> T_Bijection_1004
-> T_Bijection_1004
d_bijection_1686 ~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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 T_Bijection_1004
v9 T_Bijection_1004
v10
  = T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
du_bijection_1686 T_Bijection_1004
v9 T_Bijection_1004
v10
du_bijection_1686 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_bijection_1686 :: T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
du_bijection_1686 T_Bijection_1004
v0 T_Bijection_1004
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Bijection_1004)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_1004
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Bijection_1004
MAlonzo.Code.Function.Bundles.C_constructor_1094
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Bijection_1004 -> AgdaAny -> AgdaAny)
-> T_Bijection_1004 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Bijection_1004 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1012 T_Bijection_1004
v1
              ((T_Bijection_1004 -> AgdaAny -> AgdaAny)
-> T_Bijection_1004 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1012 T_Bijection_1004
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_1004 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1012 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v0))
         ((T_Bijection_1004 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_1014 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v0))
         ((T_Bijection_1004 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_1014 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
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_1004 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1012 (T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004
v0))
         (T_Bijection_1004 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_bijective_1016 (T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004
v0))
         (T_Bijection_1004 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_bijective_1016 (T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004
v1)))
-- Function.Construct.Composition._.equivalence
d_equivalence_1852 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_equivalence_1852 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> T_Equivalence_1858
-> T_Equivalence_1858
-> T_Equivalence_1858
d_equivalence_1852 ~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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 T_Equivalence_1858
v9 T_Equivalence_1858
v10
  = T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du_equivalence_1852 T_Equivalence_1858
v9 T_Equivalence_1858
v10
du_equivalence_1852 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_equivalence_1852 :: T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du_equivalence_1852 T_Equivalence_1858
v0 T_Equivalence_1858
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Equivalence_1858)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_1858
MAlonzo.Code.Function.Bundles.C_constructor_1940
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Equivalence_1858 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1858 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1868 T_Equivalence_1858
v1
              ((T_Equivalence_1858 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1858 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1868 T_Equivalence_1858
v0 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Equivalence_1858 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1858 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1870 T_Equivalence_1858
v0
              ((T_Equivalence_1858 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1858 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1870 T_Equivalence_1858
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_1858 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1868 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
         ((T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1872 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
         ((T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1872 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
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_1858 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1870 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v1))
         ((T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1874 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v1))
         ((T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1874 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0)))
-- Function.Construct.Composition._.leftInverse
d_leftInverse_2002 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_leftInverse_2002 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> T_LeftInverse_1942
-> T_LeftInverse_1942
-> T_LeftInverse_1942
d_leftInverse_2002 ~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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 T_LeftInverse_1942
v9 T_LeftInverse_1942
v10
  = T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942
du_leftInverse_2002 T_LeftInverse_1942
v9 T_LeftInverse_1942
v10
du_leftInverse_2002 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du_leftInverse_2002 :: T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942
du_leftInverse_2002 T_LeftInverse_1942
v0 T_LeftInverse_1942
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_LeftInverse_1942)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1942
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1942
MAlonzo.Code.Function.Bundles.C_constructor_2034
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_LeftInverse_1942 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1942 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1954 T_LeftInverse_1942
v1
              ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1942 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1954 T_LeftInverse_1942
v0 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_LeftInverse_1942 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1942 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1956 T_LeftInverse_1942
v0
              ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1942 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1956 T_LeftInverse_1942
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_1942 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1954 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
         ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1958 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
         ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1958 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
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_1942 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1956 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v1))
         ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1960 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v1))
         ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1960 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
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_1942 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1954 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
         ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1956 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v1))
         ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'737'_1962 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
         ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'737'_1962 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v1)))
-- Function.Construct.Composition._.rightInverse
d_rightInverse_2168 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_rightInverse_2168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> T_RightInverse_2036
-> T_RightInverse_2036
-> T_RightInverse_2036
d_rightInverse_2168 ~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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 T_RightInverse_2036
v9 T_RightInverse_2036
v10
  = T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036
du_rightInverse_2168 T_RightInverse_2036
v9 T_RightInverse_2036
v10
du_rightInverse_2168 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_rightInverse_2168 :: T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036
du_rightInverse_2168 T_RightInverse_2036
v0 T_RightInverse_2036
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_2036)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_2036
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036
MAlonzo.Code.Function.Bundles.C_constructor_2120
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_RightInverse_2036 -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 T_RightInverse_2036
v1
              ((T_RightInverse_2036 -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 T_RightInverse_2036
v0 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_RightInverse_2036 -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 T_RightInverse_2036
v0
              ((T_RightInverse_2036 -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 T_RightInverse_2036
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_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_2052 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_2052 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
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_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v1))
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2054 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v1))
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2054 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
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_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v1))
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_2056 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
         ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_2056 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v1)))
-- Function.Construct.Composition._.inverse
d_inverse_2322 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_inverse_2322 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> T_Inverse_2122
-> T_Inverse_2122
d_inverse_2322 ~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_46
v6 ~T_Setoid_46
v7 ~T_Setoid_46
v8 T_Inverse_2122
v9 T_Inverse_2122
v10
  = T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_inverse_2322 T_Inverse_2122
v9 T_Inverse_2122
v10
du_inverse_2322 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_inverse_2322 :: T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_inverse_2322 T_Inverse_2122
v0 T_Inverse_2122
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_2122)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_2122
MAlonzo.Code.Function.Bundles.C_constructor_2220
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Inverse_2122 -> AgdaAny -> AgdaAny)
-> T_Inverse_2122 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2134 T_Inverse_2122
v1
              ((T_Inverse_2122 -> AgdaAny -> AgdaAny)
-> T_Inverse_2122 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2134 T_Inverse_2122
v0 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Inverse_2122 -> AgdaAny -> AgdaAny)
-> T_Inverse_2122 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2136 T_Inverse_2122
v0
              ((T_Inverse_2122 -> AgdaAny -> AgdaAny)
-> T_Inverse_2122 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2136 T_Inverse_2122
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_2122 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v0))
         ((T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_2138 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v0))
         ((T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_2138 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
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_2122 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2136 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v1))
         ((T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2140 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v1))
         ((T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2140 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
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_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v0))
         (T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2136 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v1))
         (T_Inverse_2122 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_inverse_2142 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v0))
         (T_Inverse_2122 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_inverse_2142 (T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
v1)))
-- Function.Construct.Composition._⟶-∘_
d__'10230''45''8728'__2496 ::
  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_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
d__'10230''45''8728'__2496 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Func_774
-> T_Func_774
-> T_Func_774
d__'10230''45''8728'__2496 ~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_774
v6 T_Func_774
v7
  = T_Func_774 -> T_Func_774 -> T_Func_774
du__'10230''45''8728'__2496 T_Func_774
v6 T_Func_774
v7
du__'10230''45''8728'__2496 ::
  MAlonzo.Code.Function.Bundles.T_Func_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
du__'10230''45''8728'__2496 :: T_Func_774 -> T_Func_774 -> T_Func_774
du__'10230''45''8728'__2496 T_Func_774
v0 T_Func_774
v1
  = (T_Func_774 -> T_Func_774 -> T_Func_774)
-> AgdaAny -> AgdaAny -> T_Func_774
forall a b. a -> b
coe T_Func_774 -> T_Func_774 -> T_Func_774
du_function_1260 (T_Func_774 -> AgdaAny
forall a b. a -> b
coe T_Func_774
v1) (T_Func_774 -> AgdaAny
forall a b. a -> b
coe T_Func_774
v0)
-- Function.Construct.Composition._↣-∘_
d__'8611''45''8728'__2498 ::
  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_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
d__'8611''45''8728'__2498 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Injection_842
-> T_Injection_842
-> T_Injection_842
d__'8611''45''8728'__2498 ~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_842
v6 T_Injection_842
v7
  = T_Injection_842 -> T_Injection_842 -> T_Injection_842
du__'8611''45''8728'__2498 T_Injection_842
v6 T_Injection_842
v7
du__'8611''45''8728'__2498 ::
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
du__'8611''45''8728'__2498 :: T_Injection_842 -> T_Injection_842 -> T_Injection_842
du__'8611''45''8728'__2498 T_Injection_842
v0 T_Injection_842
v1
  = (T_Injection_842 -> T_Injection_842 -> T_Injection_842)
-> AgdaAny -> AgdaAny -> T_Injection_842
forall a b. a -> b
coe T_Injection_842 -> T_Injection_842 -> T_Injection_842
du_injection_1390 (T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
v1) (T_Injection_842 -> AgdaAny
forall a b. a -> b
coe T_Injection_842
v0)
-- Function.Construct.Composition._↠-∘_
d__'8608''45''8728'__2500 ::
  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_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
d__'8608''45''8728'__2500 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Surjection_918
-> T_Surjection_918
-> T_Surjection_918
d__'8608''45''8728'__2500 ~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_918
v6 T_Surjection_918
v7
  = T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918
du__'8608''45''8728'__2500 T_Surjection_918
v6 T_Surjection_918
v7
du__'8608''45''8728'__2500 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
du__'8608''45''8728'__2500 :: T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918
du__'8608''45''8728'__2500 T_Surjection_918
v0 T_Surjection_918
v1
  = (T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918)
-> AgdaAny -> AgdaAny -> T_Surjection_918
forall a b. a -> b
coe T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918
du_surjection_1532 (T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
v1) (T_Surjection_918 -> AgdaAny
forall a b. a -> b
coe T_Surjection_918
v0)
-- Function.Construct.Composition._⤖-∘_
d__'10518''45''8728'__2502 ::
  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_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d__'10518''45''8728'__2502 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_1004
-> T_Bijection_1004
-> T_Bijection_1004
d__'10518''45''8728'__2502 ~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_1004
v6 T_Bijection_1004
v7
  = T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
du__'10518''45''8728'__2502 T_Bijection_1004
v6 T_Bijection_1004
v7
du__'10518''45''8728'__2502 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du__'10518''45''8728'__2502 :: T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
du__'10518''45''8728'__2502 T_Bijection_1004
v0 T_Bijection_1004
v1
  = (T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004)
-> AgdaAny -> AgdaAny -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
du_bijection_1686 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v1) (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v0)
-- Function.Construct.Composition._⇔-∘_
d__'8660''45''8728'__2504 ::
  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_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d__'8660''45''8728'__2504 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1858
-> T_Equivalence_1858
-> T_Equivalence_1858
d__'8660''45''8728'__2504 ~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_1858
v6 T_Equivalence_1858
v7
  = T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du__'8660''45''8728'__2504 T_Equivalence_1858
v6 T_Equivalence_1858
v7
du__'8660''45''8728'__2504 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du__'8660''45''8728'__2504 :: T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du__'8660''45''8728'__2504 T_Equivalence_1858
v0 T_Equivalence_1858
v1
  = (T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858)
-> AgdaAny -> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du_equivalence_1852 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v1) (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0)
-- Function.Construct.Composition._↩-∘_
d__'8617''45''8728'__2506 ::
  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_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d__'8617''45''8728'__2506 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_LeftInverse_1942
-> T_LeftInverse_1942
-> T_LeftInverse_1942
d__'8617''45''8728'__2506 ~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_1942
v6 T_LeftInverse_1942
v7
  = T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942
du__'8617''45''8728'__2506 T_LeftInverse_1942
v6 T_LeftInverse_1942
v7
du__'8617''45''8728'__2506 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du__'8617''45''8728'__2506 :: T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942
du__'8617''45''8728'__2506 T_LeftInverse_1942
v0 T_LeftInverse_1942
v1
  = (T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942)
-> AgdaAny -> AgdaAny -> T_LeftInverse_1942
forall a b. a -> b
coe T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942
du_leftInverse_2002 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v1) (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0)
-- Function.Construct.Composition._↪-∘_
d__'8618''45''8728'__2508 ::
  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_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d__'8618''45''8728'__2508 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_RightInverse_2036
-> T_RightInverse_2036
-> T_RightInverse_2036
d__'8618''45''8728'__2508 ~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_2036
v6 T_RightInverse_2036
v7
  = T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036
du__'8618''45''8728'__2508 T_RightInverse_2036
v6 T_RightInverse_2036
v7
du__'8618''45''8728'__2508 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du__'8618''45''8728'__2508 :: T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036
du__'8618''45''8728'__2508 T_RightInverse_2036
v0 T_RightInverse_2036
v1
  = (T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036)
-> AgdaAny -> AgdaAny -> T_RightInverse_2036
forall a b. a -> b
coe T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036
du_rightInverse_2168 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v1) (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0)
-- Function.Construct.Composition._↔-∘_
d__'8596''45''8728'__2510 ::
  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_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d__'8596''45''8728'__2510 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Inverse_2122
-> T_Inverse_2122
d__'8596''45''8728'__2510 ~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_2122
v6 T_Inverse_2122
v7
  = T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du__'8596''45''8728'__2510 T_Inverse_2122
v6 T_Inverse_2122
v7
du__'8596''45''8728'__2510 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du__'8596''45''8728'__2510 :: T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du__'8596''45''8728'__2510 T_Inverse_2122
v0 T_Inverse_2122
v1
  = (T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_inverse_2322 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v1) (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v0)
-- Function.Construct.Composition._∘-⟶_
d__'8728''45''10230'__2512 ::
  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_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774 ->
  MAlonzo.Code.Function.Bundles.T_Func_774
d__'8728''45''10230'__2512 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Func_774
-> T_Func_774
-> T_Func_774
d__'8728''45''10230'__2512 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_774
v6 T_Func_774
v7
  = (T_Func_774 -> T_Func_774 -> T_Func_774)
-> T_Func_774 -> T_Func_774 -> T_Func_774
forall a b. a -> b
coe T_Func_774 -> T_Func_774 -> T_Func_774
du__'10230''45''8728'__2496 T_Func_774
v6 T_Func_774
v7
-- Function.Construct.Composition._∘-↣_
d__'8728''45''8611'__2514 ::
  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_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842
d__'8728''45''8611'__2514 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Injection_842
-> T_Injection_842
-> T_Injection_842
d__'8728''45''8611'__2514 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_842
v6 T_Injection_842
v7
  = (T_Injection_842 -> T_Injection_842 -> T_Injection_842)
-> T_Injection_842 -> T_Injection_842 -> T_Injection_842
forall a b. a -> b
coe T_Injection_842 -> T_Injection_842 -> T_Injection_842
du__'8611''45''8728'__2498 T_Injection_842
v6 T_Injection_842
v7
-- Function.Construct.Composition._∘-↠_
d__'8728''45''8608'__2516 ::
  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_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_918
d__'8728''45''8608'__2516 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Surjection_918
-> T_Surjection_918
-> T_Surjection_918
d__'8728''45''8608'__2516 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_918
v6 T_Surjection_918
v7
  = (T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918)
-> T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918
forall a b. a -> b
coe T_Surjection_918 -> T_Surjection_918 -> T_Surjection_918
du__'8608''45''8728'__2500 T_Surjection_918
v6 T_Surjection_918
v7
-- Function.Construct.Composition._∘-⤖_
d__'8728''45''10518'__2518 ::
  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_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d__'8728''45''10518'__2518 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_1004
-> T_Bijection_1004
-> T_Bijection_1004
d__'8728''45''10518'__2518 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_1004
v6 T_Bijection_1004
v7
  = (T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004)
-> T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004 -> T_Bijection_1004 -> T_Bijection_1004
du__'10518''45''8728'__2502 T_Bijection_1004
v6 T_Bijection_1004
v7
-- Function.Construct.Composition._∘-⇔_
d__'8728''45''8660'__2520 ::
  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_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d__'8728''45''8660'__2520 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1858
-> T_Equivalence_1858
-> T_Equivalence_1858
d__'8728''45''8660'__2520 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_1858
v6 T_Equivalence_1858
v7
  = (T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858)
-> T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
forall a b. a -> b
coe T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du__'8660''45''8728'__2504 T_Equivalence_1858
v6 T_Equivalence_1858
v7
-- Function.Construct.Composition._∘-↩_
d__'8728''45''8617'__2522 ::
  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_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d__'8728''45''8617'__2522 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_LeftInverse_1942
-> T_LeftInverse_1942
-> T_LeftInverse_1942
d__'8728''45''8617'__2522 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_1942
v6 T_LeftInverse_1942
v7
  = (T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942)
-> T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942
forall a b. a -> b
coe T_LeftInverse_1942 -> T_LeftInverse_1942 -> T_LeftInverse_1942
du__'8617''45''8728'__2506 T_LeftInverse_1942
v6 T_LeftInverse_1942
v7
-- Function.Construct.Composition._∘-↪_
d__'8728''45''8618'__2524 ::
  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_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d__'8728''45''8618'__2524 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_RightInverse_2036
-> T_RightInverse_2036
-> T_RightInverse_2036
d__'8728''45''8618'__2524 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_2036
v6 T_RightInverse_2036
v7
  = (T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036)
-> T_RightInverse_2036
-> T_RightInverse_2036
-> T_RightInverse_2036
forall a b. a -> b
coe T_RightInverse_2036 -> T_RightInverse_2036 -> T_RightInverse_2036
du__'8618''45''8728'__2508 T_RightInverse_2036
v6 T_RightInverse_2036
v7
-- Function.Construct.Composition._∘-↔_
d__'8728''45''8596'__2526 ::
  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_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d__'8728''45''8596'__2526 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Inverse_2122
-> T_Inverse_2122
d__'8728''45''8596'__2526 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_2122
v6 T_Inverse_2122
v7
  = (T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122)
-> T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du__'8596''45''8728'__2510 T_Inverse_2122
v6 T_Inverse_2122
v7