content: {-# 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.Consequences.Propositional where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.Irrelevant qualified
  import MAlonzo.Code.Function.Consequences.Setoid qualified
  import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties 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.Consequences.Propositional.Setoid.contraInjective
  d_contraInjective_16 ::
    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) ->
    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 ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_contraInjective_16 = erased
  -- Function.Consequences.Propositional.Setoid.inverseʳ⇒injective
  d_inverse'691''8658'injective_18 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_inverse'691''8658'injective_18 = erased
  -- Function.Consequences.Propositional.Setoid.inverseʳ⇒strictlyInverseʳ
  d_inverse'691''8658'strictlyInverse'691'_20 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_inverse'691''8658'strictlyInverse'691'_20 = erased
  -- Function.Consequences.Propositional.Setoid.inverseˡ⇒strictlyInverseˡ
  d_inverse'737''8658'strictlyInverse'737'_22 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_inverse'737''8658'strictlyInverse'737'_22 = erased
  -- Function.Consequences.Propositional.Setoid.inverseˡ⇒surjective
  d_inverse'737''8658'surjective_24 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inverse'737''8658'surjective_24 ~v0 ~v1 ~v2 ~v3
    = du_inverse'737''8658'surjective_24
  du_inverse'737''8658'surjective_24 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_inverse'737''8658'surjective_24 v0 v1
    = coe
        MAlonzo.Code.Function.Consequences.Setoid.du_inverse'737''8658'surjective_72
        v1
  -- Function.Consequences.Propositional.Setoid.inverseᵇ⇒bijective
  d_inverse'7495''8658'bijective_26 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inverse'7495''8658'bijective_26 ~v0 ~v1 ~v2 ~v3
    = du_inverse'7495''8658'bijective_26
  du_inverse'7495''8658'bijective_26 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_inverse'7495''8658'bijective_26
    = coe
        MAlonzo.Code.Function.Consequences.Setoid.du_inverse'7495''8658'bijective_80
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Function.Consequences.Propositional.Setoid.surjective⇒strictlySurjective
  d_surjective'8658'strictlySurjective_34 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_surjective'8658'strictlySurjective_34 ~v0 ~v1 ~v2 ~v3
    = du_surjective'8658'strictlySurjective_34
  du_surjective'8658'strictlySurjective_34 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_surjective'8658'strictlySurjective_34 v0
    = coe
        MAlonzo.Code.Function.Consequences.Setoid.du_surjective'8658'strictlySurjective_82
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Function.Consequences.Propositional.strictlySurjective⇒surjective
  d_strictlySurjective'8658'surjective_40 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_strictlySurjective'8658'surjective_40 ~v0 ~v1 ~v2 ~v3 v4
    = du_strictlySurjective'8658'surjective_40 v4
  du_strictlySurjective'8658'surjective_40 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_strictlySurjective'8658'surjective_40 v0
    = coe
        MAlonzo.Code.Function.Consequences.Setoid.du_strictlySurjective'8658'surjective_84
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
        v0 erased
  -- Function.Consequences.Propositional.strictlyInverseˡ⇒inverseˡ
  d_strictlyInverse'737''8658'inverse'737'_44 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_strictlyInverse'737''8658'inverse'737'_44 = erased
  -- Function.Consequences.Propositional.strictlyInverseʳ⇒inverseʳ
  d_strictlyInverse'691''8658'inverse'691'_50 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_strictlyInverse'691''8658'inverse'691'_50 = erased
  