{-# 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.Injection 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.Function.Equality
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Function.Injection.Injective
d_Injective_16 ::
  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.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Equality.T_Π_16 -> ()
d_Injective_16 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Level_18
d_Injective_16 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Π_16
-> T_Level_18
forall a. a
erased
-- Function.Injection.Injection
d_Injection_88 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_Injection_88 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Injection_88
  = C_Injection'46'constructor_3057 MAlonzo.Code.Function.Equality.T_Π_16
                                    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Function.Injection.Injection.to
d_to_106 :: T_Injection_88 -> MAlonzo.Code.Function.Equality.T_Π_16
d_to_106 :: T_Injection_88 -> T_Π_16
d_to_106 T_Injection_88
v0
  = case T_Injection_88 -> T_Injection_88
forall a b. a -> b
coe T_Injection_88
v0 of
      C_Injection'46'constructor_3057 T_Π_16
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> T_Π_16 -> T_Π_16
forall a b. a -> b
coe T_Π_16
v1
      T_Injection_88
_ -> T_Π_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Injection.Injection.injective
d_injective_108 ::
  T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_108 :: T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_108 T_Injection_88
v0
  = case T_Injection_88 -> T_Injection_88
forall a b. a -> b
coe T_Injection_88
v0 of
      C_Injection'46'constructor_3057 T_Π_16
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_Injection_88
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Function.Injection.Injection._._⟨$⟩_
d__'10216''36''10217'__112 :: T_Injection_88 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__112 :: T_Injection_88 -> AgdaAny -> AgdaAny
d__'10216''36''10217'__112 T_Injection_88
v0
  = (T_Π_16 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
      ((T_Injection_88 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_88 -> T_Π_16
d_to_106 (T_Injection_88 -> AgdaAny
forall a b. a -> b
coe T_Injection_88
v0))
-- Function.Injection.Injection._.cong
d_cong_114 ::
  T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_114 :: T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_cong_114 T_Injection_88
v0
  = (T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Π_16 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d_cong_40 ((T_Injection_88 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_88 -> T_Π_16
d_to_106 (T_Injection_88 -> AgdaAny
forall a b. a -> b
coe T_Injection_88
v0))
-- Function.Injection._↣_
d__'8611'__120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> () -> ()
d__'8611'__120 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18
d__'8611'__120 = T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Function.Injection.injection
d_injection_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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) ->
  T_Injection_88
d_injection_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> T_Injection_88
d_injection_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
v5 = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> T_Injection_88
du_injection_140 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
v5
du_injection_140 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  T_Injection_88
du_injection_140 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> T_Injection_88
du_injection_140 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
v1
  = (T_Π_16
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88)
-> AgdaAny -> AgdaAny -> T_Injection_88
forall a b. a -> b
coe
      T_Π_16
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88
C_Injection'46'constructor_3057
      ((T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Π_16
MAlonzo.Code.Relation.Binary.PropositionalEquality.du_'8594''45'to'45''10230'_68
         ((T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
            (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
               AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased))
         AgdaAny -> AgdaAny
v0)
      ((AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
v1)
-- Function.Injection.id
d_id_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 -> T_Injection_88
d_id_152 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Injection_88
d_id_152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Injection_88
du_id_152
du_id_152 :: T_Injection_88
du_id_152 :: T_Injection_88
du_id_152
  = (T_Π_16
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88)
-> AgdaAny -> AgdaAny -> T_Injection_88
forall a b. a -> b
coe
      T_Π_16
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88
C_Injection'46'constructor_3057
      (T_Π_16 -> AgdaAny
forall a b. a -> b
coe T_Π_16
MAlonzo.Code.Function.Equality.du_id_62)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2))
-- Function.Injection._∘_
d__'8728'__172 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  T_Injection_88 -> T_Injection_88 -> T_Injection_88
d__'8728'__172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> T_Injection_88
-> T_Injection_88
d__'8728'__172 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Setoid_44
v6 ~T_Setoid_44
v7 ~T_Setoid_44
v8 T_Injection_88
v9 T_Injection_88
v10
  = T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8728'__172 T_Injection_88
v9 T_Injection_88
v10
du__'8728'__172 ::
  T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8728'__172 :: T_Injection_88 -> T_Injection_88 -> T_Injection_88
du__'8728'__172 T_Injection_88
v0 T_Injection_88
v1
  = (T_Π_16
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88)
-> AgdaAny -> AgdaAny -> T_Injection_88
forall a b. a -> b
coe
      T_Π_16
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Injection_88
C_Injection'46'constructor_3057
      ((T_Π_16 -> T_Π_16 -> T_Π_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Π_16 -> T_Π_16 -> T_Π_16
MAlonzo.Code.Function.Equality.du__'8728'__82
         ((T_Injection_88 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_88 -> T_Π_16
d_to_106 (T_Injection_88 -> AgdaAny
forall a b. a -> b
coe T_Injection_88
v0)) ((T_Injection_88 -> T_Π_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Injection_88 -> T_Π_16
d_to_106 (T_Injection_88 -> AgdaAny
forall a b. a -> b
coe T_Injection_88
v1)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            (T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_108 T_Injection_88
v1 AgdaAny
v2 AgdaAny
v3
              ((T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_injective_108 T_Injection_88
v0
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                    (T_Injection_88 -> T_Π_16
d_to_106 (T_Injection_88 -> T_Injection_88
forall a b. a -> b
coe T_Injection_88
v1)) AgdaAny
v2)
                 ((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
                    (T_Injection_88 -> T_Π_16
d_to_106 (T_Injection_88 -> T_Injection_88
forall a b. a -> b
coe T_Injection_88
v1)) AgdaAny
v3)
                 AgdaAny
v4)))