{-# 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.Sum.Function.Propositional 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.Primitive
import qualified MAlonzo.Code.Data.Sum.Function.Setoid
import qualified MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Construct.Composition
import qualified MAlonzo.Code.Function.Construct.Symmetry
import qualified MAlonzo.Code.Function.Properties.Inverse
import qualified MAlonzo.Code.Function.Related.Propositional
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties

-- Data.Sum.Function.Propositional.liftViaInverse
d_liftViaInverse_64 ::
  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.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.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> ()) ->
  (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.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   AgdaAny -> AgdaAny -> AgdaAny) ->
  (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.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_liftViaInverse_64 :: 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_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Level_18)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Setoid_44
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_liftViaInverse_64 ~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_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Level_18
v8 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
v9 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny
v11
                    AgdaAny
v12 AgdaAny
v13
  = (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
v9 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 AgdaAny
v13
du_liftViaInverse_64 ::
  (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.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   AgdaAny -> AgdaAny -> AgdaAny) ->
  (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.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
   MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_liftViaInverse_64 :: (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
v0 T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
  = (T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Setoid_44
     -> AgdaAny
     -> AgdaAny
     -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> T_Inverse_1960
 -> AgdaAny
 -> T_Inverse_1960
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Setoid_44
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> T_Inverse_1960
-> AgdaAny
-> T_Inverse_1960
-> AgdaAny
MAlonzo.Code.Function.Properties.Inverse.du_transportVia_694
      (T_Level_18 -> AgdaAny
forall a b. a -> b
coe ()) (T_Level_18 -> AgdaAny
forall a b. a -> b
coe ())
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Level_18 -> AgdaAny
forall a b. a -> b
coe ()) (T_Level_18 -> AgdaAny
forall a b. a -> b
coe ())
      ((T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du__'8846''8347'__432
         (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
         (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402))
      (T_Level_18 -> AgdaAny
forall a b. a -> b
coe ()) (T_Level_18 -> AgdaAny
forall a b. a -> b
coe ())
      ((T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du__'8846''8347'__432
         (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
         (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402))
      (T_Level_18 -> AgdaAny
forall a b. a -> b
coe ()) (T_Level_18 -> AgdaAny
forall a b. a -> b
coe ())
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      ((T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
v0) ((T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Inverse_1960
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> AgdaAny
v1)
      ((T_Inverse_1960 -> T_Inverse_1960) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Symmetry.du_inverse_1052
         (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
            T_Inverse_1960
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_446))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4)
      (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
         T_Inverse_1960
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise.du_Pointwise'45''8801''8596''8801'_446)
-- Data.Sum.Function.Propositional._⊎-⟶_
d__'8846''45''10230'__76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d__'8846''45''10230'__76 :: 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_Func_714
-> T_Func_714
-> T_Func_714
d__'8846''45''10230'__76 ~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_Func_714 -> T_Func_714 -> T_Func_714
du__'8846''45''10230'__76
du__'8846''45''10230'__76 ::
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du__'8846''45''10230'__76 :: T_Func_714 -> T_Func_714 -> T_Func_714
du__'8846''45''10230'__76
  = ((T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Setoid_44
  -> T_Setoid_44
  -> T_Setoid_44
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Func_714
-> T_Func_714
-> T_Func_714
forall a b. a -> b
coe
      (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
            (T_Func_714 -> T_Func_714 -> T_Func_714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Func_714 -> T_Func_714 -> T_Func_714
MAlonzo.Code.Function.Construct.Composition.du_function_1204 AgdaAny
v9
              AgdaAny
v10))
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_Inverse_1960 -> T_Func_714) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T_Func_714
MAlonzo.Code.Function.Properties.Inverse.du_toFunction_44 AgdaAny
v6))
      ((T_Func_714 -> T_Func_714 -> T_Func_714) -> AgdaAny
forall a b. a -> b
coe
         T_Func_714 -> T_Func_714 -> T_Func_714
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'function__132)
-- Data.Sum.Function.Propositional._⊎-⇔_
d__'8846''45''8660'__78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d__'8846''45''8660'__78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1714
-> T_Equivalence_1714
-> T_Equivalence_1714
d__'8846''45''8660'__78 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7
  = T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du__'8846''45''8660'__78
du__'8846''45''8660'__78 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du__'8846''45''8660'__78 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du__'8846''45''8660'__78
  = ((T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Setoid_44
  -> T_Setoid_44
  -> T_Setoid_44
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Equivalence_1714
-> T_Equivalence_1714
-> T_Equivalence_1714
forall a b. a -> b
coe
      (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
            (T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
MAlonzo.Code.Function.Construct.Composition.du_equivalence_1764 AgdaAny
v9
              AgdaAny
v10))
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_Inverse_1960 -> T_Equivalence_1714) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_1960 -> T_Equivalence_1714
MAlonzo.Code.Function.Properties.Inverse.du_Inverse'8658'Equivalence_552
              AgdaAny
v6))
      ((T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714)
-> AgdaAny
forall a b. a -> b
coe
         T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'equivalence__142)
-- Data.Sum.Function.Propositional._⊎-↣_
d__'8846''45''8611'__80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
d__'8846''45''8611'__80 :: 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_Injection_776
-> T_Injection_776
-> T_Injection_776
d__'8846''45''8611'__80 ~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_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8846''45''8611'__80
du__'8846''45''8611'__80 ::
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
du__'8846''45''8611'__80 :: T_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8846''45''8611'__80
  = ((T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Setoid_44
  -> T_Setoid_44
  -> T_Setoid_44
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Injection_776
-> T_Injection_776
-> T_Injection_776
forall a b. a -> b
coe
      (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
            (T_Injection_776 -> T_Injection_776 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Injection_776 -> T_Injection_776 -> T_Injection_776
MAlonzo.Code.Function.Construct.Composition.du_injection_1326 AgdaAny
v9
              AgdaAny
v10))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Injection_776)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Injection_776
MAlonzo.Code.Function.Properties.Inverse.du_Inverse'8658'Injection_216
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)))
      ((T_Injection_776 -> T_Injection_776 -> T_Injection_776) -> AgdaAny
forall a b. a -> b
coe
         T_Injection_776 -> T_Injection_776 -> T_Injection_776
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'injection__152)
-- Data.Sum.Function.Propositional._⊎-↠_
d__'8846''45''8608'__82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d__'8846''45''8608'__82 :: 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_Surjection_846
-> T_Surjection_846
-> T_Surjection_846
d__'8846''45''8608'__82 ~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_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du__'8846''45''8608'__82
du__'8846''45''8608'__82 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du__'8846''45''8608'__82 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du__'8846''45''8608'__82
  = ((T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Setoid_44
  -> T_Setoid_44
  -> T_Setoid_44
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Surjection_846
-> T_Surjection_846
-> T_Surjection_846
forall a b. a -> b
coe
      (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
            (T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
MAlonzo.Code.Function.Construct.Composition.du_surjection_1460 AgdaAny
v9
              AgdaAny
v10))
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_Inverse_1960 -> T_Surjection_846) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_1960 -> T_Surjection_846
MAlonzo.Code.Function.Properties.Inverse.du_Inverse'8658'Surjection_328
              AgdaAny
v6))
      ((T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846)
-> AgdaAny
forall a b. a -> b
coe
         T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'surjection__162)
-- Data.Sum.Function.Propositional._⊎-↩_
d__'8846''45''8617'__84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d__'8846''45''8617'__84 :: 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_LeftInverse_1792
-> T_LeftInverse_1792
-> T_LeftInverse_1792
d__'8846''45''8617'__84 ~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_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du__'8846''45''8617'__84
du__'8846''45''8617'__84 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du__'8846''45''8617'__84 :: T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
du__'8846''45''8617'__84
  = ((T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Setoid_44
  -> T_Setoid_44
  -> T_Setoid_44
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1792
-> T_LeftInverse_1792
-> T_LeftInverse_1792
forall a b. a -> b
coe
      (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
            (T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
MAlonzo.Code.Function.Construct.Composition.du_leftInverse_1906 AgdaAny
v9
              AgdaAny
v10))
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_Inverse_1960 -> T_LeftInverse_1792) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T_LeftInverse_1792
MAlonzo.Code.Function.Bundles.du_leftInverse_1986 AgdaAny
v6))
      ((T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792)
-> AgdaAny
forall a b. a -> b
coe
         T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'leftInverse__182)
-- Data.Sum.Function.Propositional._⊎-↪_
d__'8846''45''8618'__86 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d__'8846''45''8618'__86 :: 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_RightInverse_1880
-> T_RightInverse_1880
-> T_RightInverse_1880
d__'8846''45''8618'__86 ~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_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du__'8846''45''8618'__86
du__'8846''45''8618'__86 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du__'8846''45''8618'__86 :: T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du__'8846''45''8618'__86
  = ((T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Setoid_44
  -> T_Setoid_44
  -> T_Setoid_44
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_1880
-> T_RightInverse_1880
-> T_RightInverse_1880
forall a b. a -> b
coe
      (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
            (T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
MAlonzo.Code.Function.Construct.Composition.du_rightInverse_2064 AgdaAny
v9
              AgdaAny
v10))
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
            (T_Inverse_1960 -> T_RightInverse_1880) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.du_rightInverse_1988 AgdaAny
v6))
      ((T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880)
-> AgdaAny
forall a b. a -> b
coe
         T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'rightInverse__198)
-- Data.Sum.Function.Propositional._⊎-⤖_
d__'8846''45''10518'__88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d__'8846''45''10518'__88 :: 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_Bijection_926
-> T_Bijection_926
-> T_Bijection_926
d__'8846''45''10518'__88 ~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_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du__'8846''45''10518'__88
du__'8846''45''10518'__88 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du__'8846''45''10518'__88 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
du__'8846''45''10518'__88
  = ((T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Setoid_44
  -> T_Setoid_44
  -> T_Setoid_44
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Bijection_926
-> T_Bijection_926
-> T_Bijection_926
forall a b. a -> b
coe
      (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
            (T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
MAlonzo.Code.Function.Construct.Composition.du_bijection_1606 AgdaAny
v9
              AgdaAny
v10))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Bijection_926)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Bijection_926
MAlonzo.Code.Function.Properties.Inverse.du_Inverse'8658'Bijection_440
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)))
      ((T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926) -> AgdaAny
forall a b. a -> b
coe
         T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'bijection__172)
-- Data.Sum.Function.Propositional._⊎-↔_
d__'8846''45''8596'__90 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d__'8846''45''8596'__90 :: 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_Inverse_1960
-> T_Inverse_1960
-> T_Inverse_1960
d__'8846''45''8596'__90 ~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_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du__'8846''45''8596'__90
du__'8846''45''8596'__90 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du__'8846''45''8596'__90 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du__'8846''45''8596'__90
  = ((T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Level_18
  -> T_Setoid_44
  -> T_Setoid_44
  -> T_Setoid_44
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Level_18
     -> T_Setoid_44
     -> T_Setoid_44
     -> T_Inverse_1960
     -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Inverse_1960
-> T_Inverse_1960
-> T_Inverse_1960
forall a b. a -> b
coe
      (T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Level_18
 -> T_Setoid_44
 -> T_Setoid_44
 -> T_Setoid_44
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Level_18
    -> T_Setoid_44
    -> T_Setoid_44
    -> T_Inverse_1960
    -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_liftViaInverse_64
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 ->
            (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Construct.Composition.du_inverse_2210 AgdaAny
v9
              AgdaAny
v10))
      ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 -> AgdaAny
v6))
      ((T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960) -> AgdaAny
forall a b. a -> b
coe
         T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Data.Sum.Function.Setoid.du__'8846''45'inverse__214)
-- Data.Sum.Function.Propositional._⊎-cong_
d__'8846''45'cong__94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
  AgdaAny -> AgdaAny -> AgdaAny
d__'8846''45'cong__94 :: 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_Kind_6
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8846''45'cong__94 ~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_Kind_6
v8
  = T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8846''45'cong__94 T_Kind_6
v8
du__'8846''45'cong__94 ::
  MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
  AgdaAny -> AgdaAny -> AgdaAny
du__'8846''45'cong__94 :: T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
du__'8846''45'cong__94 T_Kind_6
v0
  = case T_Kind_6 -> T_Kind_6
forall a b. a -> b
coe T_Kind_6
v0 of
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_implication_8
        -> (T_Func_714 -> T_Func_714 -> T_Func_714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> T_Func_714 -> T_Func_714
du__'8846''45''10230'__76
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
        -> (T_Func_714 -> T_Func_714 -> T_Func_714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> T_Func_714 -> T_Func_714
du__'8846''45''10230'__76
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
        -> (T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714
du__'8846''45''8660'__78
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_injection_14
        -> (T_Injection_776 -> T_Injection_776 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8846''45''8611'__80
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
        -> (T_Injection_776 -> T_Injection_776 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_776 -> T_Injection_776 -> T_Injection_776
du__'8846''45''8611'__80
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
        -> (T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880
du__'8846''45''8618'__86
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
        -> (T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846
du__'8846''45''8608'__82
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
        -> (T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960
du__'8846''45''8596'__90
      T_Kind_6
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError