{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Function.Related.TypeIsomorphisms where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Algebra.Structures.Biased
import qualified MAlonzo.Code.Data.Empty.Polymorphic
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Product.Function.NonDependent.Propositional
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.Sum.Function.Propositional
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Construct.Identity
import qualified MAlonzo.Code.Function.Related.Propositional
import qualified MAlonzo.Code.Level
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax

-- Function.Related.TypeIsomorphisms.Σ-assoc
d_Σ'45'assoc_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_Σ'45'assoc_32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_2122
d_Σ'45'assoc_32 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 = T_Inverse_2122
du_Σ'45'assoc_32
du_Σ'45'assoc_32 :: MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_Σ'45'assoc_32 :: T_Inverse_2122
du_Σ'45'assoc_32
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_assoc'691'_260)
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_assoc'737'_276)
-- Function.Related.TypeIsomorphisms.×-comm
d_'215''45'comm_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'215''45'comm_42 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'215''45'comm_42 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_2122
du_'215''45'comm_42
du_'215''45'comm_42 :: MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'comm_42 :: T_Inverse_2122
du_'215''45'comm_42
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370)
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370)
-- Function.Related.TypeIsomorphisms.×-identityˡ
d_'215''45'identity'737'_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'215''45'identity'737'_50 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'215''45'identity'737'_50 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_2122
du_'215''45'identity'737'_50
du_'215''45'identity'737'_50 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'identity'737'_50 :: T_Inverse_2122
du_'215''45'identity'737'_50
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 ->
            (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 -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
                 (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)))
-- Function.Related.TypeIsomorphisms.×-identityʳ
d_'215''45'identity'691'_58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'215''45'identity'691'_58 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'215''45'identity'691'_58 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_2122
du_'215''45'identity'691'_58
du_'215''45'identity'691'_58 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'identity'691'_58 :: T_Inverse_2122
du_'215''45'identity'691'_58
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 ->
            (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
v0)
              ((AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
                 (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))))
-- Function.Related.TypeIsomorphisms.×-identity
d_'215''45'identity_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'identity_68 :: T_Level_18 -> T_Σ_14
d_'215''45'identity_68 ~T_Level_18
v0 = T_Σ_14
du_'215''45'identity_68
du_'215''45'identity_68 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'identity_68 :: T_Σ_14
du_'215''45'identity_68
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (\ AgdaAny
v0 -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'identity'737'_50)
      (\ AgdaAny
v0 -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'identity'691'_58)
-- Function.Related.TypeIsomorphisms.×-zeroˡ
d_'215''45'zero'737'_74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'215''45'zero'737'_74 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'215''45'zero'737'_74 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_2122
du_'215''45'zero'737'_74
du_'215''45'zero'737'_74 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'zero'737'_74 :: T_Inverse_2122
du_'215''45'zero'737'_74
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v0)))
      (((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0))
         (\ AgdaAny
v0 ->
            AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.Polymorphic.du_'8869''45'elim_20))
-- Function.Related.TypeIsomorphisms.×-zeroʳ
d_'215''45'zero'691'_86 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'215''45'zero'691'_86 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'215''45'zero'691'_86 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_2122
du_'215''45'zero'691'_86
du_'215''45'zero'691'_86 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'zero'691'_86 :: T_Inverse_2122
du_'215''45'zero'691'_86
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v0)))
      (((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112
         (\ AgdaAny
v0 ->
            AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.Polymorphic.du_'8869''45'elim_20)
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)))
-- Function.Related.TypeIsomorphisms.×-zero
d_'215''45'zero_98 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'zero_98 :: T_Level_18 -> T_Σ_14
d_'215''45'zero_98 ~T_Level_18
v0 = T_Σ_14
du_'215''45'zero_98
du_'215''45'zero_98 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'zero_98 :: T_Σ_14
du_'215''45'zero_98
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (\ AgdaAny
v0 -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'zero'737'_74)
      (\ AgdaAny
v0 -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'zero'691'_86)
-- Function.Related.TypeIsomorphisms.⊎-assoc
d_'8846''45'assoc_104 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8846''45'assoc_104 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'8846''45'assoc_104 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_2122
du_'8846''45'assoc_104
du_'8846''45'assoc_104 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8846''45'assoc_104 :: T_Inverse_2122
du_'8846''45'assoc_104
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66
         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66
            ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
            (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
               ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
               ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)))
         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
            ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
            ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66
         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
            ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
            ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38))
         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66
            (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
               ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
               ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42))
            ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)))
-- Function.Related.TypeIsomorphisms.⊎-comm
d_'8846''45'comm_124 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8846''45'comm_124 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'8846''45'comm_124 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_2122
du_'8846''45'comm_124
du_'8846''45'comm_124 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8846''45'comm_124 :: T_Inverse_2122
du_'8846''45'comm_124
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((T__'8846'__30 -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_swap_78)
      ((T__'8846'__30 -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_swap_78)
-- Function.Related.TypeIsomorphisms.⊎-identityˡ
d_'8846''45'identity'737'_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8846''45'identity'737'_128 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'8846''45'identity'737'_128 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Inverse_2122
du_'8846''45'identity'737'_128
du_'8846''45'identity'737'_128 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8846''45'identity'737'_128 :: T_Inverse_2122
du_'8846''45'identity'737'_128
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66 AgdaAny
forall a. a
erased
         (\ AgdaAny
v0 -> AgdaAny
v0))
      ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
-- Function.Related.TypeIsomorphisms.⊎-identityʳ
d_'8846''45'identity'691'_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8846''45'identity'691'_136 :: T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'8846''45'identity'691'_136 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Inverse_2122
du_'8846''45'identity'691'_136
du_'8846''45'identity'691'_136 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8846''45'identity'691'_136 :: T_Inverse_2122
du_'8846''45'identity'691'_136
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66 (\ AgdaAny
v0 -> AgdaAny
v0)
         AgdaAny
forall a. a
erased)
      ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
-- Function.Related.TypeIsomorphisms.⊎-identity
d_'8846''45'identity_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8846''45'identity_144 :: T_Level_18 -> T_Σ_14
d_'8846''45'identity_144 ~T_Level_18
v0 = T_Σ_14
du_'8846''45'identity_144
du_'8846''45'identity_144 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8846''45'identity_144 :: T_Σ_14
du_'8846''45'identity_144
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (\ AgdaAny
v0 -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'8846''45'identity'737'_128)
      (\ AgdaAny
v0 -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'8846''45'identity'691'_136)
-- Function.Related.TypeIsomorphisms.Σ-distribˡ-⊎
d_Σ'45'distrib'737''45''8846'_154 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_Σ'45'distrib'737''45''8846'_154 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Inverse_2122
d_Σ'45'distrib'737''45''8846'_154 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5
  = T_Inverse_2122
du_Σ'45'distrib'737''45''8846'_154
du_Σ'45'distrib'737''45''8846'_154 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_Σ'45'distrib'737''45''8846'_154 :: T_Inverse_2122
du_Σ'45'distrib'737''45''8846'_154
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v0 ->
               ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66
                 (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
                    ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                       (\ AgdaAny
v1 ->
                          (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
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
                 (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
                    ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                       (\ AgdaAny
v1 ->
                          (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
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))))))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66
         (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8322'_150
            ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> (AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)))
         (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8322'_150
            ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> (AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42))))
-- Function.Related.TypeIsomorphisms.Σ-distribʳ-⊎
d_Σ'45'distrib'691''45''8846'_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_Σ'45'distrib'691''45''8846'_174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (T__'8846'__30 -> T_Level_18)
-> T_Inverse_2122
d_Σ'45'distrib'691''45''8846'_174 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T__'8846'__30 -> T_Level_18
v5
  = T_Inverse_2122
du_Σ'45'distrib'691''45''8846'_174
du_Σ'45'distrib'691''45''8846'_174 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_Σ'45'distrib'691''45''8846'_174 :: T_Inverse_2122
du_Σ'45'distrib'691''45''8846'_174
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244
         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
            (((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_curry_224
               ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38))
            (((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_curry_224
               ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42))))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_dmap_176
            ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> AgdaAny
v1)))
         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_dmap_176
            ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> AgdaAny
v1))))
-- Function.Related.TypeIsomorphisms.×-distribˡ-⊎
d_'215''45'distrib'737''45''8846'_188 ::
  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
d_'215''45'distrib'737''45''8846'_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
d_'215''45'distrib'737''45''8846'_188 ~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
du_'215''45'distrib'737''45''8846'_188
du_'215''45'distrib'737''45''8846'_188 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'distrib'737''45''8846'_188 :: T_Inverse_2122
du_'215''45'distrib'737''45''8846'_188
  = T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
du_Σ'45'distrib'737''45''8846'_154
-- Function.Related.TypeIsomorphisms.×-distribˡ-⊎′
d_'215''45'distrib'737''45''8846''8242'_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'215''45'distrib'737''45''8846''8242'_192 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'215''45'distrib'737''45''8846''8242'_192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122
du_'215''45'distrib'737''45''8846''8242'_192
du_'215''45'distrib'737''45''8846''8242'_192 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'distrib'737''45''8846''8242'_192 :: T_Inverse_2122
du_'215''45'distrib'737''45''8846''8242'_192
  = T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'distrib'737''45''8846'_188
-- Function.Related.TypeIsomorphisms.×-distribʳ-⊎
d_'215''45'distrib'691''45''8846'_196 ::
  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
d_'215''45'distrib'691''45''8846'_196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
d_'215''45'distrib'691''45''8846'_196 ~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
du_'215''45'distrib'691''45''8846'_196
du_'215''45'distrib'691''45''8846'_196 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'distrib'691''45''8846'_196 :: T_Inverse_2122
du_'215''45'distrib'691''45''8846'_196
  = T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
du_Σ'45'distrib'691''45''8846'_174
-- Function.Related.TypeIsomorphisms.×-distribʳ-⊎′
d_'215''45'distrib'691''45''8846''8242'_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'215''45'distrib'691''45''8846''8242'_200 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_2122
d_'215''45'distrib'691''45''8846''8242'_200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_2122
du_'215''45'distrib'691''45''8846''8242'_200
du_'215''45'distrib'691''45''8846''8242'_200 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'215''45'distrib'691''45''8846''8242'_200 :: T_Inverse_2122
du_'215''45'distrib'691''45''8846''8242'_200
  = T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'distrib'691''45''8846'_196
-- Function.Related.TypeIsomorphisms.×-distrib-⊎′
d_'215''45'distrib'45''8846''8242'_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'distrib'45''8846''8242'_206 :: T_Level_18 -> T_Σ_14
d_'215''45'distrib'45''8846''8242'_206 ~T_Level_18
v0
  = T_Σ_14
du_'215''45'distrib'45''8846''8242'_206
du_'215''45'distrib'45''8846''8242'_206 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'distrib'45''8846''8242'_206 :: T_Σ_14
du_'215''45'distrib'45''8846''8242'_206
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'distrib'737''45''8846''8242'_192)
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'distrib'691''45''8846''8242'_200)
-- Function.Related.TypeIsomorphisms.×-isMagma
d_'215''45'isMagma_214 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'215''45'isMagma_214 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMagma_178
d_'215''45'isMagma_214 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsMagma_178
du_'215''45'isMagma_214 T_SymmetricKind_86
v0
du_'215''45'isMagma_214 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'215''45'isMagma_214 :: T_SymmetricKind_86 -> T_IsMagma_178
du_'215''45'isMagma_214 T_SymmetricKind_86
v0
  = (T_IsEquivalence_28
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178)
-> AgdaAny -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.C_constructor_210
      ((T_SymmetricKind_86 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SymmetricKind_86 -> T_IsEquivalence_28
MAlonzo.Code.Function.Related.Propositional.du_SK'45'isEquivalence_172
         (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Product.Function.NonDependent.Propositional.du__'215''45'cong__96
              ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))))
-- Function.Related.TypeIsomorphisms.×-magma
d_'215''45'magma_222 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
d_'215''45'magma_222 :: T_SymmetricKind_86 -> T_Level_18 -> T_Magma_74
d_'215''45'magma_222 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Magma_74
du_'215''45'magma_222 T_SymmetricKind_86
v0
du_'215''45'magma_222 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
du_'215''45'magma_222 :: T_SymmetricKind_86 -> T_Magma_74
du_'215''45'magma_222 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178 -> T_Magma_74)
-> AgdaAny -> AgdaAny -> T_Magma_74
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178 -> T_Magma_74
MAlonzo.Code.Algebra.Bundles.C_constructor_124 AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMagma_178
du_'215''45'isMagma_214 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.×-isSemigroup
d_'215''45'isSemigroup_232 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'215''45'isSemigroup_232 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsSemigroup_488
d_'215''45'isSemigroup_232 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsSemigroup_488
du_'215''45'isSemigroup_232 T_SymmetricKind_86
v0
du_'215''45'isSemigroup_232 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'215''45'isSemigroup_232 :: T_SymmetricKind_86 -> T_IsSemigroup_488
du_'215''45'isSemigroup_232 T_SymmetricKind_86
v0
  = (T_IsMagma_178
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe
      T_IsMagma_178
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.C_constructor_522
      ((T_SymmetricKind_86 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMagma_178
du_'215''45'isMagma_214 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
              (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                 (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
              (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_Σ'45'assoc_32)))
-- Function.Related.TypeIsomorphisms.×-semigroup
d_'215''45'semigroup_246 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
d_'215''45'semigroup_246 :: T_SymmetricKind_86 -> T_Level_18 -> T_Semigroup_558
d_'215''45'semigroup_246 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Semigroup_558
du_'215''45'semigroup_246 T_SymmetricKind_86
v0
du_'215''45'semigroup_246 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
du_'215''45'semigroup_246 :: T_SymmetricKind_86 -> T_Semigroup_558
du_'215''45'semigroup_246 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_488 -> T_Semigroup_558)
-> AgdaAny -> AgdaAny -> T_Semigroup_558
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488 -> T_Semigroup_558
MAlonzo.Code.Algebra.Bundles.C_constructor_614 AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsSemigroup_488
du_'215''45'isSemigroup_232 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.×-isMonoid
d_'215''45'isMonoid_256 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
d_'215''45'isMonoid_256 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMonoid_712
d_'215''45'isMonoid_256 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsMonoid_712
du_'215''45'isMonoid_256 T_SymmetricKind_86
v0
du_'215''45'isMonoid_256 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
du_'215''45'isMonoid_256 :: T_SymmetricKind_86 -> T_IsMonoid_712
du_'215''45'isMonoid_256 T_SymmetricKind_86
v0
  = (T_IsSemigroup_488 -> T_Σ_14 -> T_IsMonoid_712)
-> AgdaAny -> AgdaAny -> T_IsMonoid_712
forall a b. a -> b
coe
      T_IsSemigroup_488 -> T_Σ_14 -> T_IsMonoid_712
MAlonzo.Code.Algebra.Structures.C_constructor_758
      ((T_SymmetricKind_86 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsSemigroup_488
du_'215''45'isSemigroup_232 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      ((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) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
                 (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                    (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
                 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'identity'737'_50)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
                 (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                    (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
                 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'identity'691'_58))))
-- Function.Related.TypeIsomorphisms.×-monoid
d_'215''45'monoid_264 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_'215''45'monoid_264 :: T_SymmetricKind_86 -> T_Level_18 -> T_Monoid_914
d_'215''45'monoid_264 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Monoid_914
du_'215''45'monoid_264 T_SymmetricKind_86
v0
du_'215''45'monoid_264 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_'215''45'monoid_264 :: T_SymmetricKind_86 -> T_Monoid_914
du_'215''45'monoid_264 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_712 -> T_Monoid_914)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_712 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.C_constructor_990 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMonoid_712
du_'215''45'isMonoid_256 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.×-isCommutativeMonoid
d_'215''45'isCommutativeMonoid_274 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_764
d_'215''45'isCommutativeMonoid_274 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeMonoid_764
d_'215''45'isCommutativeMonoid_274 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_IsCommutativeMonoid_764
du_'215''45'isCommutativeMonoid_274 T_SymmetricKind_86
v0
du_'215''45'isCommutativeMonoid_274 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_764
du_'215''45'isCommutativeMonoid_274 :: T_SymmetricKind_86 -> T_IsCommutativeMonoid_764
du_'215''45'isCommutativeMonoid_274 T_SymmetricKind_86
v0
  = (T_IsMonoid_712
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_764)
-> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_764
forall a b. a -> b
coe
      T_IsMonoid_712
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_764
MAlonzo.Code.Algebra.Structures.C_constructor_820
      ((T_SymmetricKind_86 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMonoid_712
du_'215''45'isMonoid_256 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
              (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                 (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
              (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'comm_42)))
-- Function.Related.TypeIsomorphisms.×-commutativeMonoid
d_'215''45'commutativeMonoid_286 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996
d_'215''45'commutativeMonoid_286 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeMonoid_996
d_'215''45'commutativeMonoid_286 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_CommutativeMonoid_996
du_'215''45'commutativeMonoid_286 T_SymmetricKind_86
v0
du_'215''45'commutativeMonoid_286 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996
du_'215''45'commutativeMonoid_286 :: T_SymmetricKind_86 -> T_CommutativeMonoid_996
du_'215''45'commutativeMonoid_286 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeMonoid_764 -> T_CommutativeMonoid_996)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_CommutativeMonoid_996
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid_764 -> T_CommutativeMonoid_996
MAlonzo.Code.Algebra.Bundles.C_constructor_1088 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsCommutativeMonoid_764)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeMonoid_764
du_'215''45'isCommutativeMonoid_274 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.⊎-isMagma
d_'8846''45'isMagma_296 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
d_'8846''45'isMagma_296 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMagma_178
d_'8846''45'isMagma_296 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsMagma_178
du_'8846''45'isMagma_296 T_SymmetricKind_86
v0
du_'8846''45'isMagma_296 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_178
du_'8846''45'isMagma_296 :: T_SymmetricKind_86 -> T_IsMagma_178
du_'8846''45'isMagma_296 T_SymmetricKind_86
v0
  = (T_IsEquivalence_28
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_178)
-> AgdaAny -> AgdaAny -> T_IsMagma_178
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_178
MAlonzo.Code.Algebra.Structures.C_constructor_210
      ((T_SymmetricKind_86 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SymmetricKind_86 -> T_IsEquivalence_28
MAlonzo.Code.Function.Related.Propositional.du_SK'45'isEquivalence_172
         (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Sum.Function.Propositional.du__'8846''45'cong__94
              ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))))
-- Function.Related.TypeIsomorphisms.⊎-magma
d_'8846''45'magma_304 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
d_'8846''45'magma_304 :: T_SymmetricKind_86 -> T_Level_18 -> T_Magma_74
d_'8846''45'magma_304 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Magma_74
du_'8846''45'magma_304 T_SymmetricKind_86
v0
du_'8846''45'magma_304 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_74
du_'8846''45'magma_304 :: T_SymmetricKind_86 -> T_Magma_74
du_'8846''45'magma_304 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178 -> T_Magma_74)
-> AgdaAny -> AgdaAny -> T_Magma_74
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_178 -> T_Magma_74
MAlonzo.Code.Algebra.Bundles.C_constructor_124 AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMagma_178
du_'8846''45'isMagma_296 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.⊎-isSemigroup
d_'8846''45'isSemigroup_314 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
d_'8846''45'isSemigroup_314 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsSemigroup_488
d_'8846''45'isSemigroup_314 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_IsSemigroup_488
du_'8846''45'isSemigroup_314 T_SymmetricKind_86
v0
du_'8846''45'isSemigroup_314 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_488
du_'8846''45'isSemigroup_314 :: T_SymmetricKind_86 -> T_IsSemigroup_488
du_'8846''45'isSemigroup_314 T_SymmetricKind_86
v0
  = (T_IsMagma_178
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_488
forall a b. a -> b
coe
      T_IsMagma_178
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_488
MAlonzo.Code.Algebra.Structures.C_constructor_522
      ((T_SymmetricKind_86 -> T_IsMagma_178) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMagma_178
du_'8846''45'isMagma_296 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
              (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                 (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
              (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'8846''45'assoc_104)))
-- Function.Related.TypeIsomorphisms.⊎-semigroup
d_'8846''45'semigroup_328 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
d_'8846''45'semigroup_328 :: T_SymmetricKind_86 -> T_Level_18 -> T_Semigroup_558
d_'8846''45'semigroup_328 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Semigroup_558
du_'8846''45'semigroup_328 T_SymmetricKind_86
v0
du_'8846''45'semigroup_328 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_558
du_'8846''45'semigroup_328 :: T_SymmetricKind_86 -> T_Semigroup_558
du_'8846''45'semigroup_328 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_488 -> T_Semigroup_558)
-> AgdaAny -> AgdaAny -> T_Semigroup_558
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_488 -> T_Semigroup_558
MAlonzo.Code.Algebra.Bundles.C_constructor_614 AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsSemigroup_488
du_'8846''45'isSemigroup_314 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.⊎-isMonoid
d_'8846''45'isMonoid_338 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
d_'8846''45'isMonoid_338 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMonoid_712
d_'8846''45'isMonoid_338 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsMonoid_712
du_'8846''45'isMonoid_338 T_SymmetricKind_86
v0
du_'8846''45'isMonoid_338 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_712
du_'8846''45'isMonoid_338 :: T_SymmetricKind_86 -> T_IsMonoid_712
du_'8846''45'isMonoid_338 T_SymmetricKind_86
v0
  = (T_IsSemigroup_488 -> T_Σ_14 -> T_IsMonoid_712)
-> AgdaAny -> AgdaAny -> T_IsMonoid_712
forall a b. a -> b
coe
      T_IsSemigroup_488 -> T_Σ_14 -> T_IsMonoid_712
MAlonzo.Code.Algebra.Structures.C_constructor_758
      ((T_SymmetricKind_86 -> T_IsSemigroup_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsSemigroup_488
du_'8846''45'isSemigroup_314 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      ((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) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
                 (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                    (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
                 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'8846''45'identity'737'_128)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
                 (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                    (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
                 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'8846''45'identity'691'_136))))
-- Function.Related.TypeIsomorphisms.⊎-monoid
d_'8846''45'monoid_346 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
d_'8846''45'monoid_346 :: T_SymmetricKind_86 -> T_Level_18 -> T_Monoid_914
d_'8846''45'monoid_346 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Monoid_914
du_'8846''45'monoid_346 T_SymmetricKind_86
v0
du_'8846''45'monoid_346 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_914
du_'8846''45'monoid_346 :: T_SymmetricKind_86 -> T_Monoid_914
du_'8846''45'monoid_346 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_712 -> T_Monoid_914)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_914
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_712 -> T_Monoid_914
MAlonzo.Code.Algebra.Bundles.C_constructor_990 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMonoid_712
du_'8846''45'isMonoid_338 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.⊎-isCommutativeMonoid
d_'8846''45'isCommutativeMonoid_356 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_764
d_'8846''45'isCommutativeMonoid_356 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeMonoid_764
d_'8846''45'isCommutativeMonoid_356 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_IsCommutativeMonoid_764
du_'8846''45'isCommutativeMonoid_356 T_SymmetricKind_86
v0
du_'8846''45'isCommutativeMonoid_356 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_764
du_'8846''45'isCommutativeMonoid_356 :: T_SymmetricKind_86 -> T_IsCommutativeMonoid_764
du_'8846''45'isCommutativeMonoid_356 T_SymmetricKind_86
v0
  = (T_IsMonoid_712
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_764)
-> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_764
forall a b. a -> b
coe
      T_IsMonoid_712
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_764
MAlonzo.Code.Algebra.Structures.C_constructor_820
      ((T_SymmetricKind_86 -> T_IsMonoid_712) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMonoid_712
du_'8846''45'isMonoid_338 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
              (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                 (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
              (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'8846''45'comm_124)))
-- Function.Related.TypeIsomorphisms.⊎-commutativeMonoid
d_'8846''45'commutativeMonoid_368 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996
d_'8846''45'commutativeMonoid_368 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeMonoid_996
d_'8846''45'commutativeMonoid_368 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_CommutativeMonoid_996
du_'8846''45'commutativeMonoid_368 T_SymmetricKind_86
v0
du_'8846''45'commutativeMonoid_368 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_996
du_'8846''45'commutativeMonoid_368 :: T_SymmetricKind_86 -> T_CommutativeMonoid_996
du_'8846''45'commutativeMonoid_368 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeMonoid_764 -> T_CommutativeMonoid_996)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_CommutativeMonoid_996
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid_764 -> T_CommutativeMonoid_996
MAlonzo.Code.Algebra.Bundles.C_constructor_1088 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsCommutativeMonoid_764)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeMonoid_764
du_'8846''45'isCommutativeMonoid_356 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.×-⊎-isCommutativeSemiring
d_'215''45''8846''45'isCommutativeSemiring_378 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1750
d_'215''45''8846''45'isCommutativeSemiring_378 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeSemiring_1750
d_'215''45''8846''45'isCommutativeSemiring_378 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_IsCommutativeSemiring_1750
du_'215''45''8846''45'isCommutativeSemiring_378 T_SymmetricKind_86
v0
du_'215''45''8846''45'isCommutativeSemiring_378 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1750
du_'215''45''8846''45'isCommutativeSemiring_378 :: T_SymmetricKind_86 -> T_IsCommutativeSemiring_1750
du_'215''45''8846''45'isCommutativeSemiring_378 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsCommutativeSemiring'737'_3088
 -> T_IsCommutativeSemiring_1750)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring_1750
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'737'_3088
-> T_IsCommutativeSemiring_1750
MAlonzo.Code.Algebra.Structures.Biased.du_isCommutativeSemiring_3114
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_IsCommutativeMonoid_764
 -> T_IsCommutativeMonoid_764
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> T_IsCommutativeSemiring'737'_3088)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_764
-> T_IsCommutativeMonoid_764
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_3088
MAlonzo.Code.Algebra.Structures.Biased.C_constructor_3208
         ((T_SymmetricKind_86 -> T_IsCommutativeMonoid_764)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeMonoid_764
du_'8846''45'isCommutativeMonoid_356 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
         ((T_SymmetricKind_86 -> T_IsCommutativeMonoid_764)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeMonoid_764
du_'215''45'isCommutativeMonoid_274 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
               (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
                 (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                    (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
                 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'distrib'691''45''8846'_196)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_6 -> T_Inverse_2122 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_2122 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
                 (T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                    (T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0))
                 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
du_'215''45'zero'737'_74))))
-- Function.Related.TypeIsomorphisms.×-⊎-commutativeSemiring
d_'215''45''8846''45'commutativeSemiring_392 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2524
d_'215''45''8846''45'commutativeSemiring_392 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeSemiring_2524
d_'215''45''8846''45'commutativeSemiring_392 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_CommutativeSemiring_2524
du_'215''45''8846''45'commutativeSemiring_392 T_SymmetricKind_86
v0
du_'215''45''8846''45'commutativeSemiring_392 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2524
du_'215''45''8846''45'commutativeSemiring_392 :: T_SymmetricKind_86 -> T_CommutativeSemiring_2524
du_'215''45''8846''45'commutativeSemiring_392 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_IsCommutativeSemiring_1750
 -> T_CommutativeSemiring_2524)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_CommutativeSemiring_2524
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring_1750
-> T_CommutativeSemiring_2524
MAlonzo.Code.Algebra.Bundles.C_constructor_2706 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsCommutativeSemiring_1750)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeSemiring_1750
du_'215''45''8846''45'isCommutativeSemiring_378 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.ΠΠ↔ΠΠ
d_ΠΠ'8596'ΠΠ_418 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_ΠΠ'8596'ΠΠ_418 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_2122
d_ΠΠ'8596'ΠΠ_418 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 = T_Inverse_2122
du_ΠΠ'8596'ΠΠ_418
du_ΠΠ'8596'ΠΠ_418 :: MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_ΠΠ'8596'ΠΠ_418 :: T_Inverse_2122
du_ΠΠ'8596'ΠΠ_418
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0 AgdaAny
v2 AgdaAny
v1))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0 AgdaAny
v2 AgdaAny
v1))
-- Function.Related.TypeIsomorphisms.∃∃↔∃∃
d_'8707''8707''8596''8707''8707'_444 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8707''8707''8596''8707''8707'_444 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_2122
d_'8707''8707''8596''8707''8707'_444 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = T_Inverse_2122
du_'8707''8707''8596''8707''8707'_444
du_'8707''8707''8596''8707''8707'_444 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8707''8707''8596''8707''8707'_444 :: T_Inverse_2122
du_'8707''8707''8596''8707''8707'_444
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_to_460) ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_from_476)
-- Function.Related.TypeIsomorphisms._.to
d_to_460 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to_460 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_to_460 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_Σ_14
v6 = T_Σ_14 -> T_Σ_14
du_to_460 T_Σ_14
v6
du_to_460 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to_460 :: T_Σ_14 -> T_Σ_14
du_to_460 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2
        -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
               -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
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
v3)
                    ((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
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.TypeIsomorphisms._.from
d_from_476 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_from_476 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_from_476 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_Σ_14
v6 = T_Σ_14 -> T_Σ_14
du_from_476 T_Σ_14
v6
du_from_476 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_476 :: T_Σ_14 -> T_Σ_14
du_from_476 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2
        -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
               -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
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
v3)
                    ((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
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.TypeIsomorphisms.Π↔Π
d_Π'8596'Π_496 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_Π'8596'Π_496 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_2122
d_Π'8596'Π_496 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 = T_Inverse_2122
du_Π'8596'Π_496
du_Π'8596'Π_496 :: MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_Π'8596'Π_496 :: T_Inverse_2122
du_Π'8596'Π_496
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0 AgdaAny
v1)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0 AgdaAny
v1))
-- Function.Related.TypeIsomorphisms.→-cong-⇔
d_'8594''45'cong'45''8660'_502 ::
  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.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_'8594''45'cong'45''8660'_502 :: 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_Equivalence_1858
-> T_Equivalence_1858
-> T_Equivalence_1858
d_'8594''45'cong'45''8660'_502 ~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_Equivalence_1858
v8
                               T_Equivalence_1858
v9
  = T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du_'8594''45'cong'45''8660'_502 T_Equivalence_1858
v8 T_Equivalence_1858
v9
du_'8594''45'cong'45''8660'_502 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_'8594''45'cong'45''8660'_502 :: T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du_'8594''45'cong'45''8660'_502 T_Equivalence_1858
v0 T_Equivalence_1858
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1858)
-> AgdaAny -> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1858
MAlonzo.Code.Function.Bundles.du_mk'8660'_2474
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (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
              (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 AgdaAny
v3))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (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 -> 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
v0 AgdaAny
v3))))
-- Function.Related.TypeIsomorphisms.→-cong-↔
d_'8594''45'cong'45''8596'_524 ::
  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 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  (() ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  () ->
  () ->
  () ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8594''45'cong'45''8596'_524 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (T_Level_18
    -> (AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> (T_Level_18
    -> (AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Inverse_2122
-> T_Inverse_2122
d_'8594''45'cong'45''8596'_524 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v4 ~T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8
                               ~T_Level_18
v9 T_Inverse_2122
v10 T_Inverse_2122
v11
  = T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_'8594''45'cong'45''8596'_524 T_Inverse_2122
v10 T_Inverse_2122
v11
du_'8594''45'cong'45''8596'_524 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8594''45'cong'45''8596'_524 :: T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_'8594''45'cong'45''8596'_524 T_Inverse_2122
v0 T_Inverse_2122
v1
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (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
              (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 AgdaAny
v3))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (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 -> 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
v0 AgdaAny
v3))))
-- Function.Related.TypeIsomorphisms.→-cong
d_'8594''45'cong_560 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  (() ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  () -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_'8594''45'cong_560 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (T_Level_18
    -> (AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> (T_Level_18
    -> (AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> T_SymmetricKind_86
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8594''45'cong_560 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v4 ~T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v5 T_SymmetricKind_86
v6 ~T_Level_18
v7 ~T_Level_18
v8 ~T_Level_18
v9 ~T_Level_18
v10
  = T_SymmetricKind_86 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8594''45'cong_560 T_SymmetricKind_86
v6
du_'8594''45'cong_560 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8594''45'cong_560 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8594''45'cong_560 T_SymmetricKind_86
v0
  = case T_SymmetricKind_86 -> T_SymmetricKind_86
forall a b. a -> b
coe T_SymmetricKind_86
v0 of
      T_SymmetricKind_86
MAlonzo.Code.Function.Related.Propositional.C_equivalence_88
        -> (T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> T_Equivalence_1858 -> T_Equivalence_1858
du_'8594''45'cong'45''8660'_502
      T_SymmetricKind_86
MAlonzo.Code.Function.Related.Propositional.C_bijection_90
        -> (T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122 -> T_Inverse_2122
du_'8594''45'cong'45''8596'_524
      T_SymmetricKind_86
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.TypeIsomorphisms.¬-cong-⇔
d_'172''45'cong'45''8660'_570 ::
  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
d_'172''45'cong'45''8660'_570 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1858
-> T_Equivalence_1858
d_'172''45'cong'45''8660'_570 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Equivalence_1858
v4
  = T_Equivalence_1858 -> T_Equivalence_1858
du_'172''45'cong'45''8660'_570 T_Equivalence_1858
v4
du_'172''45'cong'45''8660'_570 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_'172''45'cong'45''8660'_570 :: T_Equivalence_1858 -> T_Equivalence_1858
du_'172''45'cong'45''8660'_570 T_Equivalence_1858
v0
  = (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_'8594''45'cong'45''8660'_502 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0)
      (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
MAlonzo.Code.Function.Construct.Identity.du_'8660''45'id_654)
-- Function.Related.TypeIsomorphisms.¬-cong
d_'172''45'cong_580 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  (() ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  () -> () -> AgdaAny -> AgdaAny
d_'172''45'cong_580 :: T_Level_18
-> T_Level_18
-> (T_Level_18
    -> (AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> (T_Level_18
    -> (AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> T_SymmetricKind_86
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
d_'172''45'cong_580 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v2 ~T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v3 T_SymmetricKind_86
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny
v7
  = T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_'172''45'cong_580 T_SymmetricKind_86
v4 AgdaAny
v7
du_'172''45'cong_580 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  AgdaAny -> AgdaAny
du_'172''45'cong_580 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_'172''45'cong_580 T_SymmetricKind_86
v0 AgdaAny
v1
  = (T_SymmetricKind_86 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_SymmetricKind_86 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_SymmetricKind_86 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8594''45'cong_560 T_SymmetricKind_86
v0 AgdaAny
v1
      ((T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Kind_6 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'reflexive_162
         ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
            (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0)))
-- Function.Related.TypeIsomorphisms.Related-cong
d_Related'45'cong_590 ::
  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.Function.Related.Propositional.T_SymmetricKind_86 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_Related'45'cong_590 :: 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_SymmetricKind_86
-> AgdaAny
-> AgdaAny
-> T_Equivalence_1858
d_Related'45'cong_590 ~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_SymmetricKind_86
v8 AgdaAny
v9 AgdaAny
v10
  = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_SymmetricKind_86
-> AgdaAny
-> AgdaAny
-> T_Equivalence_1858
du_Related'45'cong_590 T_Level_18
v1 T_Level_18
v3 T_Level_18
v5 T_Level_18
v7 T_SymmetricKind_86
v8 AgdaAny
v9 AgdaAny
v10
du_Related'45'cong_590 ::
  () ->
  () ->
  () ->
  () ->
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_Related'45'cong_590 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_SymmetricKind_86
-> AgdaAny
-> AgdaAny
-> T_Equivalence_1858
du_Related'45'cong_590 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_SymmetricKind_86
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1858)
-> AgdaAny -> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1858
MAlonzo.Code.Function.Bundles.du_mk'8660'_2474
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v7 ->
            ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8764'_302
              (\ AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
                 (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'trans_164
                   ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                      (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v4)))
              T_Level_18
v1 T_Level_18
v0 T_Level_18
v3
              (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8764'_302
                 (\ AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
                    (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'trans_164
                      ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                         (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v4)))
                 T_Level_18
v0 T_Level_18
v2 T_Level_18
v3
                 (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8764'_302
                    (\ AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
                       (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'trans_164
                         ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                            (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v4)))
                    T_Level_18
v2 T_Level_18
v3 T_Level_18
v3
                    (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                       (\ AgdaAny
v8 ->
                          (T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Kind_6 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'refl_160
                            ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                               (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v4)))
                       (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
v3))
                    AgdaAny
v6)
                 AgdaAny
v7)
              ((T_SymmetricKind_86 -> AgdaAny -> AgdaAny)
-> T_SymmetricKind_86 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_SymmetricKind_86 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_SK'45'sym_168 T_SymmetricKind_86
v4
                 AgdaAny
v5)))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v7 ->
            ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8764'_302
              (\ AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
                 (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'trans_164
                   ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                      (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v4)))
              T_Level_18
v0 T_Level_18
v1 T_Level_18
v2
              (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8764'_302
                 (\ AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
                    (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'trans_164
                      ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                         (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v4)))
                 T_Level_18
v1 T_Level_18
v3 T_Level_18
v2
                 (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8764'_302
                    (\ AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
                       (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'trans_164
                         ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                            (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v4)))
                    T_Level_18
v3 T_Level_18
v2 T_Level_18
v2
                    (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_494
                       (\ AgdaAny
v8 ->
                          (T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_Kind_6 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'refl_160
                            ((T_SymmetricKind_86 -> T_Kind_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_SymmetricKind_86 -> T_Kind_6
MAlonzo.Code.Function.Related.Propositional.d_'8970'_'8971'_92
                               (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v4)))
                       (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
v2))
                    ((T_SymmetricKind_86 -> AgdaAny -> AgdaAny)
-> T_SymmetricKind_86 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_SymmetricKind_86 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_SK'45'sym_168 T_SymmetricKind_86
v4
                       AgdaAny
v6))
                 AgdaAny
v7)
              AgdaAny
v5))
-- Function.Related.TypeIsomorphisms.∃-≡
d_'8707''45''8801'_618 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8707''45''8801'_618 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Inverse_2122
d_'8707''45''8801'_618 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 AgdaAny
v4
  = AgdaAny -> T_Inverse_2122
du_'8707''45''8801'_618 AgdaAny
v4
du_'8707''45''8801'_618 ::
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8707''45''8801'_618 :: AgdaAny -> T_Inverse_2122
du_'8707''45''8801'_618 AgdaAny
v0
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122)
-> AgdaAny -> AgdaAny -> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            (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
v0)
              ((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
forall a. a
erased (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
      ((T_Σ_14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
du_'46'extendedlambda2_626)
-- Function.Related.TypeIsomorphisms..extendedlambda2
d_'46'extendedlambda2_626 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
d_'46'extendedlambda2_626 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Σ_14
-> AgdaAny
d_'46'extendedlambda2_626 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 T_Σ_14
v5
  = T_Σ_14 -> AgdaAny
du_'46'extendedlambda2_626 T_Σ_14
v5
du_'46'extendedlambda2_626 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
du_'46'extendedlambda2_626 :: T_Σ_14 -> AgdaAny
du_'46'extendedlambda2_626 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2
        -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
             T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.TypeIsomorphisms..extendedlambda3
d_'46'extendedlambda3_630 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'46'extendedlambda3_630 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Σ_14
-> T__'8801'__12
d_'46'extendedlambda3_630 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased