From a4b867910e4bffccb959c83dcbc4c79c2ba274fc Mon Sep 17 00:00:00 2001
From: Rahul Chhabra <rahul29112002@gmail.com>
Date: Thu, 28 Mar 2024 15:54:34 +0530
Subject: [PATCH] Formulate propositional resizing

---
 src/Realizability/PropResizing.agda | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 src/Realizability/PropResizing.agda

diff --git a/src/Realizability/PropResizing.agda b/src/Realizability/PropResizing.agda
new file mode 100644
index 0000000..67e63fe
--- /dev/null
+++ b/src/Realizability/PropResizing.agda
@@ -0,0 +1,17 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+
+module Realizability.PropResizing where
+
+-- Formulation of propositional resizing inspired by the corresponding formulation
+-- in TypeTopology
+-- https://www.cs.bham.ac.uk/~mhe/TypeTopology/UF.Size.html
+
+copyOf : ∀ {ℓ} → Type ℓ → (ℓ' : Level) → Type _
+copyOf {ℓ} X ℓ' = Σ[ copy ∈ Type ℓ' ] X ≃ copy
+
+copy = fst
+copyEquiv = snd
+
+propResizing : ∀ ℓ ℓ' → Type _
+propResizing ℓ ℓ' = ∀ (X : Type ℓ) → isProp X → copyOf X ℓ'