From 55b18bab2c784897720b0e504c9ccd7b2241b3c3 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 11 Jul 2023 17:03:29 -0400
Subject: [PATCH] More properties of later

---
 .../Common/LaterProperties.agda               | 29 +++++++++++++++++--
 1 file changed, 27 insertions(+), 2 deletions(-)

diff --git a/formalizations/guarded-cubical/Common/LaterProperties.agda b/formalizations/guarded-cubical/Common/LaterProperties.agda
index b6dcb2c..d875ae6 100644
--- a/formalizations/guarded-cubical/Common/LaterProperties.agda
+++ b/formalizations/guarded-cubical/Common/LaterProperties.agda
@@ -70,6 +70,9 @@ path-x-f-next-x {k = k} {A = A} {f = f} = (fix f , fix-eq f) , unique
           {!!} ≡⟨ {!!} ⟩
           {!!} ≡⟨ {!!} ⟩
           (cong f λ i -> λ t -> q i) ∎
+
+        eq' : PathP (λ i → q i ≡ f (next (q i))) (fix-eq f) p-h
+        eq' = compPathL→PathP {!!}
          
         eq : PathP (λ i → q i ≡ f (next (q i))) (fix-eq f) p-h
         eq = transport (sym (PathP≡doubleCompPathˡ q (fix-eq f) p-h (cong f (λ i -> λ t -> q i))))
@@ -87,16 +90,38 @@ fixpoints-unique = {!!}
 
 
 
+-- If we have an equality later, then this induces an equality now
+eq▹ : {k : Clock} {ℓ : Level} {X : Type ℓ} ->
+  (x~ y~ : ▹ k , X) ->
+  ▸ (λ t -> x~ t ≡ y~ t) -> x~ ≡ y~
+eq▹ x~ y~ eq~ i t = eq~ t i
+
+-- Dependent version:
+eq▸ : {k : Clock} {ℓ : Level} {X : ▹ k , Type ℓ} ->
+  (x~ y~ : ▸ X) ->
+  ▸ (λ t -> x~ t ≡ y~ t) -> x~ ≡ y~
+eq▸ x~ y~ eq~ i t = eq~ t i
+
+-- If we know that X is a prop later, then we can conclude that
+-- ▹ X is a prop now.
+-- Dependent version:
+isProp▸ : {k : Clock} {ℓ : Level} {X : ▹ k , Type ℓ} ->
+  ▸ (λ t -> isProp (X t)) -> isProp (▸ λ t -> X t)
+isProp▸ H x~ y~ i t = H t (x~ t) (y~ t) i
 
+
+-- If we know that X is a set later, then we can conclude that
+-- ▹ X is a set now.
 isSet▹ : {k : Clock} {ℓ : Level} {X : Type ℓ} ->
   ▹ k , (isSet X) -> isSet (▹ k ,  X)
 isSet▹ H x~ y~ p1 p2 i j t =
   H t (x~ t) (y~ t) (λ l -> p1 l t) (λ l -> p2 l t) i j
 
--- Dependent version
+-- Dependent version of the above
 isSet▸ : {k : Clock} {ℓ : Level} {X : ▹ k , Type ℓ} ->
   ▸ (λ t -> isSet (X t)) -> isSet (▸ λ t -> X t)
-isSet▸ H x~ y~ p1 p2 i j t = H t (x~ t) (y~ t) (λ l -> p1 l t) (λ l -> p2 l t) i j
+isSet▸ H x~ y~ p1 p2 i j t =
+  H t (x~ t) (y~ t) (λ l -> p1 l t) (λ l -> p2 l t) i j
 
 
 
-- 
GitLab