------------------------------------------------------------------------
-- Definitions related to type and usage restrictions for the Zero-one
-- mode instance
------------------------------------------------------------------------

import Graded.Modality
import Graded.Mode.Instances.Zero-one.Variant

module Graded.Restrictions.Zero-one
  {a} {M : Set a}
  (open Graded.Modality M)
  (𝕄 : Modality)
  (open Graded.Mode.Instances.Zero-one.Variant 𝕄)
  (variant : Mode-variant)
  where

open Modality 𝕄

open import Tools.Bool
open import Tools.Empty
open import Tools.Function
open import Tools.Level
open import Tools.Product as Ξ£
open import Tools.PropositionalEquality
open import Tools.Relation as Dec
open import Tools.Sum
open import Tools.Unit

open import Graded.Modality.Properties 𝕄
open import Graded.Mode.Instances.Zero-one variant hiding (_β‰Ÿ_)
import Graded.Usage.Decidable.Assumptions as UD
open import Graded.Usage.Erased-matches
open import Graded.Usage.Restrictions 𝕄 Zero-one-isMode
open import Graded.Usage.Restrictions.Natrec 𝕄
open import Graded.Usage.Restrictions.Omega 𝕄

import Definition.Typechecking.Decidable.Assumptions as TD
open import Definition.Typed.Restrictions 𝕄
open import Definition.Typed.Variant
open import Definition.Untyped.NotParametrised
open import Definition.Untyped.Properties.NotParametrised

open import Graded.Restrictions 𝕄 Zero-one-isMode public
  hiding (nr-available-UR; no-usage-restrictions;
          No-erased-matches; No-erased-matchesβ€²)
import Graded.Restrictions 𝕄 Zero-one-isMode as GR

private variable
  TR    : Type-restrictions
  UR    : Usage-restrictions
  b₁ bβ‚‚ : Bool
  ok    : T _
  s     : Strength
  nm    : Natrec-mode

------------------------------------------------------------------------
-- A lemma used below

opaque

  -- If a reflexive property holds for modes πŸ™α΅ and 𝟘ᡐ? then it holds
  -- for all modes m ≀ᡐ mβ€²

  πŸ™α΅πŸ˜α΅β†’β‰€α΅ :
    (P : (m mβ€² : Mode) β†’ Set) β†’
    (βˆ€ {ok} β†’ P πŸ™α΅ 𝟘ᡐ[ ok ]) β†’
    (βˆ€ {m} β†’ P m m) β†’
    βˆ€ {m mβ€²} β†’ m ≀ᡐ mβ€² β†’ P m mβ€²
  πŸ™α΅πŸ˜α΅β†’β‰€α΅ P ok₁₀ okα΅£ {(𝟘ᡐ)} {(𝟘ᡐ)} m≀ᡐmβ€² = subst (P _) 𝟘ᡐ-cong okα΅£
  πŸ™α΅πŸ˜α΅β†’β‰€α΅ P ok₁₀ okα΅£ {(𝟘ᡐ)} {(πŸ™α΅)} ()
  πŸ™α΅πŸ˜α΅β†’β‰€α΅ P ok₁₀ okα΅£ {(πŸ™α΅)} {(𝟘ᡐ[ ok ])} m≀ᡐmβ€² = subst (P _) 𝟘ᡐ-cong (ok₁₀ {ok})
  πŸ™α΅πŸ˜α΅β†’β‰€α΅ P ok₁₀ okα΅£ {(πŸ™α΅)} {(πŸ™α΅)} m≀ᡐmβ€² = okα΅£

------------------------------------------------------------------------
-- Functions that construct Usage-restrictions

-- No restrictions for prodrec, unitrec or emptyrec, all erased
-- matches are allowed for J andΒ K, the natrec mode can be anything,
-- the higher quotient constructors are allowed exactly if the mode
-- structure is non-trivial, Id-erased is inhabited if the first
-- boolean is true, starΛ’ is treated as a sink if the second boolean
-- is true, and Qrec-motive-erased is inhabited if the third boolean
-- is true.

no-usage-restrictions :
  (nm : Natrec-mode) β†’
  Bool β†’ Bool β†’ Bool β†’ Usage-restrictions
no-usage-restrictions nm =
  GR.no-usage-restrictions nm
    (Ξ» { ⦃ (Nr) ⦄ β†’ Zero-one-supports-nr ⦃ Natrec-mode-Has-nr Nr ⦄ })

-- A function used to define not-all-erased-matches-JK.

not-all-for-πŸ™α΅ : (Mode β†’ Erased-matches) β†’ Mode β†’ Erased-matches
not-all-for-πŸ™α΅ f 𝟘ᡐ = f 𝟘ᡐ
not-all-for-πŸ™α΅ f πŸ™α΅ with f πŸ™α΅
… | all = some
… | em  = em

-- The function adds the restriction that, for the modeΒ πŸ™α΅, "all"
-- erased matches are not allowed for J andΒ K.

not-all-erased-matches-JK :
  ⦃ ok : Has-omega 𝕄 ⦄ β†’ Usage-restrictions β†’ Usage-restrictions
not-all-erased-matches-JK UR = record UR
  { usage-rules-with-Ο‰ = with-Ο‰
  ; erased-matches-for-JK = Ξ» jk m β†’ not-all-for-πŸ™α΅ (erased-matches-for-JK jk) m
  ; erased-matches-for-JK-≀ᡉᡐ =
      πŸ™α΅πŸ˜α΅β†’β‰€α΅
        (Ξ» m mβ€² β†’ not-all-for-πŸ™α΅ (erased-matches-for-JK _) m ≀ᡉᡐ not-all-for-πŸ™α΅ (erased-matches-for-JK _) mβ€²)
        (not-all-for-πŸ™α΅-≀ᡉᡐ (erased-matches-for-JK _) (erased-matches-for-JK-≀ᡉᡐ πŸ™α΅β‰€))
        ≀ᡉᡐ-reflexive
  ; erased-matches-for-JK-supports-Ο‰ = Ξ» _ β†’ with-Ο‰
  }
  where
  open Usage-restrictions UR

  opaque

    not-all-for-πŸ™α΅-≀ᡉᡐ :
      (f : Mode β†’ Erased-matches) β†’
      f πŸ™α΅ ≀ᡉᡐ f 𝟘ᡐ[ ok ] β†’
      not-all-for-πŸ™α΅ f πŸ™α΅ ≀ᡉᡐ not-all-for-πŸ™α΅ f 𝟘ᡐ[ ok ]
    not-all-for-πŸ™α΅-≀ᡉᡐ f f-≀ᡉᡐ with f πŸ™α΅
    … | all  = ≀ᡉᡐ-transitive _ f-≀ᡉᡐ
    … | some = f-≀ᡉᡐ
    … | none = f-≀ᡉᡐ

-- The function adds the restriction that certain erased matches are
-- not allowed for the modeΒ πŸ™α΅. No restriction is added for emptyrec
-- or unitrec. For prodrec the added restriction only applies to
-- non-trivial modalities.

only-some-erased-matches :
  ⦃ ok : Has-omega 𝕄 ⦄ β†’ Usage-restrictions β†’ Usage-restrictions
only-some-erased-matches UR = record UR
  { Prodrec-allowed = Ξ» m r p q β†’
      Prodrec-allowed m r p q Γ—
      (m ≑ πŸ™α΅ β†’ Β¬ Trivial β†’ r β‰’ 𝟘)
  ; Prodrec-allowed-upwards-closed = Ξ» (ok , rβ‰’πŸ˜) m≀mβ€² β†’
      Prodrec-allowed-upwards-closed ok m≀mβ€² , Ξ» { refl β†’ rβ‰’πŸ˜ (≀ᡐ-πŸ™α΅β†’ m≀mβ€²) }
  ; usage-rules-with-Ο‰ = with-Ο‰
  ; erased-matches-for-JK =
      Ξ» jk β†’ f (erased-matches-for-JK jk 𝟘ᡐ?)
  ; erased-matches-for-JK-≀ᡉᡐ =
      πŸ™α΅πŸ˜α΅β†’β‰€α΅ (Ξ» m mβ€² β†’ f _ m ≀ᡉᡐ f _ mβ€²) _ ≀ᡉᡐ-reflexive
  ; erased-matches-for-JK-supports-Ο‰ = Ξ» _ β†’ with-Ο‰
  }
  where
  open Usage-restrictions UR
  f : Erased-matches β†’ Mode β†’ Erased-matches
  f _  πŸ™α΅ = none
  f em 𝟘ᡐ = em

-- The function adds the restriction that certain erased matches are
-- not allowed for the modeΒ πŸ™α΅. No restriction is added for emptyrec.
-- For prodrec and unitrec the added restriction only applies to
-- non-trivial modalities, and for unitrec the added restriction only
-- applies if Ξ·-equality is not allowed for weak unit types.

no-erased-matches-UR :
  ⦃ ok : Has-omega 𝕄 ⦄ β†’
  Type-restrictions β†’ Usage-restrictions β†’ Usage-restrictions
no-erased-matches-UR TR UR = record (only-some-erased-matches UR)
  { Unitrec-allowed = Ξ» m p q β†’
      Unitrec-allowed m p q Γ—
      (m ≑ πŸ™α΅ β†’ Β¬ Trivial β†’ p ≑ 𝟘 β†’ UnitΚ·-Ξ·)
  ; Unitrec-allowed-upwards-closed = Ξ» (ok , Ξ·) m≀mβ€² β†’
      Unitrec-allowed-upwards-closed ok m≀mβ€² , Ξ» { refl β†’ Ξ· (≀ᡐ-πŸ™α΅β†’ m≀mβ€²) }
  }
  where
  open Type-restrictions TR
  open Usage-restrictions UR

-- The function updates the usage restrictions to use the usage rule
-- natrecβ‚˜ for natrec using a given nr function.

nr-available-UR :
  (has-nr : Has-nr 𝕄) β†’
  Usage-restrictions β†’ Usage-restrictions
nr-available-UR has-nr UR = record UR
  { natrec-mode      = Nr ⦃ has-nr ⦄
  ; mode-supports-nr = Ξ» { ⦃ (Nr) ⦄ β†’ Zero-one-supports-nr}
  }

-- A function used to define []-cong-UR.

none-for-πŸ™α΅ : (Mode β†’ Erased-matches) β†’ Mode β†’ Erased-matches
none-for-πŸ™α΅ f πŸ™α΅ = none
none-for-πŸ™α΅ f 𝟘ᡐ = f 𝟘ᡐ

-- The function enables support for []-cong (if the modality is
-- non-trivial), but disables support for erased matches for J (when
-- the mode is πŸ™α΅).

[]-cong-UR : ⦃ ok : Has-omega 𝕄 ⦄ β†’ Usage-restrictions β†’ Usage-restrictions
[]-cong-UR ⦃ ok ⦄ UR = record UR
  { []-cong-allowed-mode     = Ξ» m s β†’ []-cong-allowed-mode m s ⊎
                                     Β¬ Trivial
  ; []-cong-allowed-mode-upwards-closed = Ξ» where
      (inj₁ ok) m≀mβ€² β†’ inj₁ ([]-cong-allowed-mode-upwards-closed ok m≀mβ€²)
      (injβ‚‚ πŸ™β‰’πŸ˜) _   β†’ injβ‚‚ πŸ™β‰’πŸ˜
  ; usage-rules-with-Ο‰ = with-Ο‰ ⦃ ok ⦄
  ; erased-matches-for-JK = Ξ» where
      J m β†’ none-for-πŸ™α΅ erased-matches-for-J m
      K m β†’ erased-matches-for-JK K m
  ; erased-matches-for-JK-≀ᡉᡐ = Ξ» where
      {jk = J} m≀mβ€² β†’
        πŸ™α΅πŸ˜α΅β†’β‰€α΅
          (Ξ» m₁ mβ‚‚ β†’
             none-for-πŸ™α΅ erased-matches-for-J m₁ ≀ᡉᡐ
             none-for-πŸ™α΅ erased-matches-for-J mβ‚‚)
          _ ≀ᡉᡐ-reflexive m≀mβ€²
      {jk = K} m≀mβ€² β†’ erased-matches-for-JK-≀ᡉᡐ m≀mβ€²
  ; erased-matches-for-JK-supports-Ο‰ = Ξ» _ β†’ with-Ο‰
  }
  where
  open Usage-restrictions UR

-- A function used to define no-[]-cong-UR.

at-least-some : (Mode β†’ Erased-matches) β†’ Mode β†’ Erased-matches
at-least-some f m = case f m of Ξ» where
  none β†’ some
  em   β†’ em

-- The function no-[]-cong-UR disables support for []-cong but enables
-- "some" erased matches for J.

no-[]-cong-UR : Usage-restrictions β†’ Usage-restrictions
no-[]-cong-UR UR = record UR
  { []-cong-allowed-mode                = Ξ» _ _ β†’ Lift _ βŠ₯
  ; []-cong-allowed-mode-upwards-closed = Ξ» ()
  ; erased-matches-for-JK    = Ξ» where
      J β†’ at-least-some erased-matches-for-J
      K β†’ erased-matches-for-K
  ; erased-matches-for-JK-≀ᡉᡐ = Ξ» where
      {jk = J} β†’ πŸ™α΅πŸ˜α΅β†’β‰€α΅ (Ξ» m mβ€² β†’ at-least-some erased-matches-for-J m ≀ᡉᡐ at-least-some erased-matches-for-J mβ€²)
        at-least-some-≀ᡉᡐ ≀ᡉᡐ-reflexive
      {jk = K} β†’ erased-matches-for-K-≀ᡉᡐ
  ; erased-matches-for-JK-supports-Ο‰ = Ξ» where
      {jk = J} ≀some β†’ erased-matches-for-JK-supports-Ο‰
        (≀ᡉᡐ-transitive (some-≀ᡉᡐ-at-least-some (erased-matches-for-JK J) _) ≀some)
      {jk = K} ≀some β†’ erased-matches-for-JK-supports-Ο‰ ≀some
  }
  where
  open Usage-restrictions UR

  some-≀ᡉᡐ-at-least-some :
    (f : Mode β†’ Erased-matches) (m : Mode) β†’
    f m ≀ᡉᡐ at-least-some f m
  some-≀ᡉᡐ-at-least-some f m with f m
  ... | none       = _
  ... | not-none x = ≀ᡉᡐ-reflexive

  at-least-some-≀ᡉᡐ :
    at-least-some erased-matches-for-J πŸ™α΅ ≀ᡉᡐ
    at-least-some erased-matches-for-J 𝟘ᡐ[ ok ]
  at-least-some-≀ᡉᡐ {ok}
    with erased-matches-for-J πŸ™α΅
       | erased-matches-for-J 𝟘ᡐ[ ok ]
       | erased-matches-for-J-≀ᡉᡐ {m = πŸ™α΅} {mβ€² = 𝟘ᡐ[ ok ]} πŸ™α΅β‰€
  … | none       | none       | _  = _
  … | none       | some       | _  = _
  … | none       | all        | _  = _
  … | all        | none       | ()
  … | some       | none       | ()
  … | not-none _ | not-none _ | r  = r

------------------------------------------------------------------------
-- Only-some-erased-matches

-- The property of not allowing certain erased matches:
-- * Erased matches are allowed for emptyrec and unitrec.
-- * "Erased" matches are allowed for trivial modalities.
-- * Erased matches are allowed when the mode is notΒ πŸ™α΅, except for
--   []-cong.

Only-some-erased-matches :
  Type-restrictions β†’ Usage-restrictions β†’ Set a
Only-some-erased-matches TR UR =
  Β¬ Trivial β†’
  (βˆ€ {r p q} β†’ Prodrec-allowed πŸ™α΅ r p q β†’ r β‰’ 𝟘) Γ—
  (βˆ€ {s} β†’ Β¬ ([]-cong-allowed s)) Γ—
  erased-matches-for-J πŸ™α΅ ≑ none Γ—
  erased-matches-for-K πŸ™α΅ ≑ none
  where
  open Type-restrictions TR
  open Usage-restrictions UR

opaque

  -- Certain restrictions obtained from no-erased-matches-TR and
  -- only-some-erased-matches satisfy Only-some-erased-matches.

  Only-some-erased-matches-only-some-erased-matches :
    ⦃ ok : Has-omega 𝕄 ⦄ β†’
    βˆ€ TR UR β†’
    Only-some-erased-matches
      (no-erased-matches-TR 𝕀 (no-erased-matches-TR 𝕨 TR))
      (only-some-erased-matches UR)
  Only-some-erased-matches-only-some-erased-matches _ _ πŸ™β‰’πŸ˜ =
      (Ξ» x β†’ x refl πŸ™β‰’πŸ˜) βˆ˜β†’ projβ‚‚
    , (Ξ» where
         {s = 𝕀} β†’ (_$ refl) βˆ˜β†’ projβ‚‚
         {s = 𝕨} β†’ (_$ refl) βˆ˜β†’ projβ‚‚ βˆ˜β†’ proj₁)
    , refl
    , refl

------------------------------------------------------------------------
-- No-erased-matches

-- The property of not allowing (certain) erased matches:
-- * Erased matches are allowed for emptyrec.
-- * "Erased" matches are allowed for unitrec if Ξ·-equality is allowed
--   for weak unit types.
-- * "Erased" matches are allowed for trivial modalities.
-- * Erased matches are allowed when the mode is notΒ πŸ™α΅, except for
--   []-cong. (Note that a variant of []-cong that works when the mode
--   is not πŸ™α΅ can be defined without the use of []-cong, see
--   Graded.Has-box-cong.Definable.J.β–Έ[]-cong-J-𝟘ᡐ.)

No-erased-matches : Type-restrictions β†’ Usage-restrictions β†’ Set a
No-erased-matches TR UR =
  Β¬ Trivial β†’
  (βˆ€ {r p q} β†’ Prodrec-allowed πŸ™α΅ r p q β†’ r β‰’ 𝟘) Γ—
  (βˆ€ {p q}   β†’ Unitrec-allowed πŸ™α΅ p q   β†’ p ≑ 𝟘 β†’ UnitΚ·-Ξ·) Γ—
  (βˆ€ {s} β†’ Β¬ ([]-cong-allowed s)) Γ—
  erased-matches-for-J πŸ™α΅ ≑ none Γ—
  erased-matches-for-K πŸ™α΅ ≑ none
  where
  open Type-restrictions TR
  open Usage-restrictions UR

-- Certain restrictions obtained from no-erased-matches-TR and
-- no-erased-matches-UR satisfy No-erased-matches.

No-erased-matches-no-erased-matches :
  ⦃ ok : Has-omega 𝕄 ⦄ β†’
  βˆ€ TR UR β†’
  let TRβ€² = no-erased-matches-TR 𝕀 (no-erased-matches-TR 𝕨 TR) in
  No-erased-matches TRβ€² (no-erased-matches-UR TRβ€² UR)
No-erased-matches-no-erased-matches TR UR πŸ™β‰’πŸ˜ =
  case Only-some-erased-matches-only-some-erased-matches TR UR πŸ™β‰’πŸ˜ of Ξ»
    (pr , rest) β†’
    (Ξ» {_ _ _} β†’ pr)
  , (Ξ» {_ _} β†’ (Ξ» x β†’ x refl πŸ™β‰’πŸ˜) βˆ˜β†’ projβ‚‚)
  , rest

opaque

  -- If UnitΚ·-Ξ· holds for TR, then Only-some-erased-matchesΒ TRΒ UR
  -- implies No-erased-matchesΒ TRΒ UR.

  Only-some-erased-matches→No-erased-matches :
    βˆ€ TR UR β†’
    Type-restrictions.UnitΚ·-Ξ· TR β†’
    Only-some-erased-matches TR UR β†’ No-erased-matches TR UR
  Only-some-erased-matches→No-erased-matches _ _ η =
    Ξ£.map idαΆ  ((Ξ» {_ _} _ _ β†’ Ξ·) ,_) βˆ˜β†’_

-- An alternative to No-erased-matches that refers to
-- Type-variant instead of Type-restrictions

No-erased-matchesβ€² : Type-variant a β†’ Usage-restrictions β†’ Set a
No-erased-matchesβ€² TV UR =
  Β¬ Trivial β†’
  (βˆ€ {r p q} β†’ Prodrec-allowed πŸ™α΅ r p q β†’ r β‰’ 𝟘) Γ—
  (βˆ€ {p q}   β†’ Unitrec-allowed πŸ™α΅ p q   β†’ p ≑ 𝟘 β†’ UnitΚ·-Ξ·) Γ—
  (βˆ€ {s} β†’ Β¬ ([]-cong-allowed-mode s πŸ™α΅)) Γ—
  erased-matches-for-J πŸ™α΅ ≑ none Γ—
  erased-matches-for-K πŸ™α΅ ≑ none
  where
  open Type-variant TV
  open Usage-restrictions UR

------------------------------------------------------------------------
-- Some lemmas related to UD.Assumptions

opaque

  -- If grade equality is decidable and the modality supports usage
  -- inference for a given natrec-mode nm, UD.Assumptions holds for
  -- no-usage-restrictionsΒ nmΒ b₁ falseΒ bβ‚‚.

  Assumptions-no-usage-restrictions :
    ⦃ ok : Natrec-mode-supports-usage-inference nm ⦄ β†’
    Decidable (_≑_ {A = M}) β†’
    UD.Assumptions (no-usage-restrictions nm b₁ false bβ‚‚)
  Assumptions-no-usage-restrictions dec = Ξ» where
      ._β‰Ÿ_                                   β†’ dec
      .Prodrec-allowed? _ _ _ _              β†’ yes _
      .Unitrec-allowed? _ _ _                β†’ yes _
      .Emptyrec-allowed? _ _                 β†’ yes _
      .[]-cong-allowed-mode? _ _             β†’ yes _
      .no-sink-or-β‰€πŸ˜                         β†’ inj₁ idαΆ 
      .Quotient-terms-allowed?               β†’ yes _
      .Higher-quotient-constructors-allowed? β†’
        Lift? (Resize-Dec (Β¬? trivialᡐ?) .projβ‚‚ .projβ‚‚)
    where
    open UD.Assumptions

opaque

  -- The function not-all-erased-matches-JK preserves UD.Assumptions.

  Assumptions-not-all-erased-matches-JK :
    ⦃ ok : Has-omega 𝕄 ⦄ β†’
    UD.Assumptions UR β†’ UD.Assumptions (not-all-erased-matches-JK UR)
  Assumptions-not-all-erased-matches-JK as = Ξ» where
      ._β‰Ÿ_                     β†’ A._β‰Ÿ_
      .Prodrec-allowed?        β†’ A.Prodrec-allowed?
      .Unitrec-allowed?        β†’ A.Unitrec-allowed?
      .Emptyrec-allowed?       β†’ A.Emptyrec-allowed?
      .[]-cong-allowed-mode?   β†’ A.[]-cong-allowed-mode?
      .no-sink-or-β‰€πŸ˜           β†’ A.no-sink-or-β‰€πŸ˜
      .Quotient-terms-allowed? β†’
        A.Quotient-terms-allowed?
      .Higher-quotient-constructors-allowed? β†’
        A.Higher-quotient-constructors-allowed?
    where
    module A = UD.Assumptions as
    open UD.Assumptions

opaque

  -- The function only-some-erased-matches preserves UD.Assumptions.

  Assumptions-only-some-erased-matches :
    ⦃ ok : Has-omega 𝕄 ⦄ β†’
    UD.Assumptions UR β†’ UD.Assumptions (only-some-erased-matches UR)
  Assumptions-only-some-erased-matches as = Ξ» where
      ._β‰Ÿ_                      β†’ A._β‰Ÿ_
      .Prodrec-allowed? m r p q β†’ A.Prodrec-allowed? m r p q
                                   Γ—-dec
                                 Dec.map (Ξ» β‰‘πŸ™ β†’ trans (sym (⌞⌜⌝⌟ _)) (trans (⌞⌟-cong β‰‘πŸ™) βŒžπŸ™βŒŸ))
                                   (Ξ» { refl β†’ βŒœπŸ™α΅βŒ}) (⌜ m ⌝ A.β‰Ÿ πŸ™)
                                   β†’-dec
                                 Β¬? trivial?
                                   β†’-dec
                                 Β¬? (r A.β‰Ÿ 𝟘)
      .Unitrec-allowed?         β†’ A.Unitrec-allowed?
      .Emptyrec-allowed?        β†’ A.Emptyrec-allowed?
      .[]-cong-allowed-mode?    β†’ A.[]-cong-allowed-mode?
      .no-sink-or-β‰€πŸ˜            β†’ A.no-sink-or-β‰€πŸ˜
      .Quotient-terms-allowed?  β†’
        A.Quotient-terms-allowed?
      .Higher-quotient-constructors-allowed? β†’
        A.Higher-quotient-constructors-allowed?
    where
    module A = UD.Assumptions as
    open UD.Assumptions

opaque

  -- The function no-erased-matches-URΒ TR preserves UD.Assumptions.

  Assumptions-no-erased-matches-UR :
    ⦃ ok : Has-omega 𝕄 ⦄ β†’
    βˆ€ TR β†’ UD.Assumptions UR β†’
    UD.Assumptions (no-erased-matches-UR TR UR)
  Assumptions-no-erased-matches-UR TR as = Ξ» where
      ._β‰Ÿ_                     β†’ A._β‰Ÿ_
      .Prodrec-allowed?        β†’ A.Prodrec-allowed?
      .Unitrec-allowed? m p q  β†’ A.Unitrec-allowed? m p q
                                   Γ—-dec
                                 (Dec.map
                                    (Ξ» β‰‘πŸ™ β†’
                                       trans (sym (⌞⌜⌝⌟ _)) $
                                       trans (⌞⌟-cong β‰‘πŸ™) βŒžπŸ™βŒŸ)
                                    (Ξ» { refl β†’ βŒœπŸ™α΅βŒ}) (⌜ m ⌝ A.β‰Ÿ πŸ™)
                                    β†’-dec
                                  Β¬? trivial?
                                    β†’-dec
                                  p A.β‰Ÿ 𝟘
                                    β†’-dec
                                  UnitΚ·-Ξ·?)
      .Emptyrec-allowed?       β†’ A.Emptyrec-allowed?
      .[]-cong-allowed-mode?   β†’ A.[]-cong-allowed-mode?
      .no-sink-or-β‰€πŸ˜           β†’ A.no-sink-or-β‰€πŸ˜
      .Quotient-terms-allowed? β†’
        A.Quotient-terms-allowed?
      .Higher-quotient-constructors-allowed? β†’
        A.Higher-quotient-constructors-allowed?
    where
    module A = UD.Assumptions (Assumptions-only-some-erased-matches as)
    open UD.Assumptions
    open Type-restrictions TR