{-# 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.Dependent.Bundles 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.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.Dependent.Bundles._._._≈_
d__'8776'__32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_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.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'8776'__32 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Function.Dependent.Bundles._._.Carrier
d_Carrier_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_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.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles.T_IndexedSetoid_18 ->
  ()
d_Carrier_34 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
-> T_Level_18
d_Carrier_34 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_IndexedSetoid_18
-> T_Level_18
forall a. a
erased
-- Function.Dependent.Bundles._.Func
d_Func_42 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_Func_42 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Func_42
  = C_Func'46'constructor_677 (AgdaAny -> AgdaAny)
                              (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Function.Dependent.Bundles._.Func.to
d_to_56 :: T_Func_42 -> AgdaAny -> AgdaAny
d_to_56 :: T_Func_42 -> AgdaAny -> AgdaAny
d_to_56 T_Func_42
v0
  = case T_Func_42 -> T_Func_42
forall a b. a -> b
coe T_Func_42
v0 of
      C_Func'46'constructor_677 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1
      T_Func_42
_                               -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Dependent.Bundles._.Func.cong
d_cong_62 :: T_Func_42 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_62 :: T_Func_42 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_62 T_Func_42
v0
  = case T_Func_42 -> T_Func_42
forall a b. a -> b
coe T_Func_42
v0 of
      C_Func'46'constructor_677 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_Func_42
_                               -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError