{-# 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.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Function.Dependent.Bundles
import qualified MAlonzo.Code.Function.Indexed.Relation.Binary.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.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.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