{-# 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'_206 ::
  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_238 ->
  AgdaAny -> AgdaAny
d_f'8315''185'_206 :: 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_238
-> AgdaAny
-> AgdaAny
d_f'8315''185'_206 ~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_238
v9 AgdaAny
v10
  = T_IsBijection_238 -> AgdaAny -> AgdaAny
du_f'8315''185'_206 T_IsBijection_238
v9 AgdaAny
v10
du_f'8315''185'_206 ::
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  AgdaAny -> AgdaAny
du_f'8315''185'_206 :: T_IsBijection_238 -> AgdaAny -> AgdaAny
du_f'8315''185'_206 T_IsBijection_238
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_238 -> AgdaAny -> T_Σ_14)
-> T_IsBijection_238 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Structures.d_surjective_248 T_IsBijection_238
v0 AgdaAny
v1)
-- Function.Construct.Symmetry._.isBijection
d_isBijection_208 ::
  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_238 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238
d_isBijection_208 :: 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_238
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBijection_238
d_isBijection_208 ~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_238
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
  = (AgdaAny -> AgdaAny)
-> T_IsBijection_238
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBijection_238
du_isBijection_208 AgdaAny -> AgdaAny
v8 T_IsBijection_238
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
du_isBijection_208 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238
du_isBijection_208 :: (AgdaAny -> AgdaAny)
-> T_IsBijection_238
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBijection_238
du_isBijection_208 AgdaAny -> AgdaAny
v0 T_IsBijection_238
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
  = (T_IsInjection_92 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> T_IsBijection_238
forall a b. a -> b
coe
      T_IsInjection_92 -> (AgdaAny -> T_Σ_14) -> T_IsBijection_238
MAlonzo.Code.Function.Structures.C_IsBijection'46'constructor_10113
      ((T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_92)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInjection_92
MAlonzo.Code.Function.Structures.C_IsInjection'46'constructor_3997
         (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.C_IsCongruent'46'constructor_985
            ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2)
            (let v3 :: T_IsInjection_92
v3
                   = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> T_IsBijection_238
forall a b. a -> b
coe T_IsBijection_238
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v4 :: T_IsCongruent_22
v4
                      = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v3) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsCongruent_22 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8322'_36
                     (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v4))))
            (let v3 :: T_IsInjection_92
v3
                   = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> T_IsBijection_238
forall a b. a -> b
coe T_IsBijection_238
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v4 :: T_IsCongruent_22
v4
                      = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v3) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsCongruent_22 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34
                     (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v4)))))
         (((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_238 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238 -> T_Σ_14
MAlonzo.Code.Function.Structures.du_bijective_310 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v1))
            (let v3 :: T_IsInjection_92
v3
                   = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> T_IsBijection_238
forall a b. a -> b
coe T_IsBijection_238
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v4 :: T_IsCongruent_22
v4
                      = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v3) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     ((T_IsCongruent_22 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34
                        (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v4)))))
            (let v3 :: T_IsInjection_92
v3
                   = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> T_IsBijection_238
forall a b. a -> b
coe T_IsBijection_238
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v4 :: T_IsCongruent_22
v4
                      = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v3) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v5 :: t
v5
                         = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_66 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v4) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                        ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5))))))
            (let v3 :: T_IsInjection_92
v3
                   = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> T_IsBijection_238
forall a b. a -> b
coe T_IsBijection_238
v1) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v4 :: T_IsCongruent_22
v4
                      = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v3) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v5 :: t
v5
                         = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_66 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v4) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                        ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5))))))
            ((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_92 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100
                  ((T_IsBijection_238 -> T_IsInjection_92) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
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_238 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238 -> T_Σ_14
MAlonzo.Code.Function.Structures.du_bijective_310 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v1))
         (let v3 :: T_IsInjection_92
v3
                = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> T_IsBijection_238
forall a b. a -> b
coe T_IsBijection_238
v1) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v4 :: T_IsCongruent_22
v4
                   = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v3) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                  ((T_IsCongruent_22 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34
                     (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v4)))))
         (let v3 :: T_IsInjection_92
v3
                = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> T_IsBijection_238
forall a b. a -> b
coe T_IsBijection_238
v1) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v4 :: T_IsCongruent_22
v4
                   = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v3) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v5 :: t
v5
                      = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_66 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v4) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                     ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                        (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5)))))))
-- Function.Construct.Symmetry._.isBijection-≡
d_isBijection'45''8801'_228 ::
  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_238 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238
d_isBijection'45''8801'_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_IsBijection_238
-> T_IsBijection_238
d_isBijection'45''8801'_228 ~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_238
v7
  = (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsBijection_238
du_isBijection'45''8801'_228 AgdaAny -> AgdaAny
v6 T_IsBijection_238
v7
du_isBijection'45''8801'_228 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238 ->
  MAlonzo.Code.Function.Structures.T_IsBijection_238
du_isBijection'45''8801'_228 :: (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsBijection_238
du_isBijection'45''8801'_228 AgdaAny -> AgdaAny
v0 T_IsBijection_238
v1
  = ((AgdaAny -> AgdaAny)
 -> T_IsBijection_238
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsBijection_238
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> T_IsBijection_238
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsBijection_238
du_isBijection_208 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            let v5 :: T_IsInjection_92
v5
                  = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (T_IsBijection_238 -> T_IsBijection_238
forall a b. a -> b
coe T_IsBijection_238
v1) in
            AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (let v6 :: T_IsCongruent_22
v6
                     = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v5) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v7 :: t
v7
                        = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_40 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v6) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                       ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7))
                       ((T_IsBijection_238 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238 -> AgdaAny -> AgdaAny
du_f'8315''185'_206 (T_IsBijection_238 -> AgdaAny
forall a b. a -> b
coe T_IsBijection_238
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))))))
-- Function.Construct.Symmetry._.isCongruent
d_isCongruent_324 ::
  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_324 :: 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_324 ~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_324 T_IsCongruent_22
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11
du_isCongruent_324 ::
  MAlonzo.Code.Function.Structures.T_IsCongruent_22 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Structures.T_IsCongruent_22
du_isCongruent_324 :: T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCongruent_22
du_isCongruent_324 T_IsCongruent_22
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsCongruent_22)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsCongruent_22
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> T_IsEquivalence_26 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.C_IsCongruent'46'constructor_985
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1)
      ((T_IsCongruent_22 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> T_IsEquivalence_26
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_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsCongruent_22 -> T_IsEquivalence_26
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_390 ::
  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_408 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322
d_isLeftInverse_390 :: 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_408
-> T_IsLeftInverse_322
d_isLeftInverse_390 ~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_408
v10
  = T_IsRightInverse_408 -> T_IsLeftInverse_322
du_isLeftInverse_390 T_IsRightInverse_408
v10
du_isLeftInverse_390 ::
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408 ->
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322
du_isLeftInverse_390 :: T_IsRightInverse_408 -> T_IsLeftInverse_322
du_isLeftInverse_390 T_IsRightInverse_408
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsLeftInverse_322)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsLeftInverse_322
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsLeftInverse_322
MAlonzo.Code.Function.Structures.C_IsLeftInverse'46'constructor_14363
      ((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_324
         ((T_IsRightInverse_408 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_420 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v0))
         ((T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_422 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
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_408 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_420 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
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_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'691'_424 (T_IsRightInverse_408 -> AgdaAny
forall a b. a -> b
coe T_IsRightInverse_408
v0)))
-- Function.Construct.Symmetry._.isRightInverse
d_isRightInverse_462 ::
  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_322 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408
d_isRightInverse_462 :: 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_322
-> T_IsRightInverse_408
d_isRightInverse_462 ~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_322
v10
  = T_IsLeftInverse_322 -> T_IsRightInverse_408
du_isRightInverse_462 T_IsLeftInverse_322
v10
du_isRightInverse_462 ::
  MAlonzo.Code.Function.Structures.T_IsLeftInverse_322 ->
  MAlonzo.Code.Function.Structures.T_IsRightInverse_408
du_isRightInverse_462 :: T_IsLeftInverse_322 -> T_IsRightInverse_408
du_isRightInverse_462 T_IsLeftInverse_322
v0
  = (T_IsCongruent_22
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsRightInverse_408)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsRightInverse_408
forall a b. a -> b
coe
      T_IsCongruent_22
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsRightInverse_408
MAlonzo.Code.Function.Structures.C_IsRightInverse'46'constructor_18837
      ((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_324
         ((T_IsLeftInverse_322 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_334 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v0))
         ((T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_from'45'cong_336 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
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_322 -> T_IsCongruent_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_334 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
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_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_338 (T_IsLeftInverse_322 -> AgdaAny
forall a b. a -> b
coe T_IsLeftInverse_322
v0)))
-- Function.Construct.Symmetry._.isInverse
d_isInverse_536 ::
  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_490 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490
d_isInverse_536 :: 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_490
-> T_IsInverse_490
d_isInverse_536 ~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_490
v10
  = T_IsInverse_490 -> T_IsInverse_490
du_isInverse_536 T_IsInverse_490
v10
du_isInverse_536 ::
  MAlonzo.Code.Function.Structures.T_IsInverse_490 ->
  MAlonzo.Code.Function.Structures.T_IsInverse_490
du_isInverse_536 :: T_IsInverse_490 -> T_IsInverse_490
du_isInverse_536 T_IsInverse_490
v0
  = (T_IsLeftInverse_322
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_490)
-> AgdaAny -> AgdaAny -> T_IsInverse_490
forall a b. a -> b
coe
      T_IsLeftInverse_322
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsInverse_490
MAlonzo.Code.Function.Structures.C_IsInverse'46'constructor_22449
      ((T_IsRightInverse_408 -> T_IsLeftInverse_322) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsRightInverse_408 -> T_IsLeftInverse_322
du_isLeftInverse_390
         ((T_IsInverse_490 -> T_IsRightInverse_408) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsInverse_490 -> T_IsRightInverse_408
MAlonzo.Code.Function.Structures.du_isRightInverse_570 (T_IsInverse_490 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490
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_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Structures.d_inverse'737'_338
            ((T_IsInverse_490 -> T_IsLeftInverse_322) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsInverse_490 -> T_IsLeftInverse_322
MAlonzo.Code.Function.Structures.d_isLeftInverse_500 (T_IsInverse_490 -> AgdaAny
forall a b. a -> b
coe T_IsInverse_490
v0))))
-- Function.Construct.Symmetry._.IB.Eq₁._≈_
d__'8776'__666 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__666 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__666 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- 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_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__690 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__690 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Function.Construct.Symmetry._.from
d_from_712 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 -> AgdaAny -> AgdaAny
d_from_712 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> AgdaAny
-> AgdaAny
d_from_712 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Bijection_926
v6 AgdaAny
v7 = T_Bijection_926 -> AgdaAny -> AgdaAny
du_from_712 T_Bijection_926
v6 AgdaAny
v7
du_from_712 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 -> AgdaAny -> AgdaAny
du_from_712 :: T_Bijection_926 -> AgdaAny -> AgdaAny
du_from_712 T_Bijection_926
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_926 -> AgdaAny -> T_Σ_14)
-> T_Bijection_926 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> T_Σ_14
MAlonzo.Code.Function.Bundles.du_surjective_942 T_Bijection_926
v0 AgdaAny
v1)
-- Function.Construct.Symmetry._.bijection
d_bijection_714 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_bijection_714 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_926
d_bijection_714 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_44
v4 T_Setoid_44
v5 T_Bijection_926
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
  = T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_926
du_bijection_714 T_Setoid_44
v4 T_Setoid_44
v5 T_Bijection_926
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
du_bijection_714 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_bijection_714 :: T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_926
du_bijection_714 T_Setoid_44
v0 T_Setoid_44
v1 T_Bijection_926
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Bijection_926)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_926
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Bijection_926
MAlonzo.Code.Function.Bundles.C_Bijection'46'constructor_15277
      ((T_Bijection_926 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> AgdaAny
du_from_712 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
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_926 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_934 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v2))
         ((T_Bijection_926 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_bijective_938 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v2))
         (let v4 :: t
v4
                = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238
MAlonzo.Code.Function.Bundles.du_isBijection_960 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0) (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1)
                    (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v2) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsInjection_92
v5
                   = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (AgdaAny -> T_IsBijection_238
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v6 :: T_IsCongruent_22
v6
                      = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v5) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                     ((T_IsCongruent_22 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsCongruent_22 -> T_IsEquivalence_26
MAlonzo.Code.Function.Structures.d_isEquivalence'8321'_34
                        (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v6))))))
         (let v4 :: t
v4
                = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238
MAlonzo.Code.Function.Bundles.du_isBijection_960 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0) (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1)
                    (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v2) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsInjection_92
v5
                   = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (AgdaAny -> T_IsBijection_238
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v6 :: T_IsCongruent_22
v6
                      = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v5) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v7 :: t
v7
                         = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_66 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v6) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                        ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))))))
         (let v4 :: t
v4
                = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                    T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238
MAlonzo.Code.Function.Bundles.du_isBijection_960 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0) (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1)
                    (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v2) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsInjection_92
v5
                   = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (AgdaAny -> T_IsBijection_238
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (let v6 :: T_IsCongruent_22
v6
                      = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v5) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v7 :: t
v7
                         = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_66 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v6) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                        ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7)))))))
         ((T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_cong_936 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v2)))
-- Function.Construct.Symmetry.bijection-≡
d_bijection'45''8801'_722 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_bijection'45''8801'_722 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Bijection_926
-> T_Bijection_926
d_bijection'45''8801'_722 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Setoid_44
v3 ~T_Level_18
v4 T_Bijection_926
v5
  = T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926
du_bijection'45''8801'_722 T_Setoid_44
v3 T_Bijection_926
v5
du_bijection'45''8801'_722 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_bijection'45''8801'_722 :: T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926
du_bijection'45''8801'_722 T_Setoid_44
v0 T_Bijection_926
v1
  = (T_Setoid_44
 -> T_Setoid_44
 -> T_Bijection_926
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Bijection_926)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_926
forall a b. a -> b
coe
      T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_926
du_bijection_714 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            let v5 :: t
v5
                  = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                      T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238
MAlonzo.Code.Function.Bundles.du_isBijection_960 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
                      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
                      (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v1) in
            AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (let v6 :: T_IsInjection_92
v6
                     = T_IsBijection_238 -> T_IsInjection_92
MAlonzo.Code.Function.Structures.d_isInjection_246 (AgdaAny -> T_IsBijection_238
forall a b. a -> b
coe AgdaAny
forall a. a
v5) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (let v7 :: T_IsCongruent_22
v7
                        = T_IsInjection_92 -> T_IsCongruent_22
MAlonzo.Code.Function.Structures.d_isCongruent_100 (T_IsInjection_92 -> T_IsInjection_92
forall a b. a -> b
coe T_IsInjection_92
v6) in
                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (let v8 :: t
v8
                           = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_IsCongruent_22 -> T_Setoid_44
MAlonzo.Code.Function.Structures.du_setoid_40 (T_IsCongruent_22 -> AgdaAny
forall a b. a -> b
coe T_IsCongruent_22
v7) in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
                          ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                          ((T_Bijection_926 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Bijection_926 -> AgdaAny -> AgdaAny
du_from_712 (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))))))
-- Function.Construct.Symmetry._.equivalence
d_equivalence_820 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_equivalence_820 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Equivalence_1714
-> T_Equivalence_1714
d_equivalence_820 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Equivalence_1714
v6
  = T_Equivalence_1714 -> T_Equivalence_1714
du_equivalence_820 T_Equivalence_1714
v6
du_equivalence_820 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_equivalence_820 :: T_Equivalence_1714 -> T_Equivalence_1714
du_equivalence_820 T_Equivalence_1714
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.C_Equivalence'46'constructor_25797
      ((T_Equivalence_1714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1726 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
      ((T_Equivalence_1714 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1724 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
      ((T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1730 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
      ((T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1728 (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
v0))
-- Function.Construct.Symmetry._.rightInverse
d_rightInverse_894 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_rightInverse_894 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_LeftInverse_1792
-> T_RightInverse_1880
d_rightInverse_894 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_LeftInverse_1792
v6
  = T_LeftInverse_1792 -> T_RightInverse_1880
du_rightInverse_894 T_LeftInverse_1792
v6
du_rightInverse_894 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_rightInverse_894 :: T_LeftInverse_1792 -> T_RightInverse_1880
du_rightInverse_894 T_LeftInverse_1792
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_RightInverse_1880)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_RightInverse_1880
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_RightInverse_1880
MAlonzo.Code.Function.Bundles.C_RightInverse'46'constructor_34573
      ((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))
      ((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))
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1810 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1808 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
      ((T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'737'_1812 (T_LeftInverse_1792 -> AgdaAny
forall a b. a -> b
coe T_LeftInverse_1792
v0))
-- Function.Construct.Symmetry._.leftInverse
d_leftInverse_976 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_leftInverse_976 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_RightInverse_1880
-> T_LeftInverse_1792
d_leftInverse_976 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_RightInverse_1880
v6
  = T_RightInverse_1880 -> T_LeftInverse_1792
du_leftInverse_976 T_RightInverse_1880
v6
du_leftInverse_976 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_leftInverse_976 :: T_RightInverse_1880 -> T_LeftInverse_1792
du_leftInverse_976 T_RightInverse_1880
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_LeftInverse_1792)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_LeftInverse_1792
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_LeftInverse_1792
MAlonzo.Code.Function.Bundles.C_LeftInverse'46'constructor_29775
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1894 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1892 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1898 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1896 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
      ((T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_inverse'691'_1900 (T_RightInverse_1880 -> AgdaAny
forall a b. a -> b
coe T_RightInverse_1880
v0))
-- Function.Construct.Symmetry._.inverse
d_inverse_1052 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_inverse_1052 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Inverse_1960
-> T_Inverse_1960
d_inverse_1052 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Inverse_1960
v6 = T_Inverse_1960 -> T_Inverse_1960
du_inverse_1052 T_Inverse_1960
v6
du_inverse_1052 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_inverse_1052 :: T_Inverse_1960 -> T_Inverse_1960
du_inverse_1052 T_Inverse_1960
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_Inverse_1960)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Inverse_1960
MAlonzo.Code.Function.Bundles.C_Inverse'46'constructor_38621
      ((T_Inverse_1960 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from_1974 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to_1972 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_from'45'cong_1978 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0))
      ((T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Bundles.d_to'45'cong_1976 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
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_1960 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960 -> T_Σ_14
MAlonzo.Code.Function.Bundles.d_inverse_1980 (T_Inverse_1960 -> AgdaAny
forall a b. a -> b
coe T_Inverse_1960
v0)))
-- Function.Construct.Symmetry.⤖-sym
d_'10518''45'sym_1138 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_'10518''45'sym_1138 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_926
-> T_Bijection_926
d_'10518''45'sym_1138 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Bijection_926
v4
  = T_Bijection_926 -> T_Bijection_926
du_'10518''45'sym_1138 T_Bijection_926
v4
du_'10518''45'sym_1138 ::
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
du_'10518''45'sym_1138 :: T_Bijection_926 -> T_Bijection_926
du_'10518''45'sym_1138 T_Bijection_926
v0
  = (T_Setoid_44
 -> T_Setoid_44
 -> T_Bijection_926
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Bijection_926)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Bijection_926
forall a b. a -> b
coe
      T_Setoid_44
-> T_Setoid_44
-> T_Bijection_926
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Bijection_926
du_bijection_714
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      (T_Bijection_926 -> AgdaAny
forall a b. a -> b
coe T_Bijection_926
v0) AgdaAny
forall a. a
erased
-- Function.Construct.Symmetry.⇔-sym
d_'8660''45'sym_1142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'8660''45'sym_1142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1714
-> T_Equivalence_1714
d_'8660''45'sym_1142 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Equivalence_1714 -> T_Equivalence_1714
du_'8660''45'sym_1142
du_'8660''45'sym_1142 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'8660''45'sym_1142 :: T_Equivalence_1714 -> T_Equivalence_1714
du_'8660''45'sym_1142 = (T_Equivalence_1714 -> T_Equivalence_1714)
-> T_Equivalence_1714 -> T_Equivalence_1714
forall a b. a -> b
coe T_Equivalence_1714 -> T_Equivalence_1714
du_equivalence_820
-- Function.Construct.Symmetry.↩-sym
d_'8617''45'sym_1144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_'8617''45'sym_1144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_LeftInverse_1792
-> T_RightInverse_1880
d_'8617''45'sym_1144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_LeftInverse_1792 -> T_RightInverse_1880
du_'8617''45'sym_1144
du_'8617''45'sym_1144 ::
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
du_'8617''45'sym_1144 :: T_LeftInverse_1792 -> T_RightInverse_1880
du_'8617''45'sym_1144 = (T_LeftInverse_1792 -> T_RightInverse_1880)
-> T_LeftInverse_1792 -> T_RightInverse_1880
forall a b. a -> b
coe T_LeftInverse_1792 -> T_RightInverse_1880
du_rightInverse_894
-- Function.Construct.Symmetry.↪-sym
d_'8618''45'sym_1146 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_'8618''45'sym_1146 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_RightInverse_1880
-> T_LeftInverse_1792
d_'8618''45'sym_1146 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_RightInverse_1880 -> T_LeftInverse_1792
du_'8618''45'sym_1146
du_'8618''45'sym_1146 ::
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
du_'8618''45'sym_1146 :: T_RightInverse_1880 -> T_LeftInverse_1792
du_'8618''45'sym_1146 = (T_RightInverse_1880 -> T_LeftInverse_1792)
-> T_RightInverse_1880 -> T_LeftInverse_1792
forall a b. a -> b
coe T_RightInverse_1880 -> T_LeftInverse_1792
du_leftInverse_976
-- Function.Construct.Symmetry.↔-sym
d_'8596''45'sym_1148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_'8596''45'sym_1148 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Inverse_1960
d_'8596''45'sym_1148 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'sym_1148
du_'8596''45'sym_1148 ::
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_'8596''45'sym_1148 :: T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'sym_1148 = (T_Inverse_1960 -> T_Inverse_1960)
-> T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960
du_inverse_1052
-- Function.Construct.Symmetry.sym-⤖
d_sym'45''10518'_1150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926 ->
  MAlonzo.Code.Function.Bundles.T_Bijection_926
d_sym'45''10518'_1150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Bijection_926
-> T_Bijection_926
d_sym'45''10518'_1150 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_Bijection_926
v4
  = (T_Bijection_926 -> T_Bijection_926)
-> T_Bijection_926 -> T_Bijection_926
forall a b. a -> b
coe T_Bijection_926 -> T_Bijection_926
du_'10518''45'sym_1138 T_Bijection_926
v4
-- Function.Construct.Symmetry.sym-⇔
d_sym'45''8660'_1152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_sym'45''8660'_1152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1714
-> T_Equivalence_1714
d_sym'45''8660'_1152 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 = (T_Equivalence_1714 -> T_Equivalence_1714)
-> T_Equivalence_1714 -> T_Equivalence_1714
forall a b. a -> b
coe T_Equivalence_1714 -> T_Equivalence_1714
du_'8660''45'sym_1142
-- Function.Construct.Symmetry.sym-↩
d_sym'45''8617'_1154 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792 ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880
d_sym'45''8617'_1154 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_LeftInverse_1792
-> T_RightInverse_1880
d_sym'45''8617'_1154 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 = (T_LeftInverse_1792 -> T_RightInverse_1880)
-> T_LeftInverse_1792 -> T_RightInverse_1880
forall a b. a -> b
coe T_LeftInverse_1792 -> T_RightInverse_1880
du_'8617''45'sym_1144
-- Function.Construct.Symmetry.sym-↪
d_sym'45''8618'_1156 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_RightInverse_1880 ->
  MAlonzo.Code.Function.Bundles.T_LeftInverse_1792
d_sym'45''8618'_1156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_RightInverse_1880
-> T_LeftInverse_1792
d_sym'45''8618'_1156 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 = (T_RightInverse_1880 -> T_LeftInverse_1792)
-> T_RightInverse_1880 -> T_LeftInverse_1792
forall a b. a -> b
coe T_RightInverse_1880 -> T_LeftInverse_1792
du_'8618''45'sym_1146
-- Function.Construct.Symmetry.sym-↔
d_sym'45''8596'_1158 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_sym'45''8596'_1158 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Inverse_1960
-> T_Inverse_1960
d_sym'45''8596'_1158 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 = (T_Inverse_1960 -> T_Inverse_1960)
-> T_Inverse_1960 -> T_Inverse_1960
forall a b. a -> b
coe T_Inverse_1960 -> T_Inverse_1960
du_'8596''45'sym_1148