{-# 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 Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Data.Product.Base qualified
import MAlonzo.Code.Function.Bundles qualified
import MAlonzo.Code.Function.Structures qualified
import MAlonzo.Code.Relation.Binary.Bundles qualified
import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
import MAlonzo.Code.Relation.Binary.Structures qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- 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 :: AgdaAny
v5
                         = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v5
                         = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v5
                      = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v7
                        = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v4
                = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v4
                = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v7
                         = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> AgdaAny
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
v7)))))))
         (let v4 :: AgdaAny
v4
                = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v7
                         = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v5
                  = (T_Setoid_44
 -> T_Setoid_44 -> T_Bijection_926 -> T_IsBijection_238)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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
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 :: AgdaAny
v8
                           = (T_IsCongruent_22 -> T_Setoid_44) -> AgdaAny -> AgdaAny
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
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