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

-- 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))))