{-# 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.Relation.Binary.PropositionalEquality where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Function.Equality
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.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Binary.PropositionalEquality._→-setoid_
d__'8594''45'setoid__26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> () -> MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d__'8594''45'setoid__26 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44
d__'8594''45'setoid__26 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 = T_Setoid_44
du__'8594''45'setoid__26
du__'8594''45'setoid__26 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du__'8594''45'setoid__26 :: T_Setoid_44
du__'8594''45'setoid__26
  = (T_IndexedSetoid_18 -> T_Setoid_44) -> Any -> T_Setoid_44
forall a b. a -> b
coe
      T_IndexedSetoid_18 -> T_Setoid_44
MAlonzo.Code.Function.Equality.du_'8801''45'setoid_206
      ((T_Setoid_44 -> T_IndexedSetoid_18) -> Any -> Any
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 -> Any
forall a b. a -> b
coe
            T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250))
-- Relation.Binary.PropositionalEquality._≗_
d__'8791'__36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
d__'8791'__36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> (Any -> Any)
-> T_Level_18
d__'8791'__36 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> (Any -> Any)
-> T_Level_18
forall a. a
erased
-- Relation.Binary.PropositionalEquality.:→-to-Π
d_'58''8594''45'to'45'Π_48 ::
  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 ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Function.Equality.T_Π_16
d_'58''8594''45'to'45'Π_48 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IndexedSetoid_18
-> (Any -> Any)
-> T_Π_16
d_'58''8594''45'to'45'Π_48 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IndexedSetoid_18
v4 Any -> Any
v5
  = T_IndexedSetoid_18 -> (Any -> Any) -> T_Π_16
du_'58''8594''45'to'45'Π_48 T_IndexedSetoid_18
v4 Any -> Any
v5
du_'58''8594''45'to'45'Π_48 ::
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Function.Equality.T_Π_16
du_'58''8594''45'to'45'Π_48 :: T_IndexedSetoid_18 -> (Any -> Any) -> T_Π_16
du_'58''8594''45'to'45'Π_48 T_IndexedSetoid_18
v0 Any -> Any
v1
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16)
-> Any -> (Any -> Any -> Any -> Any) -> T_Π_16
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Π_16
MAlonzo.Code.Function.Equality.C_Π'46'constructor_1171 ((Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any
v1)
      (\ Any
v2 Any
v3 Any
v4 -> (T_IndexedSetoid_18 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_IndexedSetoid_18 -> (Any -> Any) -> Any -> Any
du_'46'extendedlambda0_62 (T_IndexedSetoid_18 -> Any
forall a b. a -> b
coe T_IndexedSetoid_18
v0) ((Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any
v1) Any
v2)
-- Relation.Binary.PropositionalEquality._..extendedlambda0
d_'46'extendedlambda0_62 ::
  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 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda0_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IndexedSetoid_18
-> (Any -> Any)
-> Any
-> Any
-> T__'8801'__12
-> Any
d_'46'extendedlambda0_62 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IndexedSetoid_18
v4 Any -> Any
v5 Any
v6 ~Any
v7 ~T__'8801'__12
v8
  = T_IndexedSetoid_18 -> (Any -> Any) -> Any -> Any
du_'46'extendedlambda0_62 T_IndexedSetoid_18
v4 Any -> Any
v5 Any
v6
du_'46'extendedlambda0_62 ::
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_62 :: T_IndexedSetoid_18 -> (Any -> Any) -> Any -> Any
du_'46'extendedlambda0_62 T_IndexedSetoid_18
v0 Any -> Any
v1 Any
v2
  = (T_IsIndexedEquivalence_22 -> Any -> Any -> Any)
-> T_IsIndexedEquivalence_22 -> Any -> Any -> Any
forall a b. a -> b
coe
      T_IsIndexedEquivalence_22 -> Any -> Any -> Any
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))
      Any
v2 ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v1 Any
v2)
-- Relation.Binary.PropositionalEquality.→-to-⟶
d_'8594''45'to'45''10230'_68 ::
  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 ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Function.Equality.T_Π_16
d_'8594''45'to'45''10230'_68 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> (Any -> Any)
-> T_Π_16
d_'8594''45'to'45''10230'_68 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Setoid_44
v4
  = T_Setoid_44 -> (Any -> Any) -> T_Π_16
du_'8594''45'to'45''10230'_68 T_Setoid_44
v4
du_'8594''45'to'45''10230'_68 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Function.Equality.T_Π_16
du_'8594''45'to'45''10230'_68 :: T_Setoid_44 -> (Any -> Any) -> T_Π_16
du_'8594''45'to'45''10230'_68 T_Setoid_44
v0
  = (T_IndexedSetoid_18 -> (Any -> Any) -> T_Π_16)
-> Any -> (Any -> Any) -> T_Π_16
forall a b. a -> b
coe
      T_IndexedSetoid_18 -> (Any -> Any) -> T_Π_16
du_'58''8594''45'to'45'Π_48
      ((T_IsIndexedEquivalence_22 -> T_IndexedSetoid_18) -> Any -> Any
forall a b. a -> b
coe
         T_IsIndexedEquivalence_22 -> T_IndexedSetoid_18
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.C_IndexedSetoid'46'constructor_445
         ((T_IsEquivalence_26 -> T_IsIndexedEquivalence_22) -> Any -> Any
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.du_isIndexedEquivalence_32
            ((T_Setoid_44 -> T_IsEquivalence_26) -> Any -> Any
forall a b. a -> b
coe
               T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> Any
forall a b. a -> b
coe T_Setoid_44
v0))))
-- Relation.Binary.PropositionalEquality.Reveal_·_is_
d_Reveal_'183'_is__86 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_Reveal_'183'_is__86 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_Reveal_'183'_is__86 = C_'91'_'93'_102
-- Relation.Binary.PropositionalEquality.Reveal_·_is_.eq
d_eq_100 ::
  T_Reveal_'183'_is__86 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_eq_100 :: T_Reveal_'183'_is__86 -> T__'8801'__12
d_eq_100 = T_Reveal_'183'_is__86 -> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.inspect
d_inspect_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> T_Reveal_'183'_is__86
d_inspect_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> Any)
-> Any
-> T_Reveal_'183'_is__86
d_inspect_114 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> Any)
-> Any
-> T_Reveal_'183'_is__86
forall a. a
erased
-- Relation.Binary.PropositionalEquality.isPropositional
d_isPropositional_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_isPropositional_120 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_isPropositional_120 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Relation.Binary.PropositionalEquality.naturality
d_naturality_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_naturality_142 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Any
-> Any
-> T__'8801'__12
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_naturality_142 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Any
-> Any
-> T__'8801'__12
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.cong-≡id
d_cong'45''8801'id_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'45''8801'id_160 :: T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_cong'45''8801'id_160 = T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality._.fx≡x
d_fx'8801'x_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_fx'8801'x_172 :: T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_fx'8801'x_172 = T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality._.f²x≡x
d_f'178'x'8801'x_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_f'178'x'8801'x_174 :: T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_f'178'x'8801'x_174 = T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality._.≡-≟-identity
d_'8801''45''8799''45'identity_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8801''45''8799''45'identity_194 :: T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Dec_32)
-> Any
-> Any
-> T__'8801'__12
-> T__'8801'__12
d_'8801''45''8799''45'identity_194 = T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Dec_32)
-> Any
-> Any
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality._.≢-≟-identity
d_'8802''45''8799''45'identity_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny ->
  AgdaAny ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8802''45''8799''45'identity_200 :: T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Dec_32)
-> Any
-> Any
-> (T__'8801'__12 -> T_'8869'_4)
-> T_Σ_14
d_'8802''45''8799''45'identity_200 ~T_Level_18
v0 ~T_Level_18
v1 Any -> Any -> T_Dec_32
v2 Any
v3 Any
v4 ~T__'8801'__12 -> T_'8869'_4
v5
  = (Any -> Any -> T_Dec_32) -> Any -> Any -> T_Σ_14
du_'8802''45''8799''45'identity_200 Any -> Any -> T_Dec_32
v2 Any
v3 Any
v4
du_'8802''45''8799''45'identity_200 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8802''45''8799''45'identity_200 :: (Any -> Any -> T_Dec_32) -> Any -> Any -> T_Σ_14
du_'8802''45''8799''45'identity_200 Any -> Any -> T_Dec_32
v0 Any
v1 Any
v2
  = (T_Dec_32 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
      T_Dec_32 -> T_Σ_14
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_dec'45'no_124
      ((Any -> Any -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_Dec_32
v0 Any
v1 Any
v2)
-- Relation.Binary.PropositionalEquality.Extensionality
d_Extensionality_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> ()
d_Extensionality_204 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_Extensionality_204 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Relation.Binary.PropositionalEquality.extensionality-for-lower-levels
d_extensionality'45'for'45'lower'45'levels_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.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_extensionality'45'for'45'lower'45'levels_206 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (T_Level_18
    -> (Any -> T_Level_18)
    -> (Any -> Any)
    -> (Any -> Any)
    -> (Any -> T__'8801'__12)
    -> T__'8801'__12)
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_extensionality'45'for'45'lower'45'levels_206 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (T_Level_18
    -> (Any -> T_Level_18)
    -> (Any -> Any)
    -> (Any -> Any)
    -> (Any -> T__'8801'__12)
    -> T__'8801'__12)
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.∀-extensionality
d_'8704''45'extensionality_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() ->
   (AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8704''45'extensionality_208 :: T_Level_18
-> T_Level_18
-> (T_Level_18
    -> (Any -> T_Level_18)
    -> (Any -> Any)
    -> (Any -> Any)
    -> (Any -> T__'8801'__12)
    -> T__'8801'__12)
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> T_Level_18)
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_'8704''45'extensionality_208 = T_Level_18
-> T_Level_18
-> (T_Level_18
    -> (Any -> T_Level_18)
    -> (Any -> Any)
    -> (Any -> Any)
    -> (Any -> T__'8801'__12)
    -> T__'8801'__12)
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> T_Level_18)
-> (Any -> T__'8801'__12)
-> T__'8801'__12
forall a. a
erased