{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Function.Construct.Symmetry 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Structures
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Construct.Symmetry._.f⁻¹
d_f'8315''185'_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny -> AgdaAny
d_f'8315''185'_48 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
d_f'8315''185'_48 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 T_Σ_14
v9 AgdaAny
v10
  = T_Σ_14 -> AgdaAny -> AgdaAny
du_f'8315''185'_48 T_Σ_14
v9 AgdaAny
v10
du_f'8315''185'_48 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny -> AgdaAny
du_f'8315''185'_48 :: T_Σ_14 -> AgdaAny -> AgdaAny
du_f'8315''185'_48 T_Σ_14
v0 AgdaAny
v1
  = (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
      ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v0 AgdaAny
v1)
-- Function.Construct.Symmetry._.f∘f⁻¹≡id
d_f'8728'f'8315''185''8801'id_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_f'8728'f'8315''185''8801'id_50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_f'8728'f'8315''185''8801'id_50 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7
                                 ~AgdaAny -> AgdaAny
v8 T_Σ_14
v9 AgdaAny
v10
  = T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_f'8728'f'8315''185''8801'id_50 T_Σ_14
v9 AgdaAny
v10
du_f'8728'f'8315''185''8801'id_50 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_f'8728'f'8315''185''8801'id_50 :: T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_f'8728'f'8315''185''8801'id_50 T_Σ_14
v0 AgdaAny
v1
  = (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
      ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v0 AgdaAny
v1)
-- Function.Construct.Symmetry._.injective
d_injective_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_52 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_injective_52 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny
v8 T_Σ_14
v9 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
               AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16
  = (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_52 AgdaAny -> AgdaAny
v8 T_Σ_14
v9 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16
du_injective_52 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_injective_52 :: (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_52 AgdaAny -> AgdaAny
v0 T_Σ_14
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v6 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 ((T_Σ_14 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny -> AgdaAny
du_f'8315''185'_48 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))) AgdaAny
v7
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v6
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> AgdaAny
v0
            (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
               ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v6)))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 ((T_Σ_14 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny -> AgdaAny
du_f'8315''185'_48 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> AgdaAny
v0
               (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                  ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v6)))
            AgdaAny
v6
            ((T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_f'8728'f'8315''185''8801'id_50 T_Σ_14
v1 AgdaAny
v6
               (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                  ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v6))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v2
                  (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                     ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v6)))))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 ((T_Σ_14 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny -> AgdaAny
du_f'8315''185'_48 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
            ((T_Σ_14 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny -> AgdaAny
du_f'8315''185'_48 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)) AgdaAny
v8))
      ((T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_f'8728'f'8315''185''8801'id_50 T_Σ_14
v1 AgdaAny
v7
         (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
            ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v7))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> AgdaAny
v2
            (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
               ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v7))))
-- Function.Construct.Symmetry._.surjective
d_surjective_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 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_surjective_64 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Σ_14
d_surjective_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 ~AgdaAny -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny
v8 T_Σ_14
v9 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12
  = (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Σ_14
du_surjective_64 AgdaAny -> AgdaAny
v8 T_Σ_14
v9 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12
du_surjective_64 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_surjective_64 :: (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Σ_14
du_surjective_64 AgdaAny -> AgdaAny
v0 T_Σ_14
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v4
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v5 AgdaAny
v6 ->
            (T_Σ_14 -> AgdaAny)
-> T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 T_Σ_14
v1
              (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                 ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v5))
              AgdaAny
v4
              ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
                 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny
v0
                    (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                       ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v5)))
                 AgdaAny
v5 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4)
                 ((T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Σ_14 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_f'8728'f'8315''185''8801'id_50 T_Σ_14
v1 AgdaAny
v5
                    (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                       ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v5))
                    ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny
v2
                       (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                          ((T_Σ_14 -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v5))))
                 AgdaAny
v6)))
-- Function.Construct.Symmetry._.bijective
d_bijective_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_bijective_72 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
d_bijective_72 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny
v8 T_Σ_14
v9 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
               AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13
  = (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
du_bijective_72 AgdaAny -> AgdaAny
v8 T_Σ_14
v9 AgdaAny -> AgdaAny
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13
du_bijective_72 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_bijective_72 :: (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
du_bijective_72 AgdaAny -> AgdaAny
v0 T_Σ_14
v1 AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (((AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> 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)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_52 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4)
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5))
      (((AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Σ_14
du_surjective_64 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4))
-- Function.Construct.Symmetry._.inverseʳ
d_inverse'691'_102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'691'_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_inverse'691'_102 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny
v11
                   AgdaAny
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'691'_102 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12
du_inverse'691'_102 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'691'_102 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'691'_102 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2
-- Function.Construct.Symmetry._.inverseˡ
d_inverse'737'_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_inverse'737'_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_inverse'737'_106 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny
v11
                   AgdaAny
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'737'_106 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 AgdaAny
v11 AgdaAny
v12
du_inverse'737'_106 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'737'_106 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'737'_106 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2
-- Function.Construct.Symmetry._.inverseᵇ
d_inverse'7495'_110 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_inverse'7495'_110 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Σ_14
d_inverse'7495'_110 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny
v9 T_Σ_14
v10
  = T_Σ_14 -> T_Σ_14
du_inverse'7495'_110 T_Σ_14
v10
du_inverse'7495'_110 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_inverse'7495'_110 :: T_Σ_14 -> T_Σ_14
du_inverse'7495'_110 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2
        -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Construct.Symmetry._.f⁻¹
d_f'8315''185'_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  AgdaAny -> AgdaAny
d_f'8315''185'_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_IsBijection_256
-> AgdaAny
-> AgdaAny
d_f'8315''185'_210 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 T_IsBijection_256
v9 AgdaAny
v10
  = T_IsBijection_256 -> AgdaAny -> AgdaAny
du_f'8315''185'_210 T_IsBijection_256
v9 AgdaAny
v10
du_f'8315''185'_210 ::
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  AgdaAny -> AgdaAny
du_f'8315''185'_210 :: T_IsBijection_256 -> AgdaAny -> AgdaAny
du_f'8315''185'_210 T_IsBijection_256
v0 AgdaAny
v1
  = (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
      ((T_IsBijection_256 -> AgdaAny -> T_Σ_14)
-> T_IsBijection_256 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_266 T_IsBijection_256
v0 AgdaAny
v1)
-- Function.Construct.Symmetry._.isBijection
d_isBijection_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256
d_isBijection_212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_IsBijection_256
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBijection_256
d_isBijection_212 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny
v8 T_IsBijection_256
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
  = (AgdaAny -> AgdaAny)
-> T_IsBijection_256
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBijection_256
du_isBijection_212 AgdaAny -> AgdaAny
v8 T_IsBijection_256
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
du_isBijection_212 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256
du_isBijection_212 :: (AgdaAny -> AgdaAny)
-> T_IsBijection_256
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBijection_256
du_isBijection_212 AgdaAny -> AgdaAny
v0 T_IsBijection_256
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
  = (T_IsInjection_98 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_256)
-> AgdaAny -> AgdaAny -> T_IsBijection_256
forall a b. a -> b
coe
      T_IsInjection_98 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_256
MAlonzo.Code.Function.Structures.C_constructor_340
      ((T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_98)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_98
MAlonzo.Code.Function.Structures.C_constructor_170
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.C_constructor_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2)
            ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8322'_36
               ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                  ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1))))
            ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34
               ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                  ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1)))))
         (((AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> 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)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_injective_52 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
            ((T_IsBijection_256 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> T_Σ_14
MAlonzo.Code.Function.Structures.du_bijective_332 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1))
            ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
               ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34
                  ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                     ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1)))))
            ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
               ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8322'_36
                  ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                     ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1)))))
            ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
               ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8322'_36
                  ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                     ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1)))))
            ((T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_cong_32
               ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                  ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1))))))
      (((AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Σ_14
du_surjective_64 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)
         ((T_IsBijection_256 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> T_Σ_14
MAlonzo.Code.Function.Structures.du_bijective_332 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1))
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
            ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34
               ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                  ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1)))))
         ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
            ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8322'_36
               ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                  ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1))))))
-- Function.Construct.Symmetry._.isBijection-≡
d_isBijection'45''8801'_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256
d_isBijection'45''8801'_232 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_IsBijection_256
-> T_IsBijection_256
d_isBijection'45''8801'_232 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny
v6 T_IsBijection_256
v7
  = (AgdaAny -> AgdaAny) -> T_IsBijection_256 -> T_IsBijection_256
du_isBijection'45''8801'_232 AgdaAny -> AgdaAny
v6 T_IsBijection_256
v7
du_isBijection'45''8801'_232 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_256
du_isBijection'45''8801'_232 :: (AgdaAny -> AgdaAny) -> T_IsBijection_256 -> T_IsBijection_256
du_isBijection'45''8801'_232 AgdaAny -> AgdaAny
v0 T_IsBijection_256
v1
  = ((AgdaAny -> AgdaAny)
 -> T_IsBijection_256
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsBijection_256)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsBijection_256
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> T_IsBijection_256
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBijection_256
du_isBijection_212 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_reflexive_42
              ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34
                 ((T_IsInjection_98 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_IsInjection_98 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_106
                    ((T_IsBijection_256 -> T_IsInjection_98) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> T_IsInjection_98
MAlonzo.Code.Function.Structures.d_isInjection_264 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1))))
              ((T_IsBijection_256 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256 -> AgdaAny -> AgdaAny
du_f'8315''185'_210 (T_IsBijection_256 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_256
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
-- Function.Construct.Symmetry._.isCongruent
d_isCongruent_332 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
d_isCongruent_332 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCongruent_22
d_isCongruent_332 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny
v9 T_IsCongruent_22
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11
  = T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCongruent_22
du_isCongruent_332 T_IsCongruent_22
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11
du_isCongruent_332 ::
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
du_isCongruent_332 :: T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCongruent_22
du_isCongruent_332 T_IsCongruent_22
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> T_IsEquivalence_28 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.C_constructor_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1)
      ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8322'_36 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v0))
      ((T_IsCongruent_22 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> T_IsEquivalence_28
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v0))
-- Function.Construct.Symmetry._.isLeftInverse
d_isLeftInverse_402 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346
d_isLeftInverse_402 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsRightInverse_438
-> T_IsLeftInverse_346
d_isLeftInverse_402 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny
v9 T_IsRightInverse_438
v10
  = T_IsRightInverse_438 -> T_IsLeftInverse_346
du_isLeftInverse_402 T_IsRightInverse_438
v10
du_isLeftInverse_402 ::
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346
du_isLeftInverse_402 :: T_IsRightInverse_438 -> T_IsLeftInverse_346
du_isLeftInverse_402 T_IsRightInverse_438
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLeftInverse_346)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLeftInverse_346
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLeftInverse_346
MAlonzo.Code.Function.Structures.C_constructor_432
      ((T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCongruent_22
du_isCongruent_332
         ((T_IsRightInverse_438 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_450 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v0))
         ((T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_452 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v0)))
      ((T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_cong_32
         ((T_IsRightInverse_438 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_450 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'737'_106
         ((T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_454 (T_IsRightInverse_438 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_438
v0)))
-- Function.Construct.Symmetry._.isRightInverse
d_isRightInverse_478 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438
d_isRightInverse_478 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsLeftInverse_346
-> T_IsRightInverse_438
d_isRightInverse_478 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny
v9 T_IsLeftInverse_346
v10
  = T_IsLeftInverse_346 -> T_IsRightInverse_438
du_isRightInverse_478 T_IsLeftInverse_346
v10
du_isRightInverse_478 ::
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_346 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_438
du_isRightInverse_478 :: T_IsLeftInverse_346 -> T_IsRightInverse_438
du_isRightInverse_478 T_IsLeftInverse_346
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsRightInverse_438)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsRightInverse_438
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsRightInverse_438
MAlonzo.Code.Function.Structures.C_constructor_520
      ((T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCongruent_22
du_isCongruent_332
         ((T_IsLeftInverse_346 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_358 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v0))
         ((T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_360 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v0)))
      ((T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_cong_32
         ((T_IsLeftInverse_346 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_358 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'691'_102
         ((T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_362 (T_IsLeftInverse_346 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_346
v0)))
-- Function.Construct.Symmetry._.isInverse
d_isInverse_556 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526
d_isInverse_556 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_IsInverse_526
-> T_IsInverse_526
d_isInverse_556 ~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 -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 ~AgdaAny -> AgdaAny
v8 ~AgdaAny -> AgdaAny
v9 T_IsInverse_526
v10
  = T_IsInverse_526 -> T_IsInverse_526
du_isInverse_556 T_IsInverse_526
v10
du_isInverse_556 ::
  MAlonzo.Code.Function.Structures.T_IsInverse_526 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_526
du_isInverse_556 :: T_IsInverse_526 -> T_IsInverse_526
du_isInverse_556 T_IsInverse_526
v0
  = (T_IsLeftInverse_346
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_526)
-> AgdaAny -> AgdaAny -> T_IsInverse_526
forall a b. a -> b
coe
      T_IsLeftInverse_346
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_526
MAlonzo.Code.Function.Structures.C_constructor_618
      ((T_IsRightInverse_438 -> T_IsLeftInverse_346) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsRightInverse_438 -> T_IsLeftInverse_346
du_isLeftInverse_402
         ((T_IsInverse_526 -> T_IsRightInverse_438) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsInverse_526 -> T_IsRightInverse_438
MAlonzo.Code.Function.Structures.du_isRightInverse_610 (T_IsInverse_526 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_inverse'691'_102
         ((T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLeftInverse_346 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_362
            ((T_IsInverse_526 -> T_IsLeftInverse_346) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsInverse_526 -> T_IsLeftInverse_346
MAlonzo.Code.Function.Structures.d_isLeftInverse_536 (T_IsInverse_526 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_526
v0))))
-- Function.Construct.Symmetry._.IB.Eq₁._≈_
d__'8776'__690 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__690 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__690 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Function.Construct.Symmetry._.IB.Eq₂._≈_
d__'8776'__716 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__716 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__716 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Function.Construct.Symmetry._.from
d_from_740 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  AgdaAny -> AgdaAny
d_from_740 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> AgdaAny
-> AgdaAny
d_from_740 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_46
v4 ~T_Setoid_46
v5 T_Bijection_1004
v6 AgdaAny
v7 = T_Bijection_1004 -> AgdaAny -> AgdaAny
du_from_740 T_Bijection_1004
v6 AgdaAny
v7
du_from_740 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  AgdaAny -> AgdaAny
du_from_740 :: T_Bijection_1004 -> AgdaAny -> AgdaAny
du_from_740 T_Bijection_1004
v0 AgdaAny
v1
  = (T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
      ((T_Bijection_1004 -> AgdaAny -> T_Σ_14)
-> T_Bijection_1004 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Bundles.du_surjective_1020 T_Bijection_1004
v0 AgdaAny
v1)
-- Function.Construct.Symmetry._.bijection
d_bijection_742 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_bijection_742 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_1004
d_bijection_742 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_46
v4 T_Setoid_46
v5 T_Bijection_1004
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
  = T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_1004
du_bijection_742 T_Setoid_46
v4 T_Setoid_46
v5 T_Bijection_1004
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
du_bijection_742 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_bijection_742 :: T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_1004
du_bijection_742 T_Setoid_46
v0 T_Setoid_46
v1 T_Bijection_1004
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Bijection_1004)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_1004
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Bijection_1004
MAlonzo.Code.Function.Bundles.C_constructor_1094
      ((T_Bijection_1004 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> AgdaAny
du_from_740 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v2)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3)
      (((AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
du_bijective_72
         ((T_Bijection_1004 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1012 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v2))
         ((T_Bijection_1004 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_bijective_1016 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v2))
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
            ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)))
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v1)))
         ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
            ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v1)))
         ((T_Bijection_1004 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_1014 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v2)))
-- Function.Construct.Symmetry.bijection-≡
d_bijection'45''8801'_750 ::
  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_46 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_bijection'45''8801'_750 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Level_18
-> T_Bijection_1004
-> T_Bijection_1004
d_bijection'45''8801'_750 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Setoid_46
v3 ~T_Level_18
v4 T_Bijection_1004
v5
  = T_Setoid_46 -> T_Bijection_1004 -> T_Bijection_1004
du_bijection'45''8801'_750 T_Setoid_46
v3 T_Bijection_1004
v5
du_bijection'45''8801'_750 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_bijection'45''8801'_750 :: T_Setoid_46 -> T_Bijection_1004 -> T_Bijection_1004
du_bijection'45''8801'_750 T_Setoid_46
v0 T_Bijection_1004
v1
  = (T_Setoid_46
 -> T_Setoid_46
 -> T_Bijection_1004
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Bijection_1004)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_1004
forall a b. a -> b
coe
      T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_1004
du_bijection_742 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)
      (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_reflexive_42
              ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
              ((T_Bijection_1004 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004 -> AgdaAny -> AgdaAny
du_from_740 (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
-- Function.Construct.Symmetry._.equivalence
d_equivalence_852 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_equivalence_852 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Equivalence_1858
-> T_Equivalence_1858
d_equivalence_852 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_46
v4 ~T_Setoid_46
v5 T_Equivalence_1858
v6
  = T_Equivalence_1858 -> T_Equivalence_1858
du_equivalence_852 T_Equivalence_1858
v6
du_equivalence_852 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_equivalence_852 :: T_Equivalence_1858 -> T_Equivalence_1858
du_equivalence_852 T_Equivalence_1858
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Equivalence_1858)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Equivalence_1858
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_1858
MAlonzo.Code.Function.Bundles.C_constructor_1940
      ((T_Equivalence_1858 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1870 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
      ((T_Equivalence_1858 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1868 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
      ((T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1874 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
      ((T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1872 (T_Equivalence_1858 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1858
v0))
-- Function.Construct.Symmetry._.rightInverse
d_rightInverse_930 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_rightInverse_930 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_LeftInverse_1942
-> T_RightInverse_2036
d_rightInverse_930 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_46
v4 ~T_Setoid_46
v5 T_LeftInverse_1942
v6
  = T_LeftInverse_1942 -> T_RightInverse_2036
du_rightInverse_930 T_LeftInverse_1942
v6
du_rightInverse_930 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_rightInverse_930 :: T_LeftInverse_1942 -> T_RightInverse_2036
du_rightInverse_930 T_LeftInverse_1942
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_2036)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_2036
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_2036
MAlonzo.Code.Function.Bundles.C_constructor_2120
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1956 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1954 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1960 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1958 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
      ((T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'737'_1962 (T_LeftInverse_1942 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1942
v0))
-- Function.Construct.Symmetry._.leftInverse
d_leftInverse_1016 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_leftInverse_1016 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_RightInverse_2036
-> T_LeftInverse_1942
d_leftInverse_1016 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_46
v4 ~T_Setoid_46
v5 T_RightInverse_2036
v6
  = T_RightInverse_2036 -> T_LeftInverse_1942
du_leftInverse_1016 T_RightInverse_2036
v6
du_leftInverse_1016 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du_leftInverse_1016 :: T_RightInverse_2036 -> T_LeftInverse_1942
du_leftInverse_1016 T_RightInverse_2036
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_LeftInverse_1942)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1942
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1942
MAlonzo.Code.Function.Bundles.C_constructor_2034
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2050 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2048 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2054 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_2052 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
      ((T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_2056 (T_RightInverse_2036 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_2036
v0))
-- Function.Construct.Symmetry._.inverse
d_inverse_1096 ::
  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_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_inverse_1096 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Inverse_2122
-> T_Inverse_2122
d_inverse_1096 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_46
v4 ~T_Setoid_46
v5 T_Inverse_2122
v6 = T_Inverse_2122 -> T_Inverse_2122
du_inverse_1096 T_Inverse_2122
v6
du_inverse_1096 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_inverse_1096 :: T_Inverse_2122 -> T_Inverse_2122
du_inverse_1096 T_Inverse_2122
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_2122)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Inverse_2122
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_2122
MAlonzo.Code.Function.Bundles.C_constructor_2220
      ((T_Inverse_2122 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_2136 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_2134 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_2140 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_2138 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v0))
      ((T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370
         ((T_Inverse_2122 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_inverse_2142 (T_Inverse_2122 -> AgdaAny
forall a b. a -> b
coe T_Inverse_2122
v0)))
-- Function.Construct.Symmetry.⤖-sym
d_'10518''45'sym_1186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_'10518''45'sym_1186 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_1004
-> T_Bijection_1004
d_'10518''45'sym_1186 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Bijection_1004
v4
  = T_Bijection_1004 -> T_Bijection_1004
du_'10518''45'sym_1186 T_Bijection_1004
v4
du_'10518''45'sym_1186 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
du_'10518''45'sym_1186 :: T_Bijection_1004 -> T_Bijection_1004
du_'10518''45'sym_1186 T_Bijection_1004
v0
  = (T_Setoid_46
 -> T_Setoid_46
 -> T_Bijection_1004
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Bijection_1004)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_1004
forall a b. a -> b
coe
      T_Setoid_46
-> T_Setoid_46
-> T_Bijection_1004
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_1004
du_bijection_742
      (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Bijection_1004 -> AgdaAny
forall a b. a -> b
coe T_Bijection_1004
v0) AgdaAny
forall a. a
erased
-- Function.Construct.Symmetry.⇔-sym
d_'8660''45'sym_1190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_'8660''45'sym_1190 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1858
-> T_Equivalence_1858
d_'8660''45'sym_1190 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Equivalence_1858 -> T_Equivalence_1858
du_'8660''45'sym_1190
du_'8660''45'sym_1190 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_'8660''45'sym_1190 :: T_Equivalence_1858 -> T_Equivalence_1858
du_'8660''45'sym_1190 = (T_Equivalence_1858 -> T_Equivalence_1858)
-> T_Equivalence_1858 -> T_Equivalence_1858
forall a b. a -> b
coe T_Equivalence_1858 -> T_Equivalence_1858
du_equivalence_852
-- Function.Construct.Symmetry.↩-sym
d_'8617''45'sym_1192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_'8617''45'sym_1192 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_LeftInverse_1942
-> T_RightInverse_2036
d_'8617''45'sym_1192 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_LeftInverse_1942 -> T_RightInverse_2036
du_'8617''45'sym_1192
du_'8617''45'sym_1192 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
du_'8617''45'sym_1192 :: T_LeftInverse_1942 -> T_RightInverse_2036
du_'8617''45'sym_1192 = (T_LeftInverse_1942 -> T_RightInverse_2036)
-> T_LeftInverse_1942 -> T_RightInverse_2036
forall a b. a -> b
coe T_LeftInverse_1942 -> T_RightInverse_2036
du_rightInverse_930
-- Function.Construct.Symmetry.↪-sym
d_'8618''45'sym_1194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_'8618''45'sym_1194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_RightInverse_2036
-> T_LeftInverse_1942
d_'8618''45'sym_1194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_RightInverse_2036 -> T_LeftInverse_1942
du_'8618''45'sym_1194
du_'8618''45'sym_1194 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
du_'8618''45'sym_1194 :: T_RightInverse_2036 -> T_LeftInverse_1942
du_'8618''45'sym_1194 = (T_RightInverse_2036 -> T_LeftInverse_1942)
-> T_RightInverse_2036 -> T_LeftInverse_1942
forall a b. a -> b
coe T_RightInverse_2036 -> T_LeftInverse_1942
du_leftInverse_1016
-- Function.Construct.Symmetry.↔-sym
d_'8596''45'sym_1196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_'8596''45'sym_1196 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Inverse_2122
d_'8596''45'sym_1196 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'sym_1196
du_'8596''45'sym_1196 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_'8596''45'sym_1196 :: T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'sym_1196 = (T_Inverse_2122 -> T_Inverse_2122)
-> T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122
du_inverse_1096
-- Function.Construct.Symmetry.sym-⤖
d_sym'45''10518'_1198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_1004
d_sym'45''10518'_1198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_1004
-> T_Bijection_1004
d_sym'45''10518'_1198 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_Bijection_1004
v4
  = (T_Bijection_1004 -> T_Bijection_1004)
-> T_Bijection_1004 -> T_Bijection_1004
forall a b. a -> b
coe T_Bijection_1004 -> T_Bijection_1004
du_'10518''45'sym_1186 T_Bijection_1004
v4
-- Function.Construct.Symmetry.sym-⇔
d_sym'45''8660'_1200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_sym'45''8660'_1200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1858
-> T_Equivalence_1858
d_sym'45''8660'_1200 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 = (T_Equivalence_1858 -> T_Equivalence_1858)
-> T_Equivalence_1858 -> T_Equivalence_1858
forall a b. a -> b
coe T_Equivalence_1858 -> T_Equivalence_1858
du_'8660''45'sym_1190
-- Function.Construct.Symmetry.sym-↩
d_sym'45''8617'_1202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036
d_sym'45''8617'_1202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_LeftInverse_1942
-> T_RightInverse_2036
d_sym'45''8617'_1202 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 = (T_LeftInverse_1942 -> T_RightInverse_2036)
-> T_LeftInverse_1942 -> T_RightInverse_2036
forall a b. a -> b
coe T_LeftInverse_1942 -> T_RightInverse_2036
du_'8617''45'sym_1192
-- Function.Construct.Symmetry.sym-↪
d_sym'45''8618'_1204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_2036 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1942
d_sym'45''8618'_1204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_RightInverse_2036
-> T_LeftInverse_1942
d_sym'45''8618'_1204 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 = (T_RightInverse_2036 -> T_LeftInverse_1942)
-> T_RightInverse_2036 -> T_LeftInverse_1942
forall a b. a -> b
coe T_RightInverse_2036 -> T_LeftInverse_1942
du_'8618''45'sym_1194
-- Function.Construct.Symmetry.sym-↔
d_sym'45''8596'_1206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_sym'45''8596'_1206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_2122
-> T_Inverse_2122
d_sym'45''8596'_1206 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 = (T_Inverse_2122 -> T_Inverse_2122)
-> T_Inverse_2122 -> T_Inverse_2122
forall a b. a -> b
coe T_Inverse_2122 -> T_Inverse_2122
du_'8596''45'sym_1196