{-# 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.Data.Product.Properties 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.Primitive
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Data.Product.Properties._.,-injectiveˡ
d_'44''45'injective'737'_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'44''45'injective'737'_42 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'44''45'injective'737'_42 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._.,-injectiveʳ-≡
d_'44''45'injective'691''45''8801'_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'44''45'injective'691''45''8801'_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny
    -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12)
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'44''45'injective'691''45''8801'_54 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny
    -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12)
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._.,-injectiveʳ-UIP
d_'44''45'injective'691''45'UIP_70 ::
  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 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'44''45'injective'691''45'UIP_70 :: 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__'8801'__12)
-> T__'8801'__12
-> T__'8801'__12
d_'44''45'injective'691''45'UIP_70 = 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__'8801'__12)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._.≡-dec
d_'8801''45'dec_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8801''45'dec_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T_Σ_14
-> T_Σ_14
-> T_Dec_20
d_'8801''45'dec_78 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4 AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
v5 T_Σ_14
v6 T_Σ_14
v7
  = (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T_Σ_14
-> T_Σ_14
-> T_Dec_20
du_'8801''45'dec_78 AgdaAny -> AgdaAny -> T_Dec_20
v4 AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
v5 T_Σ_14
v6 T_Σ_14
v7
du_'8801''45'dec_78 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8801''45'dec_78 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T_Σ_14
-> T_Σ_14
-> T_Dec_20
du_'8801''45'dec_78 AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
v1 T_Σ_14
v2 T_Σ_14
v3
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
        -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
               -> let v8 :: t
v8 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
                         -> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
                              then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
                                     (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                                        AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v4 AgdaAny
v5 AgdaAny
v7))
                              else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
                                     ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                        (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
                                        (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
                       T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Σ_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Product.Properties.,-injectiveʳ
d_'44''45'injective'691'_132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'44''45'injective'691'_132 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'44''45'injective'691'_132 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties.,-injective
d_'44''45'injective_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'44''45'injective_142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T_Σ_14
d_'44''45'injective_142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~AgdaAny
v6 ~AgdaAny
v7 ~T__'8801'__12
v8
  = T_Σ_14
du_'44''45'injective_142
du_'44''45'injective_142 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'44''45'injective_142 :: T_Σ_14
du_'44''45'injective_142
  = (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
-- Data.Product.Properties.map-cong
d_map'45'cong_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'cong_152 :: 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)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Σ_14
-> T__'8801'__12
d_map'45'cong_152 = 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)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties.swap-involutive
d_swap'45'involutive_162 ::
  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.Equality.T__'8801'__12
d_swap'45'involutive_162 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T__'8801'__12
d_swap'45'involutive_162 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._.Σ-≡,≡→≡
d_Σ'45''8801''44''8801''8594''8801'_190 ::
  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.Equality.T__'8801'__12
d_Σ'45''8801''44''8801''8594''8801'_190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_Σ'45''8801''44''8801''8594''8801'_190 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._.Σ-≡,≡←≡
d_Σ'45''8801''44''8801''8592''8801'_194 ::
  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.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_Σ'45''8801''44''8801''8592''8801'_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T_Σ_14
d_Σ'45''8801''44''8801''8592''8801'_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5 ~T__'8801'__12
v6
  = T_Σ_14
du_Σ'45''8801''44''8801''8592''8801'_194
du_Σ'45''8801''44''8801''8592''8801'_194 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_Σ'45''8801''44''8801''8592''8801'_194 :: T_Σ_14
du_Σ'45''8801''44''8801''8592''8801'_194
  = (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
-- Data.Product.Properties._.left-inverse-of
d_left'45'inverse'45'of_200 ::
  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.Equality.T__'8801'__12
d_left'45'inverse'45'of_200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_left'45'inverse'45'of_200 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._.right-inverse-of
d_right'45'inverse'45'of_204 ::
  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.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_right'45'inverse'45'of_204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_right'45'inverse'45'of_204 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._.Σ-≡,≡↔≡
d_Σ'45''8801''44''8801''8596''8801'_208 ::
  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.Bundles.T_Inverse_1960
d_Σ'45''8801''44''8801''8596''8801'_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Inverse_1960
d_Σ'45''8801''44''8801''8596''8801'_208 ~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_1960
du_Σ'45''8801''44''8801''8596''8801'_208
du_Σ'45''8801''44''8801''8596''8801'_208 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_Σ'45''8801''44''8801''8596''8801'_208 :: T_Inverse_1960
du_Σ'45''8801''44''8801''8596''8801'_208
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366 AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_Σ'45''8801''44''8801''8592''8801'_194)
-- Data.Product.Properties._.×-≡,≡→≡
d_'215''45''8801''44''8801''8594''8801'_230 ::
  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.Equality.T__'8801'__12
d_'215''45''8801''44''8801''8594''8801'_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_'215''45''8801''44''8801''8594''8801'_230 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._.×-≡,≡←≡
d_'215''45''8801''44''8801''8592''8801'_232 ::
  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.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'215''45''8801''44''8801''8592''8801'_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T_Σ_14
d_'215''45''8801''44''8801''8592''8801'_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5
                                            ~T__'8801'__12
v6
  = T_Σ_14
du_'215''45''8801''44''8801''8592''8801'_232
du_'215''45''8801''44''8801''8592''8801'_232 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'215''45''8801''44''8801''8592''8801'_232 :: T_Σ_14
du_'215''45''8801''44''8801''8592''8801'_232
  = (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
-- Data.Product.Properties._.×-≡,≡↔≡
d_'215''45''8801''44''8801''8596''8801'_234 ::
  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.Bundles.T_Inverse_1960
d_'215''45''8801''44''8801''8596''8801'_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Inverse_1960
d_'215''45''8801''44''8801''8596''8801'_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5
  = T_Inverse_1960
du_'215''45''8801''44''8801''8596''8801'_234
du_'215''45''8801''44''8801''8596''8801'_234 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'215''45''8801''44''8801''8596''8801'_234 :: T_Inverse_1960
du_'215''45''8801''44''8801''8596''8801'_234
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366 AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'215''45''8801''44''8801''8592''8801'_232)
-- Data.Product.Properties._..extendedlambda0
d_'46'extendedlambda0_236 ::
  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.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'46'extendedlambda0_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_'46'extendedlambda0_236 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties._..extendedlambda1
d_'46'extendedlambda1_238 ::
  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.Equality.T__'8801'__12
d_'46'extendedlambda1_238 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_'46'extendedlambda1_238 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Properties.∃∃↔∃∃
d_'8707''8707''8596''8707''8707'_250 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'8707''8707''8596''8707''8707'_250 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_1960
d_'8707''8707''8596''8707''8707'_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = T_Inverse_1960
du_'8707''8707''8596''8707''8707'_250
du_'8707''8707''8596''8707''8707'_250 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8707''8707''8596''8707''8707'_250 :: T_Inverse_1960
du_'8707''8707''8596''8707''8707'_250
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_to_266) ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_from_282)
-- Data.Product.Properties._.to
d_to_266 ::
  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_266 :: 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_266 ~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_266 T_Σ_14
v6
du_to_266 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to_266 :: T_Σ_14 -> T_Σ_14
du_to_266 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
-- Data.Product.Properties._.from
d_from_282 ::
  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_282 :: 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_282 ~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_282 T_Σ_14
v6
du_from_282 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_282 :: T_Σ_14 -> T_Σ_14
du_from_282 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