------------------------------------------------------------------------
-- The Agda standard library
--
-- Some code related to the W type that relies on the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.W.WithK where

open import Data.Product.Base using (_,_)
open import Data.Container.Core using (Container; Shape; Position; _⇒_)
open import Data.W using (W; sup)
open import Agda.Builtin.Equality using (_≡_; refl)

module _ {s p} {C : Container s p}
         {s : Shape C} {f : Position C s → W C} where

 sup-injective₂ : ∀ {g} → sup (s , f) ≡ sup (s , g) → f ≡ g
 sup-injective₂ refl = refl