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.Relation.Binary.PropositionalEquality.Core where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.Irrelevant 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
  
  -- Relation.Binary.PropositionalEquality.Core._≢_
  d__'8802'__22 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> AgdaAny -> AgdaAny -> ()
  d__'8802'__22 = erased
  -- Relation.Binary.PropositionalEquality.Core._≗_
  d__'8791'__32 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> ()
  d__'8791'__32 = erased
  -- Relation.Binary.PropositionalEquality.Core.cong
  d_cong_54 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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_54 = erased
  -- Relation.Binary.PropositionalEquality.Core.cong′
  d_cong'8242'_62 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_cong'8242'_62 = erased
  -- Relation.Binary.PropositionalEquality.Core.icong
  d_icong_70 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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_icong_70 = erased
  -- Relation.Binary.PropositionalEquality.Core.icong′
  d_icong'8242'_76 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_icong'8242'_76 = erased
  -- Relation.Binary.PropositionalEquality.Core.cong₂
  d_cong'8322'_88 ::
    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 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_cong'8322'_88 = erased
  -- Relation.Binary.PropositionalEquality.Core.cong-app
  d_cong'45'app_104 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_cong'45'app_104 = erased
  -- Relation.Binary.PropositionalEquality.Core.sym
  d_sym_108 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_sym_108 = erased
  -- Relation.Binary.PropositionalEquality.Core.trans
  d_trans_110 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_trans_110 = erased
  -- Relation.Binary.PropositionalEquality.Core.subst
  d_subst_114 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    AgdaAny -> AgdaAny
  d_subst_114 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 = du_subst_114 v7
  du_subst_114 :: AgdaAny -> AgdaAny
  du_subst_114 v0 = coe v0
  -- Relation.Binary.PropositionalEquality.Core.subst₂
  d_subst'8322'_130 ::
    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
  d_subst'8322'_130 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10 ~v11
                    v12
    = du_subst'8322'_130 v12
  du_subst'8322'_130 :: AgdaAny -> AgdaAny
  du_subst'8322'_130 v0 = coe v0
  -- Relation.Binary.PropositionalEquality.Core.resp
  d_resp_136 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    AgdaAny -> AgdaAny
  d_resp_136 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 = du_resp_136 v7
  du_resp_136 :: AgdaAny -> AgdaAny
  du_resp_136 v0 = coe v0
  -- Relation.Binary.PropositionalEquality.Core.respˡ
  d_resp'737'_144 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    AgdaAny -> AgdaAny
  d_resp'737'_144 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8
    = du_resp'737'_144 v8
  du_resp'737'_144 :: AgdaAny -> AgdaAny
  du_resp'737'_144 v0 = coe v0
  -- Relation.Binary.PropositionalEquality.Core.respʳ
  d_resp'691'_152 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    AgdaAny -> AgdaAny
  d_resp'691'_152 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8
    = du_resp'691'_152 v8
  du_resp'691'_152 :: AgdaAny -> AgdaAny
  du_resp'691'_152 v0 = coe v0
  -- Relation.Binary.PropositionalEquality.Core.resp₂
  d_resp'8322'_160 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_resp'8322'_160 ~v0 ~v1 ~v2 ~v3 = du_resp'8322'_160
  du_resp'8322'_160 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_resp'8322'_160
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
        (coe (\ v0 v1 v2 v3 v4 -> v4)) (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.PropositionalEquality.Core.≢-sym
  d_'8802''45'sym_164 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    AgdaAny ->
    (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_'8802''45'sym_164 = erased
  