{-# 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
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- 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_1960
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_1960
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_1960
du_Σ'45'assoc_32
du_Σ'45'assoc_32 :: MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_Σ'45'assoc_32 :: T_Inverse_1960
du_Σ'45'assoc_32
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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_1960
d_'215''45'comm_42 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'215''45'comm_42 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_1960
du_'215''45'comm_42
du_'215''45'comm_42 :: MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'215''45'comm_42 :: T_Inverse_1960
du_'215''45'comm_42
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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_1960
d_'215''45'identity'737'_50 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'215''45'identity'737'_50 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_1960
du_'215''45'identity'737'_50
du_'215''45'identity'737'_50 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'215''45'identity'737'_50 :: T_Inverse_1960
du_'215''45'identity'737'_50
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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_1960
d_'215''45'identity'691'_58 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'215''45'identity'691'_58 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_1960
du_'215''45'identity'691'_58
du_'215''45'identity'691'_58 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'215''45'identity'691'_58 :: T_Inverse_1960
du_'215''45'identity'691'_58
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'identity'737'_50)
      (\ AgdaAny
v0 -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
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_1960
d_'215''45'zero'737'_74 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'215''45'zero'737'_74 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_1960
du_'215''45'zero'737'_74
du_'215''45'zero'737'_74 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'215''45'zero'737'_74 :: T_Inverse_1960
du_'215''45'zero'737'_74
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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_1960
d_'215''45'zero'691'_86 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'215''45'zero'691'_86 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_1960
du_'215''45'zero'691'_86
du_'215''45'zero'691'_86 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'215''45'zero'691'_86 :: T_Inverse_1960
du_'215''45'zero'691'_86
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'zero'737'_74)
      (\ AgdaAny
v0 -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
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_1960
d_'8846''45'assoc_104 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'8846''45'assoc_104 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_1960
du_'8846''45'assoc_104
du_'8846''45'assoc_104 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8846''45'assoc_104 :: T_Inverse_1960
du_'8846''45'assoc_104
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      (((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_1960
d_'8846''45'comm_124 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'8846''45'comm_124 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_1960
du_'8846''45'comm_124
du_'8846''45'comm_124 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8846''45'comm_124 :: T_Inverse_1960
du_'8846''45'comm_124
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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_1960
d_'8846''45'identity'737'_128 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'8846''45'identity'737'_128 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Inverse_1960
du_'8846''45'identity'737'_128
du_'8846''45'identity'737'_128 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8846''45'identity'737'_128 :: T_Inverse_1960
du_'8846''45'identity'737'_128
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      (((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_1960
d_'8846''45'identity'691'_136 :: T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'8846''45'identity'691'_136 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Inverse_1960
du_'8846''45'identity'691'_136
du_'8846''45'identity'691'_136 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8846''45'identity'691'_136 :: T_Inverse_1960
du_'8846''45'identity'691'_136
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      (((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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'8846''45'identity'737'_128)
      (\ AgdaAny
v0 -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'8846''45'identity'691'_136)
-- Function.Related.TypeIsomorphisms.×-distribˡ-⊎
d_'215''45'distrib'737''45''8846'_150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'215''45'distrib'737''45''8846'_150 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'215''45'distrib'737''45''8846'_150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960
du_'215''45'distrib'737''45''8846'_150
du_'215''45'distrib'737''45''8846'_150 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'215''45'distrib'737''45''8846'_150 :: T_Inverse_1960
du_'215''45'distrib'737''45''8846'_150
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      (((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_'215''45'distrib'691''45''8846'_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'215''45'distrib'691''45''8846'_172 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_1960
d_'215''45'distrib'691''45''8846'_172 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_1960
du_'215''45'distrib'691''45''8846'_172
du_'215''45'distrib'691''45''8846'_172 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'215''45'distrib'691''45''8846'_172 :: T_Inverse_1960
du_'215''45'distrib'691''45''8846'_172
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      (((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''8242'_66
            (((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''8242'_66
         (((AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8321'_138
            ((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) -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8321'_138
            ((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_'215''45'distrib'45''8846'_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'distrib'45''8846'_190 :: T_Level_18 -> T_Σ_14
d_'215''45'distrib'45''8846'_190 ~T_Level_18
v0
  = T_Σ_14
du_'215''45'distrib'45''8846'_190
du_'215''45'distrib'45''8846'_190 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'distrib'45''8846'_190 :: T_Σ_14
du_'215''45'distrib'45''8846'_190
  = (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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'distrib'737''45''8846'_150)
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'distrib'691''45''8846'_172)
-- Function.Related.TypeIsomorphisms.×-isMagma
d_'215''45'isMagma_198 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'215''45'isMagma_198 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMagma_176
d_'215''45'isMagma_198 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsMagma_176
du_'215''45'isMagma_198 T_SymmetricKind_86
v0
du_'215''45'isMagma_198 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'215''45'isMagma_198 :: T_SymmetricKind_86 -> T_IsMagma_176
du_'215''45'isMagma_198 T_SymmetricKind_86
v0
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_176)
-> AgdaAny -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
      ((T_SymmetricKind_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SymmetricKind_86 -> T_IsEquivalence_26
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_206 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_68
d_'215''45'magma_206 :: T_SymmetricKind_86 -> T_Level_18 -> T_Magma_68
d_'215''45'magma_206 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Magma_68
du_'215''45'magma_206 T_SymmetricKind_86
v0
du_'215''45'magma_206 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_68
du_'215''45'magma_206 :: T_SymmetricKind_86 -> T_Magma_68
du_'215''45'magma_206 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176 -> T_Magma_68)
-> AgdaAny -> AgdaAny -> T_Magma_68
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176 -> T_Magma_68
MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279 AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMagma_176
du_'215''45'isMagma_198 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.×-isSemigroup
d_'215''45'isSemigroup_216 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'215''45'isSemigroup_216 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsSemigroup_472
d_'215''45'isSemigroup_216 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsSemigroup_472
du_'215''45'isSemigroup_216 T_SymmetricKind_86
v0
du_'215''45'isSemigroup_216 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'215''45'isSemigroup_216 :: T_SymmetricKind_86 -> T_IsSemigroup_472
du_'215''45'isSemigroup_216 T_SymmetricKind_86
v0
  = (T_IsMagma_176
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe
      T_IsMagma_176
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
      ((T_SymmetricKind_86 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMagma_176
du_'215''45'isMagma_198 (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_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_Σ'45'assoc_32)))
-- Function.Related.TypeIsomorphisms.×-semigroup
d_'215''45'semigroup_230 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_'215''45'semigroup_230 :: T_SymmetricKind_86 -> T_Level_18 -> T_Semigroup_536
d_'215''45'semigroup_230 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Semigroup_536
du_'215''45'semigroup_230 T_SymmetricKind_86
v0
du_'215''45'semigroup_230 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
du_'215''45'semigroup_230 :: T_SymmetricKind_86 -> T_Semigroup_536
du_'215''45'semigroup_230 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_472 -> T_Semigroup_536)
-> AgdaAny -> AgdaAny -> T_Semigroup_536
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_472 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793 AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsSemigroup_472) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsSemigroup_472
du_'215''45'isSemigroup_216 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.×-isMonoid
d_'215''45'isMonoid_240 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_'215''45'isMonoid_240 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMonoid_686
d_'215''45'isMonoid_240 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsMonoid_686
du_'215''45'isMonoid_240 T_SymmetricKind_86
v0
du_'215''45'isMonoid_240 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
du_'215''45'isMonoid_240 :: T_SymmetricKind_86 -> T_IsMonoid_686
du_'215''45'isMonoid_240 T_SymmetricKind_86
v0
  = (T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686)
-> AgdaAny -> AgdaAny -> T_IsMonoid_686
forall a b. a -> b
coe
      T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
      ((T_SymmetricKind_86 -> T_IsSemigroup_472) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsSemigroup_472
du_'215''45'isSemigroup_216 (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_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'identity'737'_50)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_6 -> T_Inverse_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'identity'691'_58))))
-- Function.Related.TypeIsomorphisms.×-monoid
d_'215''45'monoid_248 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_'215''45'monoid_248 :: T_SymmetricKind_86 -> T_Level_18 -> T_Monoid_882
d_'215''45'monoid_248 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Monoid_882
du_'215''45'monoid_248 T_SymmetricKind_86
v0
du_'215''45'monoid_248 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_'215''45'monoid_248 :: T_SymmetricKind_86 -> T_Monoid_882
du_'215''45'monoid_248 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_686 -> T_Monoid_882)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_686 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_16157 AgdaAny
forall a. a
erased
      AgdaAny
forall a. a
erased ((T_SymmetricKind_86 -> T_IsMonoid_686) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMonoid_686
du_'215''45'isMonoid_240 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.×-isCommutativeMonoid
d_'215''45'isCommutativeMonoid_258 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
d_'215''45'isCommutativeMonoid_258 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeMonoid_736
d_'215''45'isCommutativeMonoid_258 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_IsCommutativeMonoid_736
du_'215''45'isCommutativeMonoid_258 T_SymmetricKind_86
v0
du_'215''45'isCommutativeMonoid_258 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
du_'215''45'isCommutativeMonoid_258 :: T_SymmetricKind_86 -> T_IsCommutativeMonoid_736
du_'215''45'isCommutativeMonoid_258 T_SymmetricKind_86
v0
  = (T_IsMonoid_686
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_736)
-> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_736
forall a b. a -> b
coe
      T_IsMonoid_686
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_736
MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_17695
      ((T_SymmetricKind_86 -> T_IsMonoid_686) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMonoid_686
du_'215''45'isMonoid_240 (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_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'comm_42)))
-- Function.Related.TypeIsomorphisms.×-commutativeMonoid
d_'215''45'commutativeMonoid_270 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
d_'215''45'commutativeMonoid_270 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeMonoid_962
d_'215''45'commutativeMonoid_270 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_CommutativeMonoid_962
du_'215''45'commutativeMonoid_270 T_SymmetricKind_86
v0
du_'215''45'commutativeMonoid_270 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
du_'215''45'commutativeMonoid_270 :: T_SymmetricKind_86 -> T_CommutativeMonoid_962
du_'215''45'commutativeMonoid_270 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeMonoid_736 -> T_CommutativeMonoid_962)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_CommutativeMonoid_962
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid_736 -> T_CommutativeMonoid_962
MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_17931
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_SymmetricKind_86 -> T_IsCommutativeMonoid_736)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeMonoid_736
du_'215''45'isCommutativeMonoid_258 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.⊎-isMagma
d_'8846''45'isMagma_280 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8846''45'isMagma_280 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMagma_176
d_'8846''45'isMagma_280 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsMagma_176
du_'8846''45'isMagma_280 T_SymmetricKind_86
v0
du_'8846''45'isMagma_280 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_176
du_'8846''45'isMagma_280 :: T_SymmetricKind_86 -> T_IsMagma_176
du_'8846''45'isMagma_280 T_SymmetricKind_86
v0
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_176)
-> AgdaAny -> AgdaAny -> T_IsMagma_176
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
      ((T_SymmetricKind_86 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_SymmetricKind_86 -> T_IsEquivalence_26
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_288 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_68
d_'8846''45'magma_288 :: T_SymmetricKind_86 -> T_Level_18 -> T_Magma_68
d_'8846''45'magma_288 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Magma_68
du_'8846''45'magma_288 T_SymmetricKind_86
v0
du_'8846''45'magma_288 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_68
du_'8846''45'magma_288 :: T_SymmetricKind_86 -> T_Magma_68
du_'8846''45'magma_288 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176 -> T_Magma_68)
-> AgdaAny -> AgdaAny -> T_Magma_68
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_176 -> T_Magma_68
MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279 AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMagma_176
du_'8846''45'isMagma_280 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.⊎-isSemigroup
d_'8846''45'isSemigroup_298 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8846''45'isSemigroup_298 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsSemigroup_472
d_'8846''45'isSemigroup_298 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_IsSemigroup_472
du_'8846''45'isSemigroup_298 T_SymmetricKind_86
v0
du_'8846''45'isSemigroup_298 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
du_'8846''45'isSemigroup_298 :: T_SymmetricKind_86 -> T_IsSemigroup_472
du_'8846''45'isSemigroup_298 T_SymmetricKind_86
v0
  = (T_IsMagma_176
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_472
forall a b. a -> b
coe
      T_IsMagma_176
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
      ((T_SymmetricKind_86 -> T_IsMagma_176) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMagma_176
du_'8846''45'isMagma_280 (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_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'8846''45'assoc_104)))
-- Function.Related.TypeIsomorphisms.⊎-semigroup
d_'8846''45'semigroup_312 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_'8846''45'semigroup_312 :: T_SymmetricKind_86 -> T_Level_18 -> T_Semigroup_536
d_'8846''45'semigroup_312 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Semigroup_536
du_'8846''45'semigroup_312 T_SymmetricKind_86
v0
du_'8846''45'semigroup_312 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
du_'8846''45'semigroup_312 :: T_SymmetricKind_86 -> T_Semigroup_536
du_'8846''45'semigroup_312 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_472 -> T_Semigroup_536)
-> AgdaAny -> AgdaAny -> T_Semigroup_536
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_472 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793 AgdaAny
forall a. a
erased
      ((T_SymmetricKind_86 -> T_IsSemigroup_472) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsSemigroup_472
du_'8846''45'isSemigroup_298 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.⊎-isMonoid
d_'8846''45'isMonoid_322 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_'8846''45'isMonoid_322 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsMonoid_686
d_'8846''45'isMonoid_322 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_IsMonoid_686
du_'8846''45'isMonoid_322 T_SymmetricKind_86
v0
du_'8846''45'isMonoid_322 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
du_'8846''45'isMonoid_322 :: T_SymmetricKind_86 -> T_IsMonoid_686
du_'8846''45'isMonoid_322 T_SymmetricKind_86
v0
  = (T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686)
-> AgdaAny -> AgdaAny -> T_IsMonoid_686
forall a b. a -> b
coe
      T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
      ((T_SymmetricKind_86 -> T_IsSemigroup_472) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsSemigroup_472
du_'8846''45'isSemigroup_298 (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_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'8846''45'identity'737'_128)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_6 -> T_Inverse_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'8846''45'identity'691'_136))))
-- Function.Related.TypeIsomorphisms.⊎-monoid
d_'8846''45'monoid_330 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
d_'8846''45'monoid_330 :: T_SymmetricKind_86 -> T_Level_18 -> T_Monoid_882
d_'8846''45'monoid_330 T_SymmetricKind_86
v0 ~T_Level_18
v1 = T_SymmetricKind_86 -> T_Monoid_882
du_'8846''45'monoid_330 T_SymmetricKind_86
v0
du_'8846''45'monoid_330 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_882
du_'8846''45'monoid_330 :: T_SymmetricKind_86 -> T_Monoid_882
du_'8846''45'monoid_330 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_686 -> T_Monoid_882)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_882
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_686 -> T_Monoid_882
MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_16157 AgdaAny
forall a. a
erased
      AgdaAny
forall a. a
erased ((T_SymmetricKind_86 -> T_IsMonoid_686) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMonoid_686
du_'8846''45'isMonoid_322 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.⊎-isCommutativeMonoid
d_'8846''45'isCommutativeMonoid_340 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
d_'8846''45'isCommutativeMonoid_340 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeMonoid_736
d_'8846''45'isCommutativeMonoid_340 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_IsCommutativeMonoid_736
du_'8846''45'isCommutativeMonoid_340 T_SymmetricKind_86
v0
du_'8846''45'isCommutativeMonoid_340 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
du_'8846''45'isCommutativeMonoid_340 :: T_SymmetricKind_86 -> T_IsCommutativeMonoid_736
du_'8846''45'isCommutativeMonoid_340 T_SymmetricKind_86
v0
  = (T_IsMonoid_686
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_736)
-> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_736
forall a b. a -> b
coe
      T_IsMonoid_686
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_736
MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_17695
      ((T_SymmetricKind_86 -> T_IsMonoid_686) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsMonoid_686
du_'8846''45'isMonoid_322 (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_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'8846''45'comm_124)))
-- Function.Related.TypeIsomorphisms.⊎-commutativeMonoid
d_'8846''45'commutativeMonoid_352 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
d_'8846''45'commutativeMonoid_352 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeMonoid_962
d_'8846''45'commutativeMonoid_352 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_CommutativeMonoid_962
du_'8846''45'commutativeMonoid_352 T_SymmetricKind_86
v0
du_'8846''45'commutativeMonoid_352 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
du_'8846''45'commutativeMonoid_352 :: T_SymmetricKind_86 -> T_CommutativeMonoid_962
du_'8846''45'commutativeMonoid_352 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeMonoid_736 -> T_CommutativeMonoid_962)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_CommutativeMonoid_962
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid_736 -> T_CommutativeMonoid_962
MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_17931
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_SymmetricKind_86 -> T_IsCommutativeMonoid_736)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeMonoid_736
du_'8846''45'isCommutativeMonoid_340 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.×-⊎-isCommutativeSemiring
d_'215''45''8846''45'isCommutativeSemiring_362 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678
d_'215''45''8846''45'isCommutativeSemiring_362 :: T_SymmetricKind_86 -> T_Level_18 -> T_IsCommutativeSemiring_1678
d_'215''45''8846''45'isCommutativeSemiring_362 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_IsCommutativeSemiring_1678
du_'215''45''8846''45'isCommutativeSemiring_362 T_SymmetricKind_86
v0
du_'215''45''8846''45'isCommutativeSemiring_362 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678
du_'215''45''8846''45'isCommutativeSemiring_362 :: T_SymmetricKind_86 -> T_IsCommutativeSemiring_1678
du_'215''45''8846''45'isCommutativeSemiring_362 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsCommutativeSemiring'737'_2970
 -> T_IsCommutativeSemiring_1678)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring_1678
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'737'_2970
-> T_IsCommutativeSemiring_1678
MAlonzo.Code.Algebra.Structures.Biased.du_isCommutativeSemiring_2996
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_IsCommutativeMonoid_736
 -> T_IsCommutativeMonoid_736
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> T_IsCommutativeSemiring'737'_2970)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_736
-> T_IsCommutativeMonoid_736
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_2970
MAlonzo.Code.Algebra.Structures.Biased.C_IsCommutativeSemiring'737''46'constructor_43731
         ((T_SymmetricKind_86 -> T_IsCommutativeMonoid_736)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeMonoid_736
du_'8846''45'isCommutativeMonoid_340 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
         ((T_SymmetricKind_86 -> T_IsCommutativeMonoid_736)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeMonoid_736
du_'215''45'isCommutativeMonoid_258 (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_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'distrib'691''45''8846'_172)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_6 -> T_Inverse_1960 -> AgdaAny)
-> T_Kind_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> 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_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
du_'215''45'zero'737'_74))))
-- Function.Related.TypeIsomorphisms.×-⊎-commutativeSemiring
d_'215''45''8846''45'commutativeSemiring_376 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2446
d_'215''45''8846''45'commutativeSemiring_376 :: T_SymmetricKind_86 -> T_Level_18 -> T_CommutativeSemiring_2446
d_'215''45''8846''45'commutativeSemiring_376 T_SymmetricKind_86
v0 ~T_Level_18
v1
  = T_SymmetricKind_86 -> T_CommutativeSemiring_2446
du_'215''45''8846''45'commutativeSemiring_376 T_SymmetricKind_86
v0
du_'215''45''8846''45'commutativeSemiring_376 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2446
du_'215''45''8846''45'commutativeSemiring_376 :: T_SymmetricKind_86 -> T_CommutativeSemiring_2446
du_'215''45''8846''45'commutativeSemiring_376 T_SymmetricKind_86
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_IsCommutativeSemiring_1678
 -> T_CommutativeSemiring_2446)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_CommutativeSemiring_2446
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring_1678
-> T_CommutativeSemiring_2446
MAlonzo.Code.Algebra.Bundles.C_CommutativeSemiring'46'constructor_44731
      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_1678)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86 -> T_IsCommutativeSemiring_1678
du_'215''45''8846''45'isCommutativeSemiring_362 (T_SymmetricKind_86 -> AgdaAny
forall a b. a -> b
coe T_SymmetricKind_86
v0))
-- Function.Related.TypeIsomorphisms.ΠΠ↔ΠΠ
d_ΠΠ'8596'ΠΠ_402 ::
  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_1960
d_ΠΠ'8596'ΠΠ_402 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_1960
d_ΠΠ'8596'ΠΠ_402 ~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_1960
du_ΠΠ'8596'ΠΠ_402
du_ΠΠ'8596'ΠΠ_402 :: MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_ΠΠ'8596'ΠΠ_402 :: T_Inverse_1960
du_ΠΠ'8596'ΠΠ_402
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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'_428 ::
  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_1960
d_'8707''8707''8596''8707''8707'_428 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_1960
d_'8707''8707''8596''8707''8707'_428 ~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_1960
du_'8707''8707''8596''8707''8707'_428
du_'8707''8707''8596''8707''8707'_428 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8707''8707''8596''8707''8707'_428 :: T_Inverse_1960
du_'8707''8707''8596''8707''8707'_428
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_to_444) ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_from_460)
-- Function.Related.TypeIsomorphisms._.to
d_to_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.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to_444 :: 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_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_Σ_14
v6 = T_Σ_14 -> T_Σ_14
du_to_444 T_Σ_14
v6
du_to_444 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to_444 :: T_Σ_14 -> T_Σ_14
du_to_444 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_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_from_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_from_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_from_460 T_Σ_14
v6
du_from_460 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_460 :: T_Σ_14 -> T_Σ_14
du_from_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.Π↔Π
d_Π'8596'Π_480 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_Π'8596'Π_480 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
d_Π'8596'Π_480 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 = T_Inverse_1960
du_Π'8596'Π_480
du_Π'8596'Π_480 :: MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_Π'8596'Π_480 :: T_Inverse_1960
du_Π'8596'Π_480
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((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'_486 ::
  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_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'8594''45'cong'45''8660'_486 :: 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_1714
-> T_Equivalence_1714
-> T_Equivalence_1714
d_'8594''45'cong'45''8660'_486 ~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_1714
v8
                               T_Equivalence_1714
v9
  = T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du_'8594''45'cong'45''8660'_486 T_Equivalence_1714
v8 T_Equivalence_1714
v9
du_'8594''45'cong'45''8660'_486 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'8594''45'cong'45''8660'_486 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du_'8594''45'cong'45''8660'_486 T_Equivalence_1714
v0 T_Equivalence_1714
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 T_Equivalence_1714
v1
              (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 ((T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726 T_Equivalence_1714
v0 AgdaAny
v3))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726 T_Equivalence_1714
v1
              (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 ((T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 T_Equivalence_1714
v0 AgdaAny
v3))))
-- Function.Related.TypeIsomorphisms.→-cong-↔
d_'8594''45'cong'45''8596'_508 ::
  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_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'8594''45'cong'45''8596'_508 :: 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_1960
-> T_Inverse_1960
-> T_Inverse_1960
d_'8594''45'cong'45''8596'_508 ~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_1960
v10 T_Inverse_1960
v11
  = T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_'8594''45'cong'45''8596'_508 T_Inverse_1960
v10 T_Inverse_1960
v11
du_'8594''45'cong'45''8596'_508 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8594''45'cong'45''8596'_508 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_'8594''45'cong'45''8596'_508 T_Inverse_1960
v0 T_Inverse_1960
v1
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 T_Inverse_1960
v1
              (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v0 AgdaAny
v3))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v1
              (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 T_Inverse_1960
v0 AgdaAny
v3))))
-- Function.Related.TypeIsomorphisms.→-cong
d_'8594''45'cong_544 ::
  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_544 :: 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_544 ~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_544 T_SymmetricKind_86
v6
du_'8594''45'cong_544 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_'8594''45'cong_544 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8594''45'cong_544 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_1714 -> T_Equivalence_1714 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du_'8594''45'cong'45''8660'_486
      T_SymmetricKind_86
MAlonzo.Code.Function.Related.Propositional.C_bijection_90
        -> (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du_'8594''45'cong'45''8596'_508
      T_SymmetricKind_86
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.TypeIsomorphisms.¬-cong-⇔
d_'172''45'cong'45''8660'_554 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'172''45'cong'45''8660'_554 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1714
-> T_Equivalence_1714
d_'172''45'cong'45''8660'_554 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Equivalence_1714
v4
  = T_Equivalence_1714 -> T_Equivalence_1714
du_'172''45'cong'45''8660'_554 T_Equivalence_1714
v4
du_'172''45'cong'45''8660'_554 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'172''45'cong'45''8660'_554 :: T_Equivalence_1714 -> T_Equivalence_1714
du_'172''45'cong'45''8660'_554 T_Equivalence_1714
v0
  = (T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du_'8594''45'cong'45''8660'_486 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0)
      (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
MAlonzo.Code.Function.Construct.Identity.du_'8660''45'id_814)
-- Function.Related.TypeIsomorphisms.¬-cong
d_'172''45'cong_564 ::
  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_564 :: 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_564 ~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_564 T_SymmetricKind_86
v4 AgdaAny
v7
du_'172''45'cong_564 ::
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  AgdaAny -> AgdaAny
du_'172''45'cong_564 :: T_SymmetricKind_86 -> AgdaAny -> AgdaAny
du_'172''45'cong_564 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_544 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_574 ::
  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_1714
d_Related'45'cong_574 :: 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_1714
d_Related'45'cong_574 ~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_1714
du_Related'45'cong_574 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_574 ::
  () ->
  () ->
  () ->
  () ->
  MAlonzo.Code.Function.Related.Propositional.T_SymmetricKind_86 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_Related'45'cong_574 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_SymmetricKind_86
-> AgdaAny
-> AgdaAny
-> T_Equivalence_1714
du_Related'45'cong_574 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_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
      ((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'_300
              (\ 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'_300
                 (\ 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'_300
                    (\ 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'_492
                       (\ 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'_300
              (\ 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'_300
                 (\ 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'_300
                    (\ 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'_492
                       (\ 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.True↔
d_True'8596'_606 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_True'8596'_606 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T_Inverse_1960
d_True'8596'_606 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_20
v2 ~AgdaAny -> AgdaAny -> T__'8801'__12
v3 = T_Dec_20 -> T_Inverse_1960
du_True'8596'_606 T_Dec_20
v2
du_True'8596'_606 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_True'8596'_606 :: T_Dec_20 -> T_Inverse_1960
du_True'8596'_606 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                       (\ AgdaAny
v3 ->
                          (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)))
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
                    (((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366 AgdaAny
forall a. a
erased
                       ((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38
                          (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)))
      T_Dec_20
_ -> T_Inverse_1960
forall a. a
MAlonzo.RTE.mazUnreachableError