{-# 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.Function.Indexed.Relation.Binary.Equality where

import Data.Text qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Relation.Binary.Bundles qualified
import MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles qualified
import MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures qualified
import MAlonzo.Code.Relation.Binary.Structures 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

-- Function.Indexed.Relation.Binary.Equality.≡-setoid
d_'8801''45'setoid_18 ::
  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 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_18 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_IndexedSetoid_18
-> T_Setoid_44
d_'8801''45'setoid_18 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_IndexedSetoid_18
v4
  = T_IndexedSetoid_18 -> T_Setoid_44
du_'8801''45'setoid_18 T_IndexedSetoid_18
v4
du_'8801''45'setoid_18 ::
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_'8801''45'setoid_18 :: T_IndexedSetoid_18 -> T_Setoid_44
du_'8801''45'setoid_18 T_IndexedSetoid_18
v0
  = (T_IsEquivalence_26 -> T_Setoid_44) -> Any -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_733
      (((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_26)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
         ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
            (\ 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
forall a b. a -> b
coe Any
v1 Any
v2)))
         ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v1 Any
v2 Any
v3 Any
v4 ->
               (T_IsIndexedEquivalence_22
 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsIndexedEquivalence_22
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                 T_IsIndexedEquivalence_22 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_sym_32
                 (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
v4 Any
v4 (Any -> Any -> Any
forall a b. a -> b
coe Any
v1 Any
v4) (Any -> Any -> Any
forall a b. a -> b
coe Any
v2 Any
v4) (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v4)))
         ((Any -> Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v1 Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 ->
               (T_IsIndexedEquivalence_22
 -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsIndexedEquivalence_22
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                 T_IsIndexedEquivalence_22
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_34
                 (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
v6 Any
v6 Any
v6 (Any -> Any -> Any
forall a b. a -> b
coe Any
v1 Any
v6) (Any -> Any -> Any
forall a b. a -> b
coe Any
v2 Any
v6) (Any -> Any -> Any
forall a b. a -> b
coe Any
v3 Any
v6) (Any -> Any -> Any
forall a b. a -> b
coe Any
v4 Any
v6)
                 (Any -> Any -> Any
forall a b. a -> b
coe Any
v5 Any
v6))))