content: {-# 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.Axiom.Extensionality.Heterogeneous where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Relation.Binary.HeterogeneousEquality.Core 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
  
  -- Axiom.Extensionality.Heterogeneous.Extensionality
  d_Extensionality_10 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 -> ()
  d_Extensionality_10 = erased
  -- Axiom.Extensionality.Heterogeneous.≡-ext⇒≅-ext
  d_'8801''45'ext'8658''8773''45'ext_38 ::
    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) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Binary.HeterogeneousEquality.Core.T__'8773'__22) ->
    MAlonzo.Code.Relation.Binary.HeterogeneousEquality.Core.T__'8773'__22
  d_'8801''45'ext'8658''8773''45'ext_38 = erased
  -- Axiom.Extensionality.Heterogeneous._.ext′
  d_ext'8242'_68 ::
    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 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Binary.HeterogeneousEquality.Core.T__'8773'__22) ->
    () ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_ext'8242'_68 = erased
  