{-# 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
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.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Function.Inverse
import qualified MAlonzo.Code.Function.Related
import qualified MAlonzo.Code.Level
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Function.Related.TypeIsomorphisms.Σ-assoc
d_Σ'45'assoc_22 ::
  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.Inverse.T_Inverse_58
d_Σ'45'assoc_22 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_58
d_Σ'45'assoc_22 ~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_58
du_Σ'45'assoc_22
du_Σ'45'assoc_22 :: MAlonzo.Code.Function.Inverse.T_Inverse_58
du_Σ'45'assoc_22 :: T_Inverse_58
du_Σ'45'assoc_22
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((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
              ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                 ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (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
                 ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                    ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)))
                 ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)))))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 ->
            case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe
                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                            ((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
v3))
                            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
                     T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
              T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-comm
d_'215''45'comm_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'215''45'comm_52 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'215''45'comm_52 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_58
du_'215''45'comm_52
du_'215''45'comm_52 :: MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45'comm_52 :: T_Inverse_58
du_'215''45'comm_52
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_swap_386)
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_swap_386) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-identityˡ
d_'215''45'identity'737'_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'215''45'identity'737'_60 :: T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'215''45'identity'737'_60 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_58
du_'215''45'identity'737'_60
du_'215''45'identity'737'_60 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45'identity'737'_60 :: T_Inverse_58
du_'215''45'identity'737'_60
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((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)))
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-identityʳ
d_'215''45'identity'691'_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'215''45'identity'691'_68 :: T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'215''45'identity'691'_68 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_58
du_'215''45'identity'691'_68
du_'215''45'identity'691'_68 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45'identity'691'_68 :: T_Inverse_58
du_'215''45'identity'691'_68
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((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))))
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-identity
d_'215''45'identity_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'identity_78 :: T_Level_18 -> T_Σ_14
d_'215''45'identity_78 ~T_Level_18
v0 = T_Σ_14
du_'215''45'identity_78
du_'215''45'identity_78 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'identity_78 :: T_Σ_14
du_'215''45'identity_78
  = (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_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'identity'737'_60)
      (\ AgdaAny
v0 -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'identity'691'_68)
-- Function.Related.TypeIsomorphisms.×-zeroˡ
d_'215''45'zero'737'_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'215''45'zero'737'_84 :: T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'215''45'zero'737'_84 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_58
du_'215''45'zero'737'_84
du_'215''45'zero'737'_84 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45'zero'737'_84 :: T_Inverse_58
du_'215''45'zero'737'_84
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((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.du_'60'_'44'_'62'_132 ((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))
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-zeroʳ
d_'215''45'zero'691'_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'215''45'zero'691'_96 :: T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'215''45'zero'691'_96 ~T_Level_18
v0 ~T_Level_18
v1 = T_Inverse_58
du_'215''45'zero'691'_96
du_'215''45'zero'691'_96 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45'zero'691'_96 :: T_Inverse_58
du_'215''45'zero'691'_96
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((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.du_'60'_'44'_'62'_132
         (\ 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)))
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-zero
d_'215''45'zero_108 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'zero_108 :: T_Level_18 -> T_Σ_14
d_'215''45'zero_108 ~T_Level_18
v0 = T_Σ_14
du_'215''45'zero_108
du_'215''45'zero_108 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'zero_108 :: T_Σ_14
du_'215''45'zero_108
  = (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_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'zero'737'_84)
      (\ AgdaAny
v0 -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'zero'691'_96)
-- Function.Related.TypeIsomorphisms.⊎-assoc
d_'8846''45'assoc_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'8846''45'assoc_114 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'8846''45'assoc_114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_58
du_'8846''45'assoc_114
du_'8846''45'assoc_114 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'8846''45'assoc_114 :: T_Inverse_58
du_'8846''45'assoc_114
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      (((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'__226
               ((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'__226
            ((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'__226
            ((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'__226
               ((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)))
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.⊎-comm
d_'8846''45'comm_138 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'8846''45'comm_138 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'8846''45'comm_138 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_58
du_'8846''45'comm_138
du_'8846''45'comm_138 :: MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'8846''45'comm_138 :: T_Inverse_58
du_'8846''45'comm_138
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((T__'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) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.⊎-identityˡ
d_'8846''45'identity'737'_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'8846''45'identity'737'_142 :: T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'8846''45'identity'737'_142 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Inverse_58
du_'8846''45'identity'737'_142
du_'8846''45'identity'737'_142 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'8846''45'identity'737'_142 :: T_Inverse_58
du_'8846''45'identity'737'_142
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      (((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) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.⊎-identityʳ
d_'8846''45'identity'691'_150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'8846''45'identity'691'_150 :: T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'8846''45'identity'691'_150 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Inverse_58
du_'8846''45'identity'691'_150
du_'8846''45'identity'691'_150 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'8846''45'identity'691'_150 :: T_Inverse_58
du_'8846''45'identity'691'_150
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      (((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) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.⊎-identity
d_'8846''45'identity_158 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8846''45'identity_158 :: T_Level_18 -> T_Σ_14
d_'8846''45'identity_158 ~T_Level_18
v0 = T_Σ_14
du_'8846''45'identity_158
du_'8846''45'identity_158 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8846''45'identity_158 :: T_Σ_14
du_'8846''45'identity_158
  = (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_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'8846''45'identity'737'_142)
      (\ AgdaAny
v0 -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'8846''45'identity'691'_150)
-- Function.Related.TypeIsomorphisms.×-distribˡ-⊎
d_'215''45'distrib'737''45''8846'_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'215''45'distrib'737''45''8846'_164 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'215''45'distrib'737''45''8846'_164 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_58
du_'215''45'distrib'737''45''8846'_164
du_'215''45'distrib'737''45''8846'_164 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45'distrib'737''45''8846'_164 :: T_Inverse_58
du_'215''45'distrib'737''45''8846'_164
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.du_uncurry_264
         ((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'__226
                    ((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'__226
                    ((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.du_map'8322'_170
            ((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.du_map'8322'_170
            ((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))))
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-distribʳ-⊎
d_'215''45'distrib'691''45''8846'_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> () -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'215''45'distrib'691''45''8846'_186 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Inverse_58
d_'215''45'distrib'691''45''8846'_186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3
  = T_Inverse_58
du_'215''45'distrib'691''45''8846'_186
du_'215''45'distrib'691''45''8846'_186 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45'distrib'691''45''8846'_186 :: T_Inverse_58
du_'215''45'distrib'691''45''8846'_186
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.du_uncurry_264
         (((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.du_curry_244
               ((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.du_curry_244
               ((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.du_map'8321'_158
            ((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.du_map'8321'_158
            ((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
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-distrib-⊎
d_'215''45'distrib'45''8846'_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45'distrib'45''8846'_204 :: T_Level_18 -> T_Σ_14
d_'215''45'distrib'45''8846'_204 ~T_Level_18
v0
  = T_Σ_14
du_'215''45'distrib'45''8846'_204
du_'215''45'distrib'45''8846'_204 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45'distrib'45''8846'_204 :: T_Σ_14
du_'215''45'distrib'45''8846'_204
  = (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_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'distrib'737''45''8846'_164)
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'distrib'691''45''8846'_186)
-- Function.Related.TypeIsomorphisms.×-isMagma
d_'215''45'isMagma_212 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'215''45'isMagma_212 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_IsMagma_86
d_'215''45'isMagma_212 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_IsMagma_86
du_'215''45'isMagma_212 T_Symmetric'45'kind_142
v0
du_'215''45'isMagma_212 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'215''45'isMagma_212 :: T_Symmetric'45'kind_142 -> T_IsMagma_86
du_'215''45'isMagma_212 T_Symmetric'45'kind_142
v0
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
      ((T_Symmetric'45'kind_142 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Symmetric'45'kind_142 -> T_IsEquivalence_26
MAlonzo.Code.Function.Related.du_SK'45'isEquivalence_292 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Product.Function.NonDependent.Propositional.du__'215''45'cong__102
              ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))))
-- Function.Related.TypeIsomorphisms.×-magma
d_'215''45'magma_220 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
d_'215''45'magma_220 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_Magma_36
d_'215''45'magma_220 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_Magma_36
du_'215''45'magma_220 T_Symmetric'45'kind_142
v0
du_'215''45'magma_220 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
du_'215''45'magma_220 :: T_Symmetric'45'kind_142 -> T_Magma_36
du_'215''45'magma_220 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86 -> T_Magma_36)
-> AgdaAny -> AgdaAny -> T_Magma_36
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86 -> T_Magma_36
MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_581 AgdaAny
forall a. a
erased
      ((T_Symmetric'45'kind_142 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsMagma_86
du_'215''45'isMagma_212 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.×-isSemigroup
d_'215''45'isSemigroup_230 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'215''45'isSemigroup_230 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_IsSemigroup_194
d_'215''45'isSemigroup_230 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_IsSemigroup_194
du_'215''45'isSemigroup_230 T_Symmetric'45'kind_142
v0
du_'215''45'isSemigroup_230 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'215''45'isSemigroup_230 :: T_Symmetric'45'kind_142 -> T_IsSemigroup_194
du_'215''45'isSemigroup_230 T_Symmetric'45'kind_142
v0
  = (T_IsMagma_86
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
      ((T_Symmetric'45'kind_142 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsMagma_86
du_'215''45'isMagma_212 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
              (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
              (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_Σ'45'assoc_22)))
-- Function.Related.TypeIsomorphisms.×-semigroup
d_'215''45'semigroup_244 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_'215''45'semigroup_244 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_Semigroup_206
d_'215''45'semigroup_244 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_Semigroup_206
du_'215''45'semigroup_244 T_Symmetric'45'kind_142
v0
du_'215''45'semigroup_244 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_'215''45'semigroup_244 :: T_Symmetric'45'kind_142 -> T_Semigroup_206
du_'215''45'semigroup_244 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_194 -> T_Semigroup_206)
-> AgdaAny -> AgdaAny -> T_Semigroup_206
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> T_Semigroup_206
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_3669 AgdaAny
forall a. a
erased
      ((T_Symmetric'45'kind_142 -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsSemigroup_194
du_'215''45'isSemigroup_230 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.×-isMonoid
d_'215''45'isMonoid_254 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_'215''45'isMonoid_254 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_IsMonoid_358
d_'215''45'isMonoid_254 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_IsMonoid_358
du_'215''45'isMonoid_254 T_Symmetric'45'kind_142
v0
du_'215''45'isMonoid_254 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
du_'215''45'isMonoid_254 :: T_Symmetric'45'kind_142 -> T_IsMonoid_358
du_'215''45'isMonoid_254 T_Symmetric'45'kind_142
v0
  = (T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny -> T_IsMonoid_358
forall a b. a -> b
coe
      T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_7687
      ((T_Symmetric'45'kind_142 -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsSemigroup_194
du_'215''45'isSemigroup_230 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
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_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
                 (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'identity'737'_60)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
                 (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'identity'691'_68))))
-- Function.Related.TypeIsomorphisms.×-monoid
d_'215''45'monoid_262 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'215''45'monoid_262 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_Monoid_506
d_'215''45'monoid_262 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_Monoid_506
du_'215''45'monoid_262 T_Symmetric'45'kind_142
v0
du_'215''45'monoid_262 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'215''45'monoid_262 :: T_Symmetric'45'kind_142 -> T_Monoid_506
du_'215''45'monoid_262 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_358 -> T_Monoid_506)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_358 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_8851 AgdaAny
forall a. a
erased
      AgdaAny
forall a. a
erased ((T_Symmetric'45'kind_142 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsMonoid_358
du_'215''45'isMonoid_254 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.×-isCommutativeMonoid
d_'215''45'isCommutativeMonoid_272 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
d_'215''45'isCommutativeMonoid_272 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_IsCommutativeMonoid_406
d_'215''45'isCommutativeMonoid_272 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1
  = T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406
du_'215''45'isCommutativeMonoid_272 T_Symmetric'45'kind_142
v0
du_'215''45'isCommutativeMonoid_272 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
du_'215''45'isCommutativeMonoid_272 :: T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406
du_'215''45'isCommutativeMonoid_272 T_Symmetric'45'kind_142
v0
  = (T_IsMonoid_358
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe
      T_IsMonoid_358
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_406
MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_9361
      ((T_Symmetric'45'kind_142 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsMonoid_358
du_'215''45'isMonoid_254 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
              (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
              (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'comm_52)))
-- Function.Related.TypeIsomorphisms.×-commutativeMonoid
d_'215''45'commutativeMonoid_284 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
d_'215''45'commutativeMonoid_284 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_CommutativeMonoid_582
d_'215''45'commutativeMonoid_284 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1
  = T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582
du_'215''45'commutativeMonoid_284 T_Symmetric'45'kind_142
v0
du_'215''45'commutativeMonoid_284 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
du_'215''45'commutativeMonoid_284 :: T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582
du_'215''45'commutativeMonoid_284 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeMonoid_406 -> T_CommutativeMonoid_582)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_CommutativeMonoid_582
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid_406 -> T_CommutativeMonoid_582
MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_10343
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406
du_'215''45'isCommutativeMonoid_272 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.⊎-isMagma
d_'8846''45'isMagma_294 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'8846''45'isMagma_294 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_IsMagma_86
d_'8846''45'isMagma_294 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_IsMagma_86
du_'8846''45'isMagma_294 T_Symmetric'45'kind_142
v0
du_'8846''45'isMagma_294 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'8846''45'isMagma_294 :: T_Symmetric'45'kind_142 -> T_IsMagma_86
du_'8846''45'isMagma_294 T_Symmetric'45'kind_142
v0
  = (T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
      ((T_Symmetric'45'kind_142 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Symmetric'45'kind_142 -> T_IsEquivalence_26
MAlonzo.Code.Function.Related.du_SK'45'isEquivalence_292 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Sum.Function.Propositional.du__'8846''45'cong__100
              ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))))
-- Function.Related.TypeIsomorphisms.⊎-magma
d_'8846''45'magma_302 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
d_'8846''45'magma_302 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_Magma_36
d_'8846''45'magma_302 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_Magma_36
du_'8846''45'magma_302 T_Symmetric'45'kind_142
v0
du_'8846''45'magma_302 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_Magma_36
du_'8846''45'magma_302 :: T_Symmetric'45'kind_142 -> T_Magma_36
du_'8846''45'magma_302 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86 -> T_Magma_36)
-> AgdaAny -> AgdaAny -> T_Magma_36
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_86 -> T_Magma_36
MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_581 AgdaAny
forall a. a
erased
      ((T_Symmetric'45'kind_142 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsMagma_86
du_'8846''45'isMagma_294 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.⊎-isSemigroup
d_'8846''45'isSemigroup_312 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'8846''45'isSemigroup_312 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_IsSemigroup_194
d_'8846''45'isSemigroup_312 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1
  = T_Symmetric'45'kind_142 -> T_IsSemigroup_194
du_'8846''45'isSemigroup_312 T_Symmetric'45'kind_142
v0
du_'8846''45'isSemigroup_312 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'8846''45'isSemigroup_312 :: T_Symmetric'45'kind_142 -> T_IsSemigroup_194
du_'8846''45'isSemigroup_312 T_Symmetric'45'kind_142
v0
  = (T_IsMagma_86
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
      T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
      ((T_Symmetric'45'kind_142 -> T_IsMagma_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsMagma_86
du_'8846''45'isMagma_294 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
              (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
              (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'8846''45'assoc_114)))
-- Function.Related.TypeIsomorphisms.⊎-semigroup
d_'8846''45'semigroup_326 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_'8846''45'semigroup_326 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_Semigroup_206
d_'8846''45'semigroup_326 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_Semigroup_206
du_'8846''45'semigroup_326 T_Symmetric'45'kind_142
v0
du_'8846''45'semigroup_326 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_'8846''45'semigroup_326 :: T_Symmetric'45'kind_142 -> T_Semigroup_206
du_'8846''45'semigroup_326 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsSemigroup_194 -> T_Semigroup_206)
-> AgdaAny -> AgdaAny -> T_Semigroup_206
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> T_Semigroup_206
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_3669 AgdaAny
forall a. a
erased
      ((T_Symmetric'45'kind_142 -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsSemigroup_194
du_'8846''45'isSemigroup_312 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.⊎-isMonoid
d_'8846''45'isMonoid_336 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_'8846''45'isMonoid_336 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_IsMonoid_358
d_'8846''45'isMonoid_336 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_IsMonoid_358
du_'8846''45'isMonoid_336 T_Symmetric'45'kind_142
v0
du_'8846''45'isMonoid_336 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
du_'8846''45'isMonoid_336 :: T_Symmetric'45'kind_142 -> T_IsMonoid_358
du_'8846''45'isMonoid_336 T_Symmetric'45'kind_142
v0
  = (T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny -> T_IsMonoid_358
forall a b. a -> b
coe
      T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_7687
      ((T_Symmetric'45'kind_142 -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsSemigroup_194
du_'8846''45'isSemigroup_312 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
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_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
                 (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'8846''45'identity'737'_142)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
                 (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'8846''45'identity'691'_150))))
-- Function.Related.TypeIsomorphisms.⊎-monoid
d_'8846''45'monoid_344 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'8846''45'monoid_344 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_Monoid_506
d_'8846''45'monoid_344 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 = T_Symmetric'45'kind_142 -> T_Monoid_506
du_'8846''45'monoid_344 T_Symmetric'45'kind_142
v0
du_'8846''45'monoid_344 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'8846''45'monoid_344 :: T_Symmetric'45'kind_142 -> T_Monoid_506
du_'8846''45'monoid_344 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsMonoid_358 -> T_Monoid_506)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_358 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_8851 AgdaAny
forall a. a
erased
      AgdaAny
forall a. a
erased ((T_Symmetric'45'kind_142 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsMonoid_358
du_'8846''45'isMonoid_336 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.⊎-isCommutativeMonoid
d_'8846''45'isCommutativeMonoid_354 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
d_'8846''45'isCommutativeMonoid_354 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_IsCommutativeMonoid_406
d_'8846''45'isCommutativeMonoid_354 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1
  = T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406
du_'8846''45'isCommutativeMonoid_354 T_Symmetric'45'kind_142
v0
du_'8846''45'isCommutativeMonoid_354 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_406
du_'8846''45'isCommutativeMonoid_354 :: T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406
du_'8846''45'isCommutativeMonoid_354 T_Symmetric'45'kind_142
v0
  = (T_IsMonoid_358
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny -> T_IsCommutativeMonoid_406
forall a b. a -> b
coe
      T_IsMonoid_358
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeMonoid_406
MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_9361
      ((T_Symmetric'45'kind_142 -> T_IsMonoid_358) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsMonoid_358
du_'8846''45'isMonoid_336 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 ->
            (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
              (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
              (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'8846''45'comm_138)))
-- Function.Related.TypeIsomorphisms.⊎-commutativeMonoid
d_'8846''45'commutativeMonoid_366 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
d_'8846''45'commutativeMonoid_366 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_CommutativeMonoid_582
d_'8846''45'commutativeMonoid_366 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1
  = T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582
du_'8846''45'commutativeMonoid_366 T_Symmetric'45'kind_142
v0
du_'8846''45'commutativeMonoid_366 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
du_'8846''45'commutativeMonoid_366 :: T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582
du_'8846''45'commutativeMonoid_366 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_IsCommutativeMonoid_406 -> T_CommutativeMonoid_582)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_CommutativeMonoid_582
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsCommutativeMonoid_406 -> T_CommutativeMonoid_582
MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_10343
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406
du_'8846''45'isCommutativeMonoid_354 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.×-⊎-isCommutativeSemiring
d_'215''45''8846''45'isCommutativeSemiring_376 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1344
d_'215''45''8846''45'isCommutativeSemiring_376 :: T_Symmetric'45'kind_142
-> T_Level_18 -> T_IsCommutativeSemiring_1344
d_'215''45''8846''45'isCommutativeSemiring_376 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1
  = T_Symmetric'45'kind_142 -> T_IsCommutativeSemiring_1344
du_'215''45''8846''45'isCommutativeSemiring_376 T_Symmetric'45'kind_142
v0
du_'215''45''8846''45'isCommutativeSemiring_376 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1344
du_'215''45''8846''45'isCommutativeSemiring_376 :: T_Symmetric'45'kind_142 -> T_IsCommutativeSemiring_1344
du_'215''45''8846''45'isCommutativeSemiring_376 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_IsCommutativeSemiring'737'_1626
 -> T_IsCommutativeSemiring_1344)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring_1344
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsCommutativeSemiring'737'_1626
-> T_IsCommutativeSemiring_1344
MAlonzo.Code.Algebra.Structures.Biased.du_isCommutativeSemiring_1744
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_IsCommutativeMonoid_406
 -> T_IsCommutativeMonoid_406
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> T_IsCommutativeSemiring'737'_1626)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCommutativeMonoid_406
-> T_IsCommutativeMonoid_406
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsCommutativeSemiring'737'_1626
MAlonzo.Code.Algebra.Structures.Biased.C_IsCommutativeSemiring'737''46'constructor_21625
         ((T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406
du_'8846''45'isCommutativeMonoid_354 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
         ((T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsCommutativeMonoid_406
du_'215''45'isCommutativeMonoid_272 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
               (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
                 (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'distrib'691''45''8846'_186)))
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> T_Kind_52 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
                 (T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                 (T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe T_Inverse_58
du_'215''45'zero'737'_84))))
-- Function.Related.TypeIsomorphisms.×-⊎-commutativeSemiring
d_'215''45''8846''45'commutativeSemiring_390 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2094
d_'215''45''8846''45'commutativeSemiring_390 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_CommutativeSemiring_2094
d_'215''45''8846''45'commutativeSemiring_390 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1
  = T_Symmetric'45'kind_142 -> T_CommutativeSemiring_2094
du_'215''45''8846''45'commutativeSemiring_390 T_Symmetric'45'kind_142
v0
du_'215''45''8846''45'commutativeSemiring_390 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2094
du_'215''45''8846''45'commutativeSemiring_390 :: T_Symmetric'45'kind_142 -> T_CommutativeSemiring_2094
du_'215''45''8846''45'commutativeSemiring_390 T_Symmetric'45'kind_142
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_IsCommutativeSemiring_1344
 -> T_CommutativeSemiring_2094)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_CommutativeSemiring_2094
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_IsCommutativeSemiring_1344
-> T_CommutativeSemiring_2094
MAlonzo.Code.Algebra.Bundles.C_CommutativeSemiring'46'constructor_36513
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      ((T_Symmetric'45'kind_142 -> T_IsCommutativeSemiring_1344)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_IsCommutativeSemiring_1344
du_'215''45''8846''45'isCommutativeSemiring_376 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
-- Function.Related.TypeIsomorphisms.ΠΠ↔ΠΠ
d_ΠΠ'8596'ΠΠ_416 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58
d_ΠΠ'8596'ΠΠ_416 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_58
d_ΠΠ'8596'ΠΠ_416 ~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_58
du_ΠΠ'8596'ΠΠ_416
du_ΠΠ'8596'ΠΠ_416 :: MAlonzo.Code.Function.Inverse.T_Inverse_58
du_ΠΠ'8596'ΠΠ_416 :: T_Inverse_58
du_ΠΠ'8596'ΠΠ_416
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((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)) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms.∃∃↔∃∃
d_'8707''8707''8596''8707''8707'_442 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'8707''8707''8596''8707''8707'_442 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_58
d_'8707''8707''8596''8707''8707'_442 ~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_58
du_'8707''8707''8596''8707''8707'_442
du_'8707''8707''8596''8707''8707'_442 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'8707''8707''8596''8707''8707'_442 :: T_Inverse_58
du_'8707''8707''8596''8707''8707'_442
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156 ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_to_458)
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_from_474) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.to
d_to_458 ::
  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_458 :: 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_458 ~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_458 T_Σ_14
v6
du_to_458 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to_458 :: T_Σ_14 -> T_Σ_14
du_to_458 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_474 ::
  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_474 :: 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_474 ~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_474 T_Σ_14
v6
du_from_474 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_474 :: T_Σ_14 -> T_Σ_14
du_from_474 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'Π_498 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> ()) -> MAlonzo.Code.Function.Inverse.T_Inverse_58
d_Π'8596'Π_498 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_58
d_Π'8596'Π_498 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 = T_Inverse_58
du_Π'8596'Π_498
du_Π'8596'Π_498 :: MAlonzo.Code.Function.Inverse.T_Inverse_58
du_Π'8596'Π_498 :: T_Inverse_58
du_Π'8596'Π_498
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
      ((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)) AgdaAny
forall a. a
erased
      AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms._→-cong-⇔_
d__'8594''45'cong'45''8660'__528 ::
  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.Equivalence.T_Equivalence_16 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d__'8594''45'cong'45''8660'__528 :: 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_16
-> T_Equivalence_16
-> T_Equivalence_16
d__'8594''45'cong'45''8660'__528 ~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_16
v8
                                 T_Equivalence_16
v9
  = T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8594''45'cong'45''8660'__528 T_Equivalence_16
v8 T_Equivalence_16
v9
du__'8594''45'cong'45''8660'__528 ::
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du__'8594''45'cong'45''8660'__528 :: T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8594''45'cong'45''8660'__528 T_Equivalence_16
v0 T_Equivalence_16
v1
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_equivalence_56
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
              (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v1))
              (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny
v2
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                    (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v0)) AgdaAny
v3))))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
              (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v1))
              (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny
v2
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                    (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34 (T_Equivalence_16 -> T_Equivalence_16
forall a b. a -> b
coe T_Equivalence_16
v0)) AgdaAny
v3))))
-- Function.Related.TypeIsomorphisms.→-cong
d_'8594''45'cong_560 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  (() ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  () -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_'8594''45'cong_560 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (T_Level_18
    -> (AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> (T_Level_18
    -> (AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny)
    -> (AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> T_Symmetric'45'kind_142
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8594''45'cong_560 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v4 T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v5 T_Symmetric'45'kind_142
v6
  = (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_Symmetric'45'kind_142
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8594''45'cong_560 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_Symmetric'45'kind_142
v6
du_'8594''45'cong_560 ::
  (() ->
   (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.T_Symmetric'45'kind_142 ->
  () -> () -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du_'8594''45'cong_560 :: (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_Symmetric'45'kind_142
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8594''45'cong_560 T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v0 T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v1 T_Symmetric'45'kind_142
v2
  = case T_Symmetric'45'kind_142 -> T_Symmetric'45'kind_142
forall a b. a -> b
coe T_Symmetric'45'kind_142
v2 of
      T_Symmetric'45'kind_142
MAlonzo.Code.Function.Related.C_equivalence_144
        -> (AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 ->
                (T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8594''45'cong'45''8660'__528 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8))
      T_Symmetric'45'kind_142
MAlonzo.Code.Function.Related.C_bijection_146
        -> (AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
             (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 ->
                (T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Π_16 -> T_Π_16 -> T__InverseOf__20 -> T_Inverse_58
MAlonzo.Code.Function.Inverse.C_Inverse'46'constructor_3557
                  ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34
                     ((T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)))
                  ((T_Equivalence_16 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
                     ((T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)))
                  (((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T__InverseOf__20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T__InverseOf__20
MAlonzo.Code.Function.Inverse.C__InverseOf_'46'constructor_2103
                     ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                        (\ AgdaAny
v9 ->
                           (T_Level_18
 -> (AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> T__'8801'__12)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                             T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v0 AgdaAny
v3 (\ AgdaAny
v10 -> AgdaAny
v5)
                             ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                                (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
                                   ((T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)))
                                ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                   T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                                   (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34
                                      ((T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)))
                                   AgdaAny
v9))
                             AgdaAny
v9 AgdaAny
forall a. a
erased))
                     ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                        (\ AgdaAny
v9 ->
                           (T_Level_18
 -> (AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> T__'8801'__12)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                             T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v1 AgdaAny
v4 (\ AgdaAny
v10 -> AgdaAny
v6)
                             ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                                (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34
                                   ((T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)))
                                ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                   T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                                   (T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
                                      ((T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)))
                                   AgdaAny
v9))
                             AgdaAny
v9 AgdaAny
forall a. a
erased))))
      T_Symmetric'45'kind_142
_ -> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.TypeIsomorphisms._.A→C⇔B→D
d_A'8594'C'8660'B'8594'D_582 ::
  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.Inverse.T_Inverse_58 ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_A'8594'C'8660'B'8594'D_582 :: 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_58
-> T_Inverse_58
-> T_Equivalence_16
d_A'8594'C'8660'B'8594'D_582 ~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_58
v10 T_Inverse_58
v11
  = T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 T_Inverse_58
v10 T_Inverse_58
v11
du_A'8594'C'8660'B'8594'D_582 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 :: T_Inverse_58 -> T_Inverse_58 -> T_Equivalence_16
du_A'8594'C'8660'B'8594'D_582 T_Inverse_58
v0 T_Inverse_58
v1
  = (T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8594''45'cong'45''8660'__528
      ((T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> AgdaAny -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe
         T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
         (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
MAlonzo.Code.Function.Related.C_equivalence_58) T_Inverse_58
v0)
      ((T_Kind_52 -> T_Inverse_58 -> AgdaAny)
-> AgdaAny -> T_Inverse_58 -> AgdaAny
forall a b. a -> b
coe
         T_Kind_52 -> T_Inverse_58 -> AgdaAny
MAlonzo.Code.Function.Related.du_'8596''8658'_130
         (T_Kind_52 -> AgdaAny
forall a b. a -> b
coe T_Kind_52
MAlonzo.Code.Function.Related.C_equivalence_58) T_Inverse_58
v1)
-- Function.Related.TypeIsomorphisms.¬-cong-⇔
d_'172''45'cong'45''8660'_600 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_'172''45'cong'45''8660'_600 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_16
-> T_Equivalence_16
d_'172''45'cong'45''8660'_600 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Equivalence_16
v4
  = T_Equivalence_16 -> T_Equivalence_16
du_'172''45'cong'45''8660'_600 T_Equivalence_16
v4
du_'172''45'cong'45''8660'_600 ::
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_'172''45'cong'45''8660'_600 :: T_Equivalence_16 -> T_Equivalence_16
du_'172''45'cong'45''8660'_600 T_Equivalence_16
v0
  = (T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      T_Equivalence_16 -> T_Equivalence_16 -> T_Equivalence_16
du__'8594''45'cong'45''8660'__528 (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
v0)
      (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_id_66)
-- Function.Related.TypeIsomorphisms.¬-cong
d_'172''45'cong_614 ::
  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.T_Symmetric'45'kind_142 ->
  () -> () -> AgdaAny -> AgdaAny
d_'172''45'cong_614 :: 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_Symmetric'45'kind_142
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
d_'172''45'cong_614 ~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_Symmetric'45'kind_142
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny
v7
  = T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_'172''45'cong_614 T_Symmetric'45'kind_142
v4 AgdaAny
v7
du_'172''45'cong_614 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  AgdaAny -> AgdaAny
du_'172''45'cong_614 :: T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
du_'172''45'cong_614 T_Symmetric'45'kind_142
v0 AgdaAny
v1
  = ((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_Symmetric'45'kind_142
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Symmetric'45'kind_142
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      (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_Symmetric'45'kind_142
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_'8594''45'cong_560 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased T_Symmetric'45'kind_142
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
      AgdaAny
v1
      ((T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Kind_52 -> AgdaAny
MAlonzo.Code.Function.Related.du_K'45'reflexive_260
         ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0)))
-- Function.Related.TypeIsomorphisms.Related-cong
d_Related'45'cong_640 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  () ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_Related'45'cong_640 :: T_Symmetric'45'kind_142
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Equivalence_16
d_Related'45'cong_640 T_Symmetric'45'kind_142
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~T_Level_18
v8 AgdaAny
v9 AgdaAny
v10
  = T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny -> T_Equivalence_16
du_Related'45'cong_640 T_Symmetric'45'kind_142
v0 AgdaAny
v9 AgdaAny
v10
du_Related'45'cong_640 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_Related'45'cong_640 :: T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny -> T_Equivalence_16
du_Related'45'cong_640 T_Symmetric'45'kind_142
v0 AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_equivalence_56
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 ->
            (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du__'8764''10216'_'10217'__340
              ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
              ((T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny)
-> T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du_SK'45'sym_286 T_Symmetric'45'kind_142
v0 AgdaAny
v1)
              ((T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du__'8764''10216'_'10217'__340
                 ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                 ((T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du__'8764''10216'_'10217'__340
                    ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                    (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
                    ((T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Kind_52 -> AgdaAny
MAlonzo.Code.Function.Related.du__'8718'_410
                       ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0)))))))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 ->
            (T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du__'8764''10216'_'10217'__340
              ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
              ((T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du__'8764''10216'_'10217'__340
                 ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                 ((T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Kind_52 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du__'8764''10216'_'10217'__340
                    ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0))
                    ((T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny)
-> T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.du_SK'45'sym_286 T_Symmetric'45'kind_142
v0 AgdaAny
v2)
                    ((T_Kind_52 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Kind_52 -> AgdaAny
MAlonzo.Code.Function.Related.du__'8718'_410
                       ((T_Symmetric'45'kind_142 -> T_Kind_52) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Symmetric'45'kind_142 -> T_Kind_52
MAlonzo.Code.Function.Related.d_'8970'_'8971'_148 (T_Symmetric'45'kind_142 -> AgdaAny
forall a b. a -> b
coe T_Symmetric'45'kind_142
v0)))))))
-- Function.Related.TypeIsomorphisms.True↔
d_True'8596'_672 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58
d_True'8596'_672 :: T_Level_18
-> T_Level_18
-> T_Dec_32
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T_Inverse_58
d_True'8596'_672 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 ~AgdaAny -> AgdaAny -> T__'8801'__12
v3 = T_Dec_32 -> T_Inverse_58
du_True'8596'_672 T_Dec_32
v2
du_True'8596'_672 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_True'8596'_672 :: T_Dec_32 -> T_Inverse_58
du_True'8596'_672 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                       (\ AgdaAny
v3 ->
                          (T_Reflects_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_14 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
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)) AgdaAny
forall a. a
erased
                    AgdaAny
forall a. a
erased
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v2)
                    (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156 AgdaAny
forall a. a
erased
                       ((T_Reflects_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Reflects_14 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20
                          (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
                       AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased)
      T_Dec_32
_ -> T_Inverse_58
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Related.TypeIsomorphisms.Σ-≡,≡↔≡
d_Σ'45''8801''44''8801''8596''8801'_700 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58
d_Σ'45''8801''44''8801''8596''8801'_700 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Inverse_58
d_Σ'45''8801''44''8801''8596''8801'_700 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5
  = T_Inverse_58
du_Σ'45''8801''44''8801''8596''8801'_700
du_Σ'45''8801''44''8801''8596''8801'_700 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_Σ'45''8801''44''8801''8596''8801'_700 :: T_Inverse_58
du_Σ'45''8801''44''8801''8596''8801'_700
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156 AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_from_724) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.to
d_to_716 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_to_716 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_to_716 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.from
d_from_724 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_from_724 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T_Σ_14
d_from_724 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5 ~T_Σ_14
v6 ~T_Σ_14
v7 ~T__'8801'__12
v8 = T_Σ_14
du_from_724
du_from_724 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_724 :: T_Σ_14
du_from_724
  = (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
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.left-inverse-of
d_left'45'inverse'45'of_734 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_left'45'inverse'45'of_734 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_left'45'inverse'45'of_734 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.right-inverse-of
d_right'45'inverse'45'of_742 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_right'45'inverse'45'of_742 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_right'45'inverse'45'of_742 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-≡,≡↔≡
d_'215''45''8801''44''8801''8596''8801'_756 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Function.Inverse.T_Inverse_58
d_'215''45''8801''44''8801''8596''8801'_756 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Inverse_58
d_'215''45''8801''44''8801''8596''8801'_756 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5
  = T_Inverse_58
du_'215''45''8801''44''8801''8596''8801'_756
du_'215''45''8801''44''8801''8596''8801'_756 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45''8801''44''8801''8596''8801'_756 :: T_Inverse_58
du_'215''45''8801''44''8801''8596''8801'_756
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156 AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_from_776) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.to
d_to_770 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_to_770 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_to_770 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.from
d_from_776 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_from_776 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T_Σ_14
d_from_776 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5 ~T_Σ_14
v6 ~T_Σ_14
v7 ~T__'8801'__12
v8 = T_Σ_14
du_from_776
du_from_776 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_776 :: T_Σ_14
du_from_776
  = (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
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.left-inverse-of
d_left'45'inverse'45'of_784 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_left'45'inverse'45'of_784 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_left'45'inverse'45'of_784 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.right-inverse-of
d_right'45'inverse'45'of_792 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_right'45'inverse'45'of_792 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_right'45'inverse'45'of_792 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-≡×≡↔≡,≡
d_'215''45''8801''215''8801''8596''8801''44''8801'_808 ::
  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.Function.Inverse.T_Inverse_58
d_'215''45''8801''215''8801''8596''8801''44''8801'_808 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Inverse_58
d_'215''45''8801''215''8801''8596''8801''44''8801'_808 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2
                                                       ~T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~T_Σ_14
v6
  = T_Inverse_58
du_'215''45''8801''215''8801''8596''8801''44''8801'_808
du_'215''45''8801''215''8801''8596''8801''44''8801'_808 ::
  MAlonzo.Code.Function.Inverse.T_Inverse_58
du_'215''45''8801''215''8801''8596''8801''44''8801'_808 :: T_Inverse_58
du_'215''45''8801''215''8801''8596''8801''44''8801'_808
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_58)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_58
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_58
MAlonzo.Code.Function.Inverse.du_inverse_156 AgdaAny
forall a. a
erased
      ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_from_822) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.to
d_to_820 ::
  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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_to_820 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_to_820 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.from
d_from_822 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_from_822 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T__'8801'__12
-> T_Σ_14
d_from_822 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~T_Σ_14
v6 = T__'8801'__12 -> T_Σ_14
du_from_822
du_from_822 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_822 :: T__'8801'__12 -> T_Σ_14
du_from_822
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.du_'60'_'44'_'62'_132 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.from∘to
d_from'8728'to_826 ::
  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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_from'8728'to_826 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_from'8728'to_826 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms._.to∘from
d_to'8728'from_830 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_to'8728'from_830 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_to'8728'from_830 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Function.Related.TypeIsomorphisms.×-CommutativeMonoid
d_'215''45'CommutativeMonoid_832 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
d_'215''45'CommutativeMonoid_832 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_CommutativeMonoid_582
d_'215''45'CommutativeMonoid_832 T_Symmetric'45'kind_142
v0 T_Level_18
v1
  = (T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582)
-> T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582
du_'215''45'commutativeMonoid_284 T_Symmetric'45'kind_142
v0
-- Function.Related.TypeIsomorphisms.⊎-CommutativeMonoid
d_'8846''45'CommutativeMonoid_834 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_582
d_'8846''45'CommutativeMonoid_834 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_CommutativeMonoid_582
d_'8846''45'CommutativeMonoid_834 T_Symmetric'45'kind_142
v0 T_Level_18
v1
  = (T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582)
-> T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_CommutativeMonoid_582
du_'8846''45'commutativeMonoid_366 T_Symmetric'45'kind_142
v0
-- Function.Related.TypeIsomorphisms.×⊎-CommutativeSemiring
d_'215''8846''45'CommutativeSemiring_836 ::
  MAlonzo.Code.Function.Related.T_Symmetric'45'kind_142 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2094
d_'215''8846''45'CommutativeSemiring_836 :: T_Symmetric'45'kind_142 -> T_Level_18 -> T_CommutativeSemiring_2094
d_'215''8846''45'CommutativeSemiring_836 T_Symmetric'45'kind_142
v0 T_Level_18
v1
  = (T_Symmetric'45'kind_142 -> T_CommutativeSemiring_2094)
-> T_Symmetric'45'kind_142 -> T_CommutativeSemiring_2094
forall a b. a -> b
coe T_Symmetric'45'kind_142 -> T_CommutativeSemiring_2094
du_'215''45''8846''45'commutativeSemiring_390 T_Symmetric'45'kind_142
v0