{-# 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.Equality where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles
import qualified MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
import qualified MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Equality.Π
d_Π_16 :: p -> p -> p -> p -> p -> p -> ()
d_Π_16 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Π_16
  = C_Π'46'constructor_1171 (AgdaAny -> AgdaAny)
                            (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Function.Equality.Π._⟨$⟩_
d__'10216''36''10217'__38 :: T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 :: T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 T_Π_16
v0
  = case T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v0 of
      C_Π'46'constructor_1171 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1
      T_Π_16
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Equality.Π.cong
d_cong_40 :: T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_40 :: T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_40 T_Π_16
v0
  = case T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v0 of
      C_Π'46'constructor_1171 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_Π_16
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Equality._⟶_
d__'10230'__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 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> ()
d__'10230'__50 :: () -> () -> () -> () -> T_Setoid_44 -> T_Setoid_44 -> ()
d__'10230'__50 = () -> () -> () -> () -> T_Setoid_44 -> T_Setoid_44 -> ()
forall a. a
erased
-- Function.Equality.id
d_id_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> T_Π_16
d_id_62 :: () -> () -> T_Setoid_44 -> T_Π_16
d_id_62 ~()
v0 ~()
v1 ~T_Setoid_44
v2 = T_Π_16
du_id_62
du_id_62 :: T_Π_16
du_id_62 :: T_Π_16
du_id_62
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> AgdaAny -> T_Π_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16
C_Π'46'constructor_1171 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0)) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Equality._∘_
d__'8728'__82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Π_16 -> T_Π_16 -> T_Π_16
d__'8728'__82 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
-> T_Π_16
d__'8728'__82 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 ~T_Setoid_44
v5 ~()
v6 ~()
v7 ~T_Setoid_44
v8 T_Π_16
v9 T_Π_16
v10
  = T_Π_16 -> T_Π_16 -> T_Π_16
du__'8728'__82 T_Π_16
v9 T_Π_16
v10
du__'8728'__82 :: T_Π_16 -> T_Π_16 -> T_Π_16
du__'8728'__82 :: T_Π_16 -> T_Π_16 -> T_Π_16
du__'8728'__82 T_Π_16
v0 T_Π_16
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> AgdaAny -> T_Π_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16
C_Π'46'constructor_1171
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 T_Π_16
v0
              ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 T_Π_16
v1 AgdaAny
v2)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_40 T_Π_16
v0 ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 T_Π_16
v1 AgdaAny
v2)
              ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 T_Π_16
v1 AgdaAny
v3) ((T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_40 T_Π_16
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4)))
-- Function.Equality.const
d_const_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny -> T_Π_16
d_const_100 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> AgdaAny
-> T_Π_16
d_const_100 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 T_Setoid_44
v5 AgdaAny
v6 = T_Setoid_44 -> AgdaAny -> T_Π_16
du_const_100 T_Setoid_44
v5 AgdaAny
v6
du_const_100 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny -> T_Π_16
du_const_100 :: T_Setoid_44 -> AgdaAny -> T_Π_16
du_const_100 T_Setoid_44
v0 AgdaAny
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> AgdaAny -> T_Π_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16
C_Π'46'constructor_1171 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v1))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            let v4 :: t
v4
                  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> t
forall a b. a -> b
coe
                      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                      (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                      AgdaAny
v1 in
            (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 -> AgdaAny
forall a. a
v4)))
-- Function.Equality.setoid
d_setoid_116 ::
  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.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_setoid_116 :: ()
-> ()
-> ()
-> ()
-> T_Setoid_44
-> T_IndexedSetoid_18
-> T_Setoid_44
d_setoid_116 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Setoid_44
v4 T_IndexedSetoid_18
v5 = T_Setoid_44 -> T_IndexedSetoid_18 -> T_Setoid_44
du_setoid_116 T_Setoid_44
v4 T_IndexedSetoid_18
v5
du_setoid_116 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_setoid_116 :: T_Setoid_44 -> T_IndexedSetoid_18 -> T_Setoid_44
du_setoid_116 T_Setoid_44
v0 T_IndexedSetoid_18
v1
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_40 (AgdaAny -> T_Π_16
forall a b. a -> b
coe AgdaAny
v2)))
         ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 ->
               (T_IsIndexedEquivalence_22
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                 T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_sym_32
                 (T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.d_isEquivalence_38
                    (T_IndexedSetoid_18 -> T_IndexedSetoid_18
forall a b. a -> b
coe T_IndexedSetoid_18
v1))
                 AgdaAny
v6 AgdaAny
v5 ((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 AgdaAny
v2 AgdaAny
v6)
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 AgdaAny
v3 AgdaAny
v5)
                 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny
v4 AgdaAny
v6 AgdaAny
v5
                    ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> 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
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                       AgdaAny
v5 AgdaAny
v6 AgdaAny
v7))))
         ((AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 ->
               (T_IsIndexedEquivalence_22
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                 T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_34
                 (T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.d_isEquivalence_38
                    (T_IndexedSetoid_18 -> T_IndexedSetoid_18
forall a b. a -> b
coe T_IndexedSetoid_18
v1))
                 AgdaAny
v7 AgdaAny
v7 AgdaAny
v8 ((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 AgdaAny
v2 AgdaAny
v7)
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 AgdaAny
v3 AgdaAny
v7)
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 AgdaAny
v4 AgdaAny
v8)
                 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny
v5 AgdaAny
v7 AgdaAny
v7
                    ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                       (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                       AgdaAny
v7))
                 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9))))
-- Function.Equality._⇨_
d__'8680'__192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d__'8680'__192 :: () -> () -> () -> () -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
d__'8680'__192 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Setoid_44
v4 T_Setoid_44
v5 = T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du__'8680'__192 T_Setoid_44
v4 T_Setoid_44
v5
du__'8680'__192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du__'8680'__192 :: T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44
du__'8680'__192 T_Setoid_44
v0 T_Setoid_44
v1
  = (T_Setoid_44 -> T_IndexedSetoid_18 -> T_Setoid_44)
-> AgdaAny -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_Setoid_44 -> T_IndexedSetoid_18 -> T_Setoid_44
du_setoid_116 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)
      ((T_Setoid_44 -> T_IndexedSetoid_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> T_IndexedSetoid_18
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.du_indexedSetoid_100
         (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v1))
-- Function.Equality.≡-setoid
d_'8801''45'setoid_206 ::
  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.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_206 :: () -> () -> () -> () -> T_IndexedSetoid_18 -> T_Setoid_44
d_'8801''45'setoid_206 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_IndexedSetoid_18
v4
  = T_IndexedSetoid_18 -> T_Setoid_44
du_'8801''45'setoid_206 T_IndexedSetoid_18
v4
du_'8801''45'setoid_206 ::
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_'8801''45'setoid_206 :: T_IndexedSetoid_18 -> T_Setoid_44
du_'8801''45'setoid_206 T_IndexedSetoid_18
v0
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 ->
               (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_refl_30
                 (T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.d_isEquivalence_38
                    (T_IndexedSetoid_18 -> T_IndexedSetoid_18
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
                 AgdaAny
v2 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 AgdaAny
v2)))
         ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
               (T_IsIndexedEquivalence_22
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                 T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_sym_32
                 (T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.d_isEquivalence_38
                    (T_IndexedSetoid_18 -> T_IndexedSetoid_18
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
                 AgdaAny
v4 AgdaAny
v4 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 AgdaAny
v4) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v4) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 AgdaAny
v4)))
         ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
               (T_IsIndexedEquivalence_22
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                 T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_34
                 (T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.d_isEquivalence_38
                    (T_IndexedSetoid_18 -> T_IndexedSetoid_18
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
                 AgdaAny
v6 AgdaAny
v6 AgdaAny
v6 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1 AgdaAny
v6) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v6) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 AgdaAny
v6) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4 AgdaAny
v6)
                 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5 AgdaAny
v6))))
-- Function.Equality.flip
d_flip_272 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Π_16 -> T_Π_16
d_flip_272 :: ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> ()
-> ()
-> T_Setoid_44
-> T_Π_16
-> T_Π_16
d_flip_272 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 T_Setoid_44
v5 ~()
v6 ~()
v7 ~T_Setoid_44
v8 T_Π_16
v9
  = T_Setoid_44 -> T_Π_16 -> T_Π_16
du_flip_272 T_Setoid_44
v5 T_Π_16
v9
du_flip_272 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Π_16 -> T_Π_16
du_flip_272 :: T_Setoid_44 -> T_Π_16 -> T_Π_16
du_flip_272 T_Setoid_44
v0 T_Π_16
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> AgdaAny -> T_Π_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16
C_Π'46'constructor_1171
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Π_16
C_Π'46'constructor_1171
              ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                 (\ AgdaAny
v3 ->
                    (T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__38 T_Π_16
v1 AgdaAny
v3)
                      AgdaAny
v2))
              ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                 (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
                    (T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Π_16
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                      T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_40 T_Π_16
v1 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v2 AgdaAny
v2
                      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                         (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                         AgdaAny
v2)))))
      ((AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 -> (T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Π_16
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_40 T_Π_16
v1 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4))