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

-- Data.Product.Properties._.,-injectiveˡ
d_'44''45'injective'737'_34 ::
  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'_34 :: 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'_34 = 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'_46 ::
  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'_46 :: 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'_46 = 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_62 ::
  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_62 :: 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_62 = 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_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8801''45'dec_70 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T_Σ_14
-> T_Σ_14
-> T_Dec_32
d_'8801''45'dec_70 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Dec_32
v4 AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
v5 T_Σ_14
v6 T_Σ_14
v7
  = (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T_Σ_14
-> T_Σ_14
-> T_Dec_32
du_'8801''45'dec_70 AgdaAny -> AgdaAny -> T_Dec_32
v4 AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
v5 T_Σ_14
v6 T_Σ_14
v7
du_'8801''45'dec_70 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8801''45'dec_70 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T_Σ_14
-> T_Σ_14
-> T_Dec_32
du_'8801''45'dec_70 AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
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_32) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    (case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
                       MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v9 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v10)
                                     (((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                                        AgdaAny
forall a. a
erased ((AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v10)
                                     ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
                                        (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
                       T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Σ_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Product.Properties.,-injectiveʳ
d_'44''45'injective'691'_124 ::
  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'_124 :: 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'_124 = 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_134 ::
  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_134 :: 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_134 ~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_134
du_'44''45'injective_134 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'44''45'injective_134 :: T_Σ_14
du_'44''45'injective_134
  = (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.swap-involutive
d_swap'45'involutive_136 ::
  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_136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T__'8801'__12
d_swap'45'involutive_136 = 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''8596''8801'_156 ::
  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_1048
d_Σ'45''8801''44''8801''8596''8801'_156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_Inverse_1048
d_Σ'45''8801''44''8801''8596''8801'_156 ~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_1048
du_Σ'45''8801''44''8801''8596''8801'_156
du_Σ'45''8801''44''8801''8596''8801'_156 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1048
du_Σ'45''8801''44''8801''8596''8801'_156 :: T_Inverse_1048
du_Σ'45''8801''44''8801''8596''8801'_156
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Inverse_1048)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Inverse_1048
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Inverse_1048
MAlonzo.Code.Function.Bundles.du_mk'8596'_1370 AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_from_196)
      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased)
-- Data.Product.Properties._.to
d_to_180 ::
  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_180 :: 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_180 = 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
-- Data.Product.Properties._.from
d_from_196 ::
  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_196 :: 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_196 ~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_196
du_from_196 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_196 :: T_Σ_14
du_from_196
  = (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_214 ::
  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_214 :: 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_214 = 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
-- Data.Product.Properties._.right-inverse-of
d_right'45'inverse'45'of_222 ::
  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_222 :: 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_222 = 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
-- Data.Product.Properties.×-≡,≡↔≡
d_'215''45''8801''44''8801''8596''8801'_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.Function.Bundles.T_Inverse_1048
d_'215''45''8801''44''8801''8596''8801'_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Inverse_1048
d_'215''45''8801''44''8801''8596''8801'_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Σ_14
v4 ~T_Σ_14
v5
  = T_Inverse_1048
du_'215''45''8801''44''8801''8596''8801'_236
du_'215''45''8801''44''8801''8596''8801'_236 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1048
du_'215''45''8801''44''8801''8596''8801'_236 :: T_Inverse_1048
du_'215''45''8801''44''8801''8596''8801'_236
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_1048)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Inverse_1048
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_1048
MAlonzo.Code.Function.Bundles.du_mk'8596''8242'_1382 AgdaAny
forall a. a
erased
      (\ AgdaAny
v0 -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'46'extendedlambda1_240) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Data.Product.Properties..extendedlambda0
d_'46'extendedlambda0_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'extendedlambda0_238 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_'46'extendedlambda0_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..extendedlambda1
d_'46'extendedlambda1_240 ::
  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_'46'extendedlambda1_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T_Σ_14
d_'46'extendedlambda1_240 ~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_'46'extendedlambda1_240
du_'46'extendedlambda1_240 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'46'extendedlambda1_240 :: T_Σ_14
du_'46'extendedlambda1_240
  = (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..extendedlambda2
d_'46'extendedlambda2_242 ::
  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'extendedlambda2_242 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_'46'extendedlambda2_242 = 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..extendedlambda3
d_'46'extendedlambda3_244 ::
  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'extendedlambda3_244 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
d_'46'extendedlambda3_244 = 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'_256 ::
  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_1048
d_'8707''8707''8596''8707''8707'_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Inverse_1048
d_'8707''8707''8596''8707''8707'_256 ~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_1048
du_'8707''8707''8596''8707''8707'_256
du_'8707''8707''8596''8707''8707'_256 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1048
du_'8707''8707''8596''8707''8707'_256 :: T_Inverse_1048
du_'8707''8707''8596''8707''8707'_256
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> T__'8801'__12)
 -> (AgdaAny -> T__'8801'__12)
 -> T_Inverse_1048)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Inverse_1048
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> (AgdaAny -> T__'8801'__12)
-> T_Inverse_1048
MAlonzo.Code.Function.Bundles.du_mk'8596''8242'_1382
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_to_272) ((T_Σ_14 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
du_from_288) AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Data.Product.Properties._.to
d_to_272 ::
  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_272 :: 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_272 ~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_272 T_Σ_14
v6
du_to_272 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to_272 :: T_Σ_14 -> T_Σ_14
du_to_272 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_288 ::
  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_288 :: 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_288 ~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_288 T_Σ_14
v6
du_from_288 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from_288 :: T_Σ_14 -> T_Σ_14
du_from_288 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