{-# 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.Function.Dependent.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.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Properties.Inverse
import qualified MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence
import qualified MAlonzo.Code.Function.Properties.RightInverse
import qualified MAlonzo.Code.Function.Related.Propositional
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax

-- Data.Product.Function.Dependent.Propositional._.Σ-⟶
d_Σ'45''10230'_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Func_714) ->
  MAlonzo.Code.Function.Bundles.T_Func_714
d_Σ'45''10230'_36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Func_714
-> (AgdaAny -> T_Func_714)
-> T_Func_714
d_Σ'45''10230'_36 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Func_714
v8 AgdaAny -> T_Func_714
v9
  = T_Func_714 -> (AgdaAny -> T_Func_714) -> T_Func_714
du_Σ'45''10230'_36 T_Func_714
v8 AgdaAny -> T_Func_714
v9
du_Σ'45''10230'_36 ::
  MAlonzo.Code.Function.Bundles.T_Func_714 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Func_714) ->
  MAlonzo.Code.Function.Bundles.T_Func_714
du_Σ'45''10230'_36 :: T_Func_714 -> (AgdaAny -> T_Func_714) -> T_Func_714
du_Σ'45''10230'_36 T_Func_714
v0 AgdaAny -> T_Func_714
v1
  = ((AgdaAny -> AgdaAny) -> T_Func_714) -> AgdaAny -> T_Func_714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> T_Func_714
MAlonzo.Code.Function.Bundles.du_mk'10230'_2266
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
         ((T_Func_714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Func_714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_720 (T_Func_714 -> AgdaAny
forall a b. a -> b
coe T_Func_714
v0))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> T_Func_714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_720 ((AgdaAny -> T_Func_714) -> AgdaAny -> T_Func_714
forall a b. a -> b
coe AgdaAny -> T_Func_714
v1 AgdaAny
v2))))
-- Data.Product.Function.Dependent.Propositional._.Σ-⇔
d_Σ'45''8660'_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_Σ'45''8660'_50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Surjection_846
-> (AgdaAny -> T_Equivalence_1714)
-> T_Equivalence_1714
d_Σ'45''8660'_50 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_846
v8 AgdaAny -> T_Equivalence_1714
v9
  = T_Surjection_846
-> (AgdaAny -> T_Equivalence_1714) -> T_Equivalence_1714
du_Σ'45''8660'_50 T_Surjection_846
v8 AgdaAny -> T_Equivalence_1714
v9
du_Σ'45''8660'_50 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_Σ'45''8660'_50 :: T_Surjection_846
-> (AgdaAny -> T_Equivalence_1714) -> T_Equivalence_1714
du_Σ'45''8660'_50 T_Surjection_846
v0 AgdaAny -> T_Equivalence_1714
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
         ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 ((AgdaAny -> T_Equivalence_1714) -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe AgdaAny -> T_Equivalence_1714
v1 AgdaAny
v2))))
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
         ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 AgdaAny
v3 ->
               (T_Equivalence_1714 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726
                 ((AgdaAny -> T_Equivalence_1714) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> T_Equivalence_1714
v1
                    (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                       ((T_Surjection_846 -> AgdaAny -> T_Σ_14)
-> T_Surjection_846 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_surjective_858 T_Surjection_846
v0 AgdaAny
v2)))
                 AgdaAny
v3)))
-- Data.Product.Function.Dependent.Propositional._.Σ-↣
d_Σ'45''8611'_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
d_Σ'45''8611'_66 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> T_Injection_776
d_Σ'45''8611'_66 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 AgdaAny -> T_Injection_776
v9
  = T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Injection_776
du_Σ'45''8611'_66 T_Inverse_1960
v8 AgdaAny -> T_Injection_776
v9
du_Σ'45''8611'_66 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  MAlonzo.Code.Function.Bundles.T_Injection_776
du_Σ'45''8611'_66 :: T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Injection_776
du_Σ'45''8611'_66 T_Inverse_1960
v0 AgdaAny -> T_Injection_776
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
 -> T_Injection_776)
-> AgdaAny -> AgdaAny -> T_Injection_776
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> T_Injection_776
MAlonzo.Code.Function.Bundles.du_mk'8611'_2272
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (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__'8771'__24 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T__'8771'__24 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.d_to_46
                 ((T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
                 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2)))
              ((T_Injection_776 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Injection_776 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_784
                 ((AgdaAny -> T_Injection_776) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Injection_776
v1 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2)))
                 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2)))))
      AgdaAny
forall a. a
erased
-- Data.Product.Function.Dependent.Propositional._._.I≃J
d_I'8771'J_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.T__'8771'__24
d_I'8771'J_84 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> T__'8771'__24
d_I'8771'J_84 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 ~AgdaAny -> T_Injection_776
v9
  = T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 T_Inverse_1960
v8
du_I'8771'J_84 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.T__'8771'__24
du_I'8771'J_84 :: T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 T_Inverse_1960
v0
  = (T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> T__'8771'__24
forall a b. a -> b
coe
      T_Inverse_1960 -> T__'8771'__24
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.du_'8596''8658''8771'_100
      (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0)
-- Data.Product.Function.Dependent.Propositional._._._.from
d_from_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  AgdaAny -> AgdaAny
d_from_88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
d_from_88 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 ~AgdaAny -> T_Injection_776
v9 = T_Inverse_1960 -> AgdaAny -> AgdaAny
du_from_88 T_Inverse_1960
v8
du_from_88 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny -> AgdaAny
du_from_88 :: T_Inverse_1960 -> AgdaAny -> AgdaAny
du_from_88 T_Inverse_1960
v0
  = (T__'8771'__24 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__'8771'__24 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.d_from_48
      ((T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
-- Data.Product.Function.Dependent.Propositional._._._.to
d_to_98 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  AgdaAny -> AgdaAny
d_to_98 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
d_to_98 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 ~AgdaAny -> T_Injection_776
v9 = T_Inverse_1960 -> AgdaAny -> AgdaAny
du_to_98 T_Inverse_1960
v8
du_to_98 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny -> AgdaAny
du_to_98 :: T_Inverse_1960 -> AgdaAny -> AgdaAny
du_to_98 T_Inverse_1960
v0
  = (T__'8771'__24 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__'8771'__24 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.d_to_46
      ((T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
-- Data.Product.Function.Dependent.Propositional._._.subst-application′
d_subst'45'application'8242'_112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'application'8242'_112 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_subst'45'application'8242'_112 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Function.Dependent.Propositional._._._._.from
d_from_130 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> AgdaAny
d_from_130 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d_from_130 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 ~AgdaAny -> T_Injection_776
v9 ~AgdaAny
v10 ~AgdaAny
v11 ~AgdaAny
v12
           ~AgdaAny -> AgdaAny -> AgdaAny
v13 ~T__'8801'__12
v14
  = T_Inverse_1960 -> AgdaAny -> AgdaAny
du_from_130 T_Inverse_1960
v8
du_from_130 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny -> AgdaAny
du_from_130 :: T_Inverse_1960 -> AgdaAny -> AgdaAny
du_from_130 T_Inverse_1960
v0
  = (T__'8771'__24 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__'8771'__24 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.d_from_48
      ((T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
-- Data.Product.Function.Dependent.Propositional._._._._.to
d_to_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> AgdaAny
d_to_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d_to_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 ~AgdaAny -> T_Injection_776
v9 ~AgdaAny
v10 ~AgdaAny
v11 ~AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny
v13
         ~T__'8801'__12
v14
  = T_Inverse_1960 -> AgdaAny -> AgdaAny
du_to_140 T_Inverse_1960
v8
du_to_140 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 -> AgdaAny -> AgdaAny
du_to_140 :: T_Inverse_1960 -> AgdaAny -> AgdaAny
du_to_140 T_Inverse_1960
v0
  = (T__'8771'__24 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__'8771'__24 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.d_to_46
      ((T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
-- Data.Product.Function.Dependent.Propositional._._._.g′
d_g'8242'_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_g'8242'_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_g'8242'_144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 ~AgdaAny -> T_Injection_776
v9 ~AgdaAny
v10 ~AgdaAny
v11 ~AgdaAny
v12
              AgdaAny -> AgdaAny -> AgdaAny
v13 ~T__'8801'__12
v14 AgdaAny
v15 AgdaAny
v16
  = T_Inverse_1960
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_g'8242'_144 T_Inverse_1960
v8 AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v15 AgdaAny
v16
du_g'8242'_144 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_g'8242'_144 :: T_Inverse_1960
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_g'8242'_144 T_Inverse_1960
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny
v1
      ((T__'8771'__24 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T__'8771'__24 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.d_from_48
         ((T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0)) AgdaAny
v2)
      AgdaAny
v3
-- Data.Product.Function.Dependent.Propositional._._._.g′-lemma
d_g'8242''45'lemma_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_g'8242''45'lemma_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
d_g'8242''45'lemma_152 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Function.Dependent.Propositional._._._._.lemma
d_lemma_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemma_168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_lemma_168 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Function.Dependent.Propositional._._.to′
d_to'8242'_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to'8242'_172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> T_Σ_14
-> T_Σ_14
d_to'8242'_172 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 AgdaAny -> T_Injection_776
v9
  = T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Σ_14 -> T_Σ_14
du_to'8242'_172 T_Inverse_1960
v8 AgdaAny -> T_Injection_776
v9
du_to'8242'_172 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to'8242'_172 :: T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Σ_14 -> T_Σ_14
du_to'8242'_172 T_Inverse_1960
v0 AgdaAny -> T_Injection_776
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
      ((T__'8771'__24 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T__'8771'__24 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.d_to_46
         ((T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_84 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> T_Injection_776 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_784 ((AgdaAny -> T_Injection_776) -> AgdaAny -> T_Injection_776
forall a b. a -> b
coe AgdaAny -> T_Injection_776
v1 AgdaAny
v2)))
-- Data.Product.Function.Dependent.Propositional._._.to-injective
d_to'45'injective_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Injection_776) ->
  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_to'45'injective_174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_to'45'injective_174 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Injection_776)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Function.Dependent.Propositional._.Σ-↠
d_Σ'45''8608'_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_Σ'45''8608'_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Surjection_846
-> (AgdaAny -> T_Surjection_846)
-> T_Surjection_846
d_Σ'45''8608'_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_846
v8 AgdaAny -> T_Surjection_846
v9
  = T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Surjection_846
du_Σ'45''8608'_210 T_Surjection_846
v8 AgdaAny -> T_Surjection_846
v9
du_Σ'45''8608'_210 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_Σ'45''8608'_210 :: T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Surjection_846
du_Σ'45''8608'_210 T_Surjection_846
v0 AgdaAny -> T_Surjection_846
v1
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> T_Surjection_846
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_846
MAlonzo.Code.Function.Bundles.du_mk'8608''8347'_2360
      ((T_Surjection_846
 -> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_to'8242'_228 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0) ((AgdaAny -> T_Surjection_846) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Surjection_846
v1))
      ((T_Surjection_846
 -> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_strictlySurjective'8242'_236 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0) ((AgdaAny -> T_Surjection_846) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Surjection_846
v1))
-- Data.Product.Function.Dependent.Propositional._._.to′
d_to'8242'_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to'8242'_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Surjection_846
-> (AgdaAny -> T_Surjection_846)
-> T_Σ_14
-> T_Σ_14
d_to'8242'_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_846
v8 AgdaAny -> T_Surjection_846
v9
  = T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_to'8242'_228 T_Surjection_846
v8 AgdaAny -> T_Surjection_846
v9
du_to'8242'_228 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to'8242'_228 :: T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_to'8242'_228 T_Surjection_846
v0 AgdaAny -> T_Surjection_846
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
      ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854 ((AgdaAny -> T_Surjection_846) -> AgdaAny -> T_Surjection_846
forall a b. a -> b
coe AgdaAny -> T_Surjection_846
v1 AgdaAny
v2)))
-- Data.Product.Function.Dependent.Propositional._._.backcast
d_backcast_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_backcast_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Surjection_846
-> (AgdaAny -> T_Surjection_846)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_backcast_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 ~T_Surjection_846
v8 ~AgdaAny -> T_Surjection_846
v9 ~AgdaAny
v10 AgdaAny
v11
  = AgdaAny -> AgdaAny
du_backcast_232 AgdaAny
v11
du_backcast_232 :: AgdaAny -> AgdaAny
du_backcast_232 :: AgdaAny -> AgdaAny
du_backcast_232 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Data.Product.Function.Dependent.Propositional._._.to⁻′
d_to'8315''8242'_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to'8315''8242'_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Surjection_846
-> (AgdaAny -> T_Surjection_846)
-> T_Σ_14
-> T_Σ_14
d_to'8315''8242'_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_846
v8 AgdaAny -> T_Surjection_846
v9
  = T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_to'8315''8242'_234 T_Surjection_846
v8 AgdaAny -> T_Surjection_846
v9
du_to'8315''8242'_234 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to'8315''8242'_234 :: T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_to'8315''8242'_234 T_Surjection_846
v0 AgdaAny -> T_Surjection_846
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
      ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920
              ((AgdaAny -> T_Surjection_846) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny -> T_Surjection_846
v1
                 ((T_Surjection_846 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920 (T_Surjection_846 -> AgdaAny
forall a b. a -> b
coe T_Surjection_846
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)))
-- Data.Product.Function.Dependent.Propositional._._.strictlySurjective′
d_strictlySurjective'8242'_236 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_strictlySurjective'8242'_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Surjection_846
-> (AgdaAny -> T_Surjection_846)
-> T_Σ_14
-> T_Σ_14
d_strictlySurjective'8242'_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Surjection_846
v8
                               AgdaAny -> T_Surjection_846
v9 T_Σ_14
v10
  = T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_strictlySurjective'8242'_236 T_Surjection_846
v8 AgdaAny -> T_Surjection_846
v9 T_Σ_14
v10
du_strictlySurjective'8242'_236 ::
  MAlonzo.Code.Function.Bundles.T_Surjection_846 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Surjection_846) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_strictlySurjective'8242'_236 :: T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_strictlySurjective'8242'_236 T_Surjection_846
v0 AgdaAny -> T_Surjection_846
v1 T_Σ_14
v2
  = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v2)
      ((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_Surjection_846
 -> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14)
-> T_Surjection_846
-> (AgdaAny -> T_Surjection_846)
-> T_Σ_14
-> AgdaAny
forall a b. a -> b
coe T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Σ_14 -> T_Σ_14
du_to'8315''8242'_234 T_Surjection_846
v0 AgdaAny -> T_Surjection_846
v1 T_Σ_14
v2) AgdaAny
forall a. a
erased)
-- Data.Product.Function.Dependent.Propositional._.Σ-↩
d_Σ'45''8617'_254 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792) ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_Σ'45''8617'_254 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792)
-> T_LeftInverse_1792
d_Σ'45''8617'_254 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_LeftInverse_1792
v8 AgdaAny -> T_LeftInverse_1792
v9
  = T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_LeftInverse_1792
du_Σ'45''8617'_254 T_LeftInverse_1792
v8 AgdaAny -> T_LeftInverse_1792
v9
du_Σ'45''8617'_254 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792) ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_Σ'45''8617'_254 :: T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_LeftInverse_1792
du_Σ'45''8617'_254 T_LeftInverse_1792
v0 AgdaAny -> T_LeftInverse_1792
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
 -> T_LeftInverse_1792)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_LeftInverse_1792
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> T_LeftInverse_1792
MAlonzo.Code.Function.Bundles.du_mk'8617'_2308
      ((T_LeftInverse_1792
 -> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14
du_to'8242'_272 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0) ((AgdaAny -> T_LeftInverse_1792) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_LeftInverse_1792
v1))
      ((T_LeftInverse_1792
 -> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14
du_from'8242'_278 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0) ((AgdaAny -> T_LeftInverse_1792) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_LeftInverse_1792
v1)) AgdaAny
forall a. a
erased
-- Data.Product.Function.Dependent.Propositional._._.to′
d_to'8242'_272 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_to'8242'_272 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792)
-> T_Σ_14
-> T_Σ_14
d_to'8242'_272 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_LeftInverse_1792
v8 AgdaAny -> T_LeftInverse_1792
v9
  = T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14
du_to'8242'_272 T_LeftInverse_1792
v8 AgdaAny -> T_LeftInverse_1792
v9
du_to'8242'_272 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_to'8242'_272 :: T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14
du_to'8242'_272 T_LeftInverse_1792
v0 AgdaAny -> T_LeftInverse_1792
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1804 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1804 ((AgdaAny -> T_LeftInverse_1792) -> AgdaAny -> T_LeftInverse_1792
forall a b. a -> b
coe AgdaAny -> T_LeftInverse_1792
v1 AgdaAny
v2)))
-- Data.Product.Function.Dependent.Propositional._._.backcast
d_backcast_276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_backcast_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_backcast_276 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 ~T_LeftInverse_1792
v8 ~AgdaAny -> T_LeftInverse_1792
v9 ~AgdaAny
v10 AgdaAny
v11
  = AgdaAny -> AgdaAny
du_backcast_276 AgdaAny
v11
du_backcast_276 :: AgdaAny -> AgdaAny
du_backcast_276 :: AgdaAny -> AgdaAny
du_backcast_276 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Data.Product.Function.Dependent.Propositional._._.from′
d_from'8242'_278 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_from'8242'_278 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792)
-> T_Σ_14
-> T_Σ_14
d_from'8242'_278 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_LeftInverse_1792
v8 AgdaAny -> T_LeftInverse_1792
v9
  = T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14
du_from'8242'_278 T_LeftInverse_1792
v8 AgdaAny -> T_LeftInverse_1792
v9
du_from'8242'_278 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_from'8242'_278 :: T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_Σ_14 -> T_Σ_14
du_from'8242'_278 T_LeftInverse_1792
v0 AgdaAny -> T_LeftInverse_1792
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1806 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            (T_LeftInverse_1792 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1806
              ((AgdaAny -> T_LeftInverse_1792) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_LeftInverse_1792
v1 ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1806 T_LeftInverse_1792
v0 AgdaAny
v2)) AgdaAny
v3))
-- Data.Product.Function.Dependent.Propositional._._.inv
d_inv_280 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_LeftInverse_1792) ->
  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_inv_280 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
d_inv_280 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792)
-> T_Σ_14
-> T_Σ_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Function.Dependent.Propositional._.Σ-↔
d_Σ'45''8596'_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_Σ'45''8596'_298 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Inverse_1960)
-> T_Inverse_1960
d_Σ'45''8596'_298 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 AgdaAny -> T_Inverse_1960
v9
  = T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Inverse_1960
du_Σ'45''8596'_298 T_Inverse_1960
v8 AgdaAny -> T_Inverse_1960
v9
du_Σ'45''8596'_298 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_Σ'45''8596'_298 :: T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Inverse_1960
du_Σ'45''8596'_298 T_Inverse_1960
v0 AgdaAny -> T_Inverse_1960
v1
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_854
         ((T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Surjection_846
du_surjection'8242'_318 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0) ((AgdaAny -> T_Inverse_1960) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Inverse_1960
v1)))
      ((T_Surjection_846 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Surjection_846 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.du_to'8315'_920
         ((T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Surjection_846
du_surjection'8242'_318 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0) ((AgdaAny -> T_Inverse_1960) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Inverse_1960
v1)))
-- Data.Product.Function.Dependent.Propositional._._.I≃J
d_I'8771'J_316 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960) ->
  MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.T__'8771'__24
d_I'8771'J_316 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Inverse_1960)
-> T__'8771'__24
d_I'8771'J_316 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 ~AgdaAny -> T_Inverse_1960
v9
  = T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_316 T_Inverse_1960
v8
du_I'8771'J_316 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.T__'8771'__24
du_I'8771'J_316 :: T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_316 T_Inverse_1960
v0
  = (T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> T__'8771'__24
forall a b. a -> b
coe
      T_Inverse_1960 -> T__'8771'__24
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.du_'8596''8658''8771'_100
      (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0)
-- Data.Product.Function.Dependent.Propositional._._.surjection′
d_surjection'8242'_318 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
d_surjection'8242'_318 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Inverse_1960)
-> T_Surjection_846
d_surjection'8242'_318 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Inverse_1960
v8 AgdaAny -> T_Inverse_1960
v9
  = T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Surjection_846
du_surjection'8242'_318 T_Inverse_1960
v8 AgdaAny -> T_Inverse_1960
v9
du_surjection'8242'_318 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960) ->
  MAlonzo.Code.Function.Bundles.T_Surjection_846
du_surjection'8242'_318 :: T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Surjection_846
du_surjection'8242'_318 T_Inverse_1960
v0 AgdaAny -> T_Inverse_1960
v1
  = (T_Surjection_846
 -> (AgdaAny -> T_Surjection_846) -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> T_Surjection_846
forall a b. a -> b
coe
      T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Surjection_846
du_Σ'45''8608'_210
      ((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_'8596''8658''8608'_644
         ((T__'8771'__24 -> T_Inverse_1960) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T__'8771'__24 -> T_Inverse_1960
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence.du_'8771''8658''8596'_78
            ((T_Inverse_1960 -> T__'8771'__24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T__'8771'__24
du_I'8771'J_316 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (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_'8596''8658''8608'_644
              ((AgdaAny -> T_Inverse_1960) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Inverse_1960
v1 AgdaAny
v2)))
-- Data.Product.Function.Dependent.Propositional._._.left-inverse-of
d_left'45'inverse'45'of_322 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Inverse_1960) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_left'45'inverse'45'of_322 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Inverse_1960)
-> T_Σ_14
-> T__'8801'__12
d_left'45'inverse'45'of_322 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> T_Inverse_1960)
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.Product.Function.Dependent.Propositional._.swap-coercions
d_swap'45'coercions_346 ::
  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 -> ()) ->
  MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_swap'45'coercions_346 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Kind_6
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_swap'45'coercions_346 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> T_Level_18
v6 T_Kind_6
v7 AgdaAny -> T_Level_18
v8 T_Inverse_1960
v9 AgdaAny -> AgdaAny
v10 AgdaAny
v11
  = (AgdaAny -> T_Level_18)
-> T_Kind_6
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_swap'45'coercions_346 AgdaAny -> T_Level_18
v6 T_Kind_6
v7 AgdaAny -> T_Level_18
v8 T_Inverse_1960
v9 AgdaAny -> AgdaAny
v10 AgdaAny
v11
du_swap'45'coercions_346 ::
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_swap'45'coercions_346 :: (AgdaAny -> T_Level_18)
-> T_Kind_6
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_swap'45'coercions_346 AgdaAny -> T_Level_18
v0 T_Kind_6
v1 AgdaAny -> T_Level_18
v2 T_Inverse_1960
v3 AgdaAny -> AgdaAny
v4 AgdaAny
v5
  = ((AgdaAny -> AgdaAny -> AgdaAny -> 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
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8764'_300
      (\ AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 ->
         (T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'trans_164
           (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v1))
      ((AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Level_18
v0 ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v3 AgdaAny
v5))
      ((AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T_Level_18
v2
         ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 T_Inverse_1960
v3
            ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v3 AgdaAny
v5)))
      ((AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Level_18
v2 AgdaAny
v5)
      (((AgdaAny -> AgdaAny -> AgdaAny -> 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
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8596''45''10217'_410
         (\ AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 ->
            ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
              ((T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'trans_164
                 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v1))
              ((T_Kind_6 -> T_Inverse_1960 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> T_Inverse_1960 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_'8596''8658'_82
                 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v1)))
         ((AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T_Level_18
v2
            ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 T_Inverse_1960
v3
               ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v3 AgdaAny
v5)))
         ((AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Level_18
v2 AgdaAny
v5) ((AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Level_18
v2 AgdaAny
v5)
         (((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
            (\ AgdaAny
v6 ->
               (T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Kind_6 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'refl_160
                 (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v1))
            ((AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Level_18
v2 AgdaAny
v5))
         ((T_Kind_6 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Kind_6 -> AgdaAny
MAlonzo.Code.Function.Related.Propositional.du_K'45'reflexive_162
            (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_bijection_22)))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v4 ((T_Inverse_1960 -> AgdaAny -> AgdaAny)
-> T_Inverse_1960 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 T_Inverse_1960
v3 AgdaAny
v5))
-- Data.Product.Function.Dependent.Propositional.cong
d_cong_368 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> AgdaAny) -> AgdaAny
d_cong_368 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Kind_6
-> T_Inverse_1960
-> (AgdaAny -> AgdaAny)
-> AgdaAny
d_cong_368 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 T_Kind_6
v8 T_Inverse_1960
v9 AgdaAny -> AgdaAny
v10
  = T_Kind_6 -> T_Inverse_1960 -> (AgdaAny -> AgdaAny) -> AgdaAny
du_cong_368 T_Kind_6
v8 T_Inverse_1960
v9 AgdaAny -> AgdaAny
v10
du_cong_368 ::
  MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  (AgdaAny -> AgdaAny) -> AgdaAny
du_cong_368 :: T_Kind_6 -> T_Inverse_1960 -> (AgdaAny -> AgdaAny) -> AgdaAny
du_cong_368 T_Kind_6
v0 T_Inverse_1960
v1 AgdaAny -> AgdaAny
v2
  = 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 -> (AgdaAny -> T_Func_714) -> T_Func_714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Func_714 -> (AgdaAny -> T_Func_714) -> T_Func_714
du_Σ'45''10230'_36
             ((T_Inverse_1960 -> T_Func_714) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
                T_Inverse_1960 -> T_Func_714
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''10230'_638
                T_Inverse_1960
v1)
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
        -> (T_Func_714 -> (AgdaAny -> T_Func_714) -> T_Func_714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Func_714 -> (AgdaAny -> T_Func_714) -> T_Func_714
du_Σ'45''10230'_36
             ((T_Inverse_1960 -> T_Func_714) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
                T_Inverse_1960 -> T_Func_714
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''10229'_640
                T_Inverse_1960
v1)
             (((AgdaAny -> T_Level_18)
 -> T_Kind_6
 -> (AgdaAny -> T_Level_18)
 -> T_Inverse_1960
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (AgdaAny -> T_Level_18)
-> T_Kind_6
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_swap'45'coercions_346 AgdaAny
forall a. a
erased (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0) AgdaAny
forall a. a
erased (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2))
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
        -> (T_Surjection_846
 -> (AgdaAny -> T_Equivalence_1714) -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Surjection_846
-> (AgdaAny -> T_Equivalence_1714) -> T_Equivalence_1714
du_Σ'45''8660'_50
             ((T_Inverse_1960 -> T_Surjection_846) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
                T_Inverse_1960 -> T_Surjection_846
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8608'_644
                T_Inverse_1960
v1)
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_injection_14
        -> (T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Injection_776
du_Σ'45''8611'_66 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
        -> (T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Injection_776)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Inverse_1960 -> (AgdaAny -> T_Injection_776) -> T_Injection_776
du_Σ'45''8611'_66
             ((T_Inverse_1960 -> T_Inverse_1960) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
                T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Properties.Inverse.du_'8596''45'sym_38 T_Inverse_1960
v1)
             (((AgdaAny -> T_Level_18)
 -> T_Kind_6
 -> (AgdaAny -> T_Level_18)
 -> T_Inverse_1960
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (AgdaAny -> T_Level_18)
-> T_Kind_6
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_swap'45'coercions_346 AgdaAny
forall a. a
erased (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0) AgdaAny
forall a. a
erased (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2))
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
        -> (T_LeftInverse_1792 -> T_RightInverse_1880) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_LeftInverse_1792 -> T_RightInverse_1880
MAlonzo.Code.Function.Properties.RightInverse.du_'8617''8658''8618'_402
             ((T_LeftInverse_1792
 -> (AgdaAny -> T_LeftInverse_1792) -> T_LeftInverse_1792)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_LeftInverse_1792
-> (AgdaAny -> T_LeftInverse_1792) -> T_LeftInverse_1792
du_Σ'45''8617'_254
                ((T_Inverse_1960 -> T_LeftInverse_1792) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Inverse_1960 -> T_LeftInverse_1792
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8617'_650
                   ((T_Inverse_1960 -> T_Inverse_1960) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
                      T_Inverse_1960 -> T_Inverse_1960
MAlonzo.Code.Function.Properties.Inverse.du_'8596''45'sym_38 T_Inverse_1960
v1))
                ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                   (\ AgdaAny
v3 ->
                      (T_RightInverse_1880 -> T_LeftInverse_1792) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_RightInverse_1880 -> T_LeftInverse_1792
MAlonzo.Code.Function.Properties.RightInverse.du_'8618''8658''8617'_400
                        (((AgdaAny -> T_Level_18)
 -> T_Kind_6
 -> (AgdaAny -> T_Level_18)
 -> T_Inverse_1960
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                           (AgdaAny -> T_Level_18)
-> T_Kind_6
-> (AgdaAny -> T_Level_18)
-> T_Inverse_1960
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_swap'45'coercions_346 AgdaAny
forall a. a
erased (T_Kind_6 -> AgdaAny
forall a b. a -> b
coe T_Kind_6
v0) AgdaAny
forall a. a
erased (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)))))
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
        -> (T_Surjection_846
 -> (AgdaAny -> T_Surjection_846) -> T_Surjection_846)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Surjection_846
-> (AgdaAny -> T_Surjection_846) -> T_Surjection_846
du_Σ'45''8608'_210
             ((T_Inverse_1960 -> T_Surjection_846) -> T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe
                T_Inverse_1960 -> T_Surjection_846
MAlonzo.Code.Function.Properties.Inverse.du_'8596''8658''8608'_644
                T_Inverse_1960
v1)
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      T_Kind_6
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
        -> (T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> (AgdaAny -> T_Inverse_1960) -> T_Inverse_1960
du_Σ'45''8596'_298 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
      T_Kind_6
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError