{-

 Martin Escardo, 9 May 2016.

 I wanted an inconsistent function

   resize : {i j : Level} → Set i → Set j

 in Agda such that (resize X) is definitionally equal to X,
 as an alternative to --type-in-type.

 Andreas Abel suggested to use Agda's new option --rewriting,
 with the rewrite rule

   resize-id : {i j : Level} {A : Set i} → resize {i} {j} A ↦ A

 Jesper Cockx added a patch to Agda to allow rewrite rules which
 change type, such as the above.

 Thanks to Andreas and Jesper for their instant help!

 I also needed to add the functions resize-in and resize-out below,
 with corresponding rewriting rules.

 This module should not be used other than by specialized modules that
 know what they are doing.

 In this development it is prop.agda only.

 In the current version of Agda, 2.5.2, direct or indirect users of
 this module will need to use the option --rewriting like this:

-}

{-# OPTIONS --without-K #-}
{-# OPTIONS --rewriting #-}

module resize where

open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_) public

postulate
  _↦_ : {i j : Level}{A : Set i}{B : Set j} → A → B → Set (i ⊔ j)

{-# BUILTIN REWRITE _↦_ #-}

postulate
  resize        : {i j : Level} → Set i → Set j
  resize-id     : {i j : Level} {X : Set i} → resize {i} {j} X ↦ X
  resize-in     : {i j : Level} {X : Set i} → X → resize {i} {j} X
  resize-in-id  : {i j : Level} {X : Set i} (x : X) → resize-in {i} {j} {X} x ↦ x
  resize-out    : {i j : Level} {X : Set i} → resize {i} {j} X → X
  resize-out-id : {i j : Level} {X : Set i} (r : resize {i} {j} X) → resize-out {i} {j} {X} r ↦ r

{-# REWRITE resize-id #-}
{-# REWRITE resize-in-id #-}
{-# REWRITE resize-out-id #-}