{-# 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 Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Equality qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Data.Irrelevant qualified
import MAlonzo.Code.Function.Dependent.Bundles qualified
import MAlonzo.Code.Function.Indexed.Relation.Binary.Equality qualified
import MAlonzo.Code.Relation.Binary.Bundles qualified
import MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles qualified
import MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Construct.Trivial qualified
import MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures qualified
import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
import MAlonzo.Code.Relation.Nullary.Decidable.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

-- 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.Indexed.Relation.Binary.Equality.du_'8801''45'setoid_18
      ((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_106
         (T_Setoid_44 -> Any
forall a b. a -> b
coe
            T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402))
-- Relation.Binary.PropositionalEquality.:→-to-Π
d_'58''8594''45'to'45'Π_38 ::
  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.Dependent.Bundles.T_Func_42
d_'58''8594''45'to'45'Π_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IndexedSetoid_18
-> (Any -> Any)
-> T_Func_42
d_'58''8594''45'to'45'Π_38 ~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_Func_42
du_'58''8594''45'to'45'Π_38 T_IndexedSetoid_18
v4 Any -> Any
v5
du_'58''8594''45'to'45'Π_38 ::
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Dependent.Bundles.T_Func_42
du_'58''8594''45'to'45'Π_38 :: T_IndexedSetoid_18 -> (Any -> Any) -> T_Func_42
du_'58''8594''45'to'45'Π_38 T_IndexedSetoid_18
v0 Any -> Any
v1
  = ((Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_42)
-> Any -> (Any -> Any -> Any -> Any) -> T_Func_42
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> Any -> Any) -> T_Func_42
MAlonzo.Code.Function.Dependent.Bundles.C_Func'46'constructor_677
      ((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_44 (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_44 ::
  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_44 :: 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_44 ~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_44 T_IndexedSetoid_18
v4 Any -> Any
v5 Any
v6
du_'46'extendedlambda0_44 ::
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_44 :: T_IndexedSetoid_18 -> (Any -> Any) -> Any -> Any
du_'46'extendedlambda0_44 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'_50 ::
  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.Dependent.Bundles.T_Func_42
d_'8594''45'to'45''10230'_50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> (Any -> Any)
-> T_Func_42
d_'8594''45'to'45''10230'_50 ~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_Func_42
du_'8594''45'to'45''10230'_50 T_Setoid_44
v4
du_'8594''45'to'45''10230'_50 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Function.Dependent.Bundles.T_Func_42
du_'8594''45'to'45''10230'_50 :: T_Setoid_44 -> (Any -> Any) -> T_Func_42
du_'8594''45'to'45''10230'_50 T_Setoid_44
v0
  = (T_IndexedSetoid_18 -> (Any -> Any) -> T_Func_42)
-> Any -> (Any -> Any) -> T_Func_42
forall a b. a -> b
coe
      T_IndexedSetoid_18 -> (Any -> Any) -> T_Func_42
du_'58''8594''45'to'45'Π_38
      ((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.naturality
d_naturality_66 ::
  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_66 :: 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_66 = 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_84 ::
  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_84 :: T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_cong'45''8801'id_84 = 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_96 ::
  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_96 :: T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_fx'8801'x_96 = 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_98 ::
  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_98 :: T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Any
-> (Any -> T__'8801'__12)
-> T__'8801'__12
d_f'178'x'8801'x_98 = 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_118 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8801''45''8799''45'identity_118 :: T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Dec_20)
-> Any
-> Any
-> T__'8801'__12
-> T__'8801'__12
d_'8801''45''8799''45'identity_118 = T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Dec_20)
-> Any
-> Any
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality._.≢-≟-identity
d_'8802''45''8799''45'identity_124 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  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
d_'8802''45''8799''45'identity_124 :: T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Dec_20)
-> Any
-> Any
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T__'8801'__12
d_'8802''45''8799''45'identity_124 = T_Level_18
-> T_Level_18
-> (Any -> Any -> T_Dec_20)
-> Any
-> Any
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Reveal_·_is_
d_Reveal_'183'_is__142 :: p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_Reveal_'183'_is__142 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
data T_Reveal_'183'_is__142 = C_'91'_'93'_158
-- Relation.Binary.PropositionalEquality.Reveal_·_is_.eq
d_eq_156 ::
  T_Reveal_'183'_is__142 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_eq_156 :: T_Reveal_'183'_is__142 -> T__'8801'__12
d_eq_156 = T_Reveal_'183'_is__142 -> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.inspect
d_inspect_170 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> T_Reveal_'183'_is__142
d_inspect_170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> Any)
-> Any
-> T_Reveal_'183'_is__142
d_inspect_170 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> T_Level_18)
-> (Any -> Any)
-> Any
-> T_Reveal_'183'_is__142
forall a. a
erased
-- Relation.Binary.PropositionalEquality.isPropositional
d_isPropositional_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_isPropositional_176 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_isPropositional_176 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased