prop ext lacking

RedProp.agda

@@ -1,5 +1,5 @@
 {-# OPTIONS --prop --rewriting --allow-unsolved-metas #-}
-module AME where
+module RedProp where
 
 open import Lib hiding (id; _∘_)
 open import StrictLib renaming (_,_ to _p,_)
@@ -200,7 +200,7 @@ appS : {Γ : Con} {a : TmS Γ U} → {B : TyS (Γ ▶P El a)} → (f : TmS Γ (
 appS {Γ}{a}{B} f = record { ᴬ   = λ { (γ , α) → f.ᴬ γ α } ;
                             ᴹ   = λ { {γᴬ , αᴬ} {δᴬ , βᴬ} (γᴹ , lift refl) → (f.ᴹ γᴹ αᴬ) } ;
                             ᴾᴬ  = λ { (γᴾᴬ , plift α) → f.ᴾᴬ γᴾᴬ α } ;
-                            E   = f.E  ;
+                            E   = f.E ;
                             w   = λ { (γ , α) → f.w γ S.$S α } ;
                             R   = λ { (γ , α) (γᴬ , αᴬ) → f.R γ γᴬ S.$S αᴬ } }
   where

StrictLib.agda

@@ -0,0 +1,44 @@
+{-# OPTIONS --prop --rewriting --allow-unsolved-metas #-}
+
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Lib
+
+module StrictLib where
+
+data P⊤ {ℓ} : Prop ℓ where
+  ptt : P⊤
+
+data _∧_ {ℓ}(p q : Prop ℓ) : Prop ℓ where
+  _,_ : p → q → (p ∧ q)
+
+p₁ : ∀{ℓ}{p q : Prop ℓ} → p ∧ q → p
+p₁ (x , y) = x
+
+p₂ : ∀{ℓ}{p q : Prop ℓ} → p ∧ q → q
+p₂ (x , y) = y
+
+Pcoe : ∀{ℓ}{A A' : Prop ℓ} → A ≡ A' → A → A'
+Pcoe refl a = a
+
+PΠ≡ :
+  ∀ {α β}{A A' : Set α}{B : A → Prop β}{B' : A' → Prop β}
+  → (p : A ≡ A') → ((a : A) → B a ≡ B' (coe p a))
+  → ((a : A) → B a) ≡ ((a' : A') → B' a')
+PΠ≡ {A = A} {B = B} {B'} refl q = (λ B → (x : A) → B x) & ext q
+
+PPΠ≡ :
+  ∀ {α β}{A A' : Prop α}{B : A → Prop β}{B' : A' → Prop β}
+  → (p : A ≡ A') → ((a : A) → B a ≡ B' (Pcoe p a))
+  → ((a : A) → B a) ≡ ((a' : A') → B' a')
+PPΠ≡ {A = A} {B = B} {B'} refl q = {!!} --(λ B → (x : A) → B x) & pext q
+
+PPΠ≡' :
+  ∀ {α β}{A : Prop α}{B B' : A → Prop β} → ((a : A) → B a ≡ B' a)
+  → ((a : A) → B a) ≡ ((a' : A) → B' a')
+PPΠ≡' {A = A}{B}{B'} q = apd (λ (B : A → Prop _) → (a : A) → B a) {!!}
+
+PΠ≡i :
+  ∀ {α β}{A A' : Set α}{B : A → Prop β}{B' : A' → Prop β}
+  → (p : A ≡ A') → ((a : A) → B a ≡ B' (coe p a))
+  → ({a : A} → B a) ≡ ({a' : A'} → B' a')
+PΠ≡i {A = A}{B = B} refl q = (λ B → {x : A} → B x) & ext q