removed postulated property for elim UI

+ added funext as explicit parameter

.gitignore

@@ -1,3 +1,4 @@
 *~
 _build
 *.agdai
+paper

examples/Parametrized.agda

@@ -28,7 +28,7 @@ module Nat where
 
   elimℕ : ∀ {ℓ} (P : ℕ → Set ℓ) → P 0 → (∀ n → P n → P (suc n))
         → ∀ n → P n
-  elimℕ P H0 Hn n = elim″ natHasDesc P H0 Hn n
+  elimℕ P H0 Hn n = elim″ natHasDesc P {!!} H0 Hn n
 
   showℕ : ℕ → String
   showℕ = show natHasDesc (tt , tt , tt)
@@ -59,8 +59,8 @@ module Vek where
 
   postulate P : {A : Set} {n : ℕ} → vek A n → Set
 
-  -- t : ∀ {A} {n} (x : vek A n) → P x
-  -- t = elim″ vekHasDesc P {!!} λ x g Pg → {!!}
+  t : ∀ {A} {n} (x : vek A n) → P x
+  t = elim″ vekHasDesc P {!!} {!!} λ x g Pg → {!!}
 
   showV : {A : Set} → (A → String) → ∀ {n} → vek A n → String
   showV showA =

generics.agda-lib

@@ -1,5 +1,4 @@
 name: generics
 include: src
 depend:
-  agda-prelude
-  standard-library
+  standard-library

src/Generics/Constructions/Elim.agda

@@ -1,9 +1,7 @@
-{-# OPTIONS --rewriting #-}
+{-# OPTIONS --safe #-}
 
 module Generics.Constructions.Elim where
 
-open import Agda.Builtin.Equality.Rewrite
-
 open import Generics.Prelude hiding (lookup)
 open import Generics.Telescope
 open import Generics.Desc
@@ -52,7 +50,8 @@ module Elim {P} {I : ExTele P} {ℓ} {A : Indexed P I ℓ} (H : HasDesc {P} {I}
          elim x rewrite sym (from∘to x) = Ind.ind to-hypothesis (to x)
 
 module _ {P} {I : ExTele P} {ℓ} {A : Indexed P I ℓ} (H : HasDesc {P} {I} {ℓ} A)
-         {c} (Pr : Pred P I (uncurry P I A) c) where
+         {c} (Pr : Pred P I (uncurry P I A) c)
+         (funext : ∀ {a b} → Extensionality a b) where
 
   open HasDesc H
   open Elim H Pr
@@ -197,13 +196,45 @@ module _ {P} {I : ExTele P} {ℓ} {A : Indexed P I ℓ} (H : HasDesc {P} {I} {
   --        {pv : Σ[ P ⇒ V ]} (x : ⟦⟧ᵇ ℓ e i A′ S C pv) (H : All⟦⟧ᵇ e i A′ S C Pr′ x)
   --      → mott′ e i S C pv (mmott′ e i S C pv x H) ≡ x
 
-  postulate rew : ∀ {V} {C : Desc P V I ℓ} {pv : Σ[ P ⇒ V ]}
-                  (x : ⟦ C ⟧ ℓ A′ pv)
-                  (H : All⟦⟧ C A′ Pr′ x)
-                → mott {C = C} (mmott {C = C} x H) ≡ x
+  -- postulate rew : ∀ {V} {C : Desc P V I ℓ} {pv : Σ[ P ⇒ V ]}
+  --                 (x : ⟦ C ⟧ ℓ A′ pv)
+  --                 (H : All⟦⟧ C A′ Pr′ x)
+  --               → mott {C = C} (mmott {C = C} x H) ≡ x
+
+
+  mutual
+    rew : ∀ {V} {C : Desc P V I ℓ} {pv : Σ[ P ⇒ V ]}
+          (x : ⟦ C ⟧ ℓ A′ pv)
+          (H : All⟦⟧ C A′ Pr′ x)
+        → mott {C = C} (mmott {C = C} x H) ≡ x
+    rew {C = var i    } x H = refl
+    rew {C = π p i S C} x H = rewᵇ x H
+    rew {C = A ⊗ B} (a , b) (HA , HB)
+      rewrite rew {C = A} a HA
+            | rew {C = B} b HB = refl
+
+    rewᵇ : ∀ {V} {ℓ₁ ℓ₂} {p : ℓ₁ ≡ ℓ₂ ⊔ ℓ} {i} {S : Σ[ P ⇒ V ] → Set ℓ₂}
+           {C : Desc P (V ⊢< i > S)  I ℓ}
+           {pv : Σ[ P ⇒ V ]}
+           (x : ⟦⟧ᵇ ℓ p i A′ S C pv)
+           (H : All⟦⟧ᵇ p i A′ S C Pr′ x)
+         → mott′ p i S C pv (mmott′ p i S C pv x H) ≡ x
+    rewᵇ {p = refl} {ai visible relevant} {C = C} x H =
+      funext (λ y → rew {C = C} (x y) (H y))
+    rewᵇ {p = refl} {ai visible irrelevant} {C = C} x H =
+      funext (λ y → rew {C = C} (x y) (H y))
+    rewᵇ {p = refl} {ai hidden relevant} {C = C} x H =
+      funext (λ y → rew {C = C} (x y) (H y))
+    rewᵇ {p = refl} {ai hidden irrelevant} {C = C} x H =
+      funext (λ y → rew {C = C} (x y) (H y))
+    rewᵇ {p = refl} {ai instance′ relevant} {C = C} x H =
+      funext (λ y → rew {C = C} (x y) (H y))
+    rewᵇ {p = refl} {ai instance′ irrelevant} {C = C} x H =
+      funext (λ y → rew {C = C} (x y) (H y))
 
   -- TODO: remove this rewrite rule, actually prove it
-  {-# REWRITE rew #-}
+  -- {-# REWRITE rew #-}
+
 
   module _ {k} where
 
@@ -218,8 +249,13 @@ module _ {P} {I : ExTele P} {ℓ} {A : Indexed P I ℓ} (H : HasDesc {P} {I} {
           → Pr′ (constr (k , g x))
       mmmE {C = var x} (lift refl) m f tie _ = tie m
       mmmE {C = π e i S C} x m mk tie H = mmmE′ e i S C x m mk tie H
-      mmmE {C = A ⊗ B} (xa , xb) m f tie (HA , HB) =
-        mmmE {C = B} xb (m (mmott {C = A} xa HA) (mottt {C = A} HA)) (f ∘ (xa ,_)) tie HB
+      mmmE {C = A ⊗ B} (xa , xb) {g} m f tie (HA , HB)  =
+        mmmE {C = B} xb (m (mmott {C = A} xa HA)
+                           (mottt {C = A} (subst (All⟦⟧ A A′ Pr′) (sym p) HA)))
+                        (f ∘ (xa ,_))
+                        (subst (λ X → g (X , xb) → Pr′ (constr (k , f (xa , xb)))) (sym p) tie)
+                        HB
+        where p = rew {C = A} xa HA
 
       mmmE′ : ∀ {V}{ℓ₁ ℓ₂}
             → (e  : ℓ₁ ≡ ℓ₂ ⊔ ℓ)
@@ -241,7 +277,6 @@ module _ {P} {I : ExTele P} {ℓ} {A : Indexed P I ℓ} (H : HasDesc {P} {I} {
       mmmE′ refl (ai instance′ relevant  ) S C (s      , d) {f} m mk tie H = mmmE {C = C} d (m ⦃ s ⦄) (mk ∘ (s ,_)) tie H
       mmmE′ refl (ai instance′ irrelevant) S C (irrv s , d) {f} m mk tie H = mmmE {C = C} d (m ⦃ s ⦄) (mk ∘ (irrv s ,_)) tie H
 
-
   GoodMethods : SetList n
   GoodMethods = tabulate _ motive
 

src/Generics/Prelude.agda

@@ -9,9 +9,11 @@ open import Function.Base     public
 open import Data.Product      public hiding (map; uncurry; uncurry′)
 open import Level             public using (Lift; lift)
 
-open import Relation.Binary.PropositionalEquality public hiding ([_])
+open import Relation.Binary.PropositionalEquality public
+  hiding ([_]; Extensionality; ∀-extensionality)
 open import Data.Vec.Base     public using (_∷_; []; Vec; map; lookup)
 open import Data.Fin.Base     public using (Fin; zero; suc)
+open import Axiom.Extensionality.Propositional public
 
 open import Agda.Builtin.Reflection public
   using ( ArgInfo; Relevance; Visibility