-
-
Save jespercockx/7bc583734a578809e5bf31cc54c01aa9 to your computer and use it in GitHub Desktop.
Diffs needed to make code on http://www.cse.chalmers.se/~nad/software.html work with https://github.com/agda/agda/pull/2866
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
diff --git a/src/Bool.agda b/src/Bool.agda | |
index 25a0a7f..ff7c092 100644 | |
--- a/src/Bool.agda | |
+++ b/src/Bool.agda | |
@@ -86,7 +86,7 @@ not≡↔≡not {false} {false} = | |
-- Some lemmas related to T. | |
-T↔≡true : ∀ {b} → T b ↔ b ≡ true | |
+T↔≡true : {b : Bool} → T b ↔ b ≡ true | |
T↔≡true {false} = $⟨ Bool.true≢false ⟩ | |
true ≢ false ↝⟨ (_∘ sym) ⟩ | |
false ≢ true ↝⟨ Bijection.⊥↔uninhabited ⟩□ | |
diff --git a/src/Equality.agda b/src/Equality.agda | |
index d45e369..8b74c2d 100644 | |
--- a/src/Equality.agda | |
+++ b/src/Equality.agda | |
@@ -1590,7 +1590,7 @@ module Derived-definitions-and-properties | |
trans (f≡g x px) (cong g (refl x)) ∎) | |
_ | |
where | |
- T-irr : ∀ b → Proof-irrelevant (T b) | |
+ T-irr : (b : Bool) → Proof-irrelevant (T b) | |
T-irr true _ _ = refl _ | |
T-irr false () | |
diff --git a/src/H-level/Closure.agda b/src/H-level/Closure.agda | |
index 82ad340..8428906 100644 | |
--- a/src/H-level/Closure.agda | |
+++ b/src/H-level/Closure.agda | |
@@ -625,7 +625,7 @@ abstract | |
to : A ⊎ B → (∃ λ x → if x then ↑ b A else ↑ a B) | |
to = [ _,_ true ∘ lift , _,_ false ∘ lift ] | |
- from : (∃ λ x → if x then ↑ b A else ↑ a B) → A ⊎ B | |
+ from : (∃ {A = Bool} λ x → if x then ↑ b A else ↑ a B) → A ⊎ B | |
from (true , x) = inj₁ $ lower x | |
from (false , y) = inj₂ $ lower y | |
@@ -665,7 +665,7 @@ abstract | |
Bool-2+n : H-level (2 + n) Bool | |
Bool-2+n = mono (m≤m+n 2 n) Bool-set | |
- if-2+n : ∀ x → H-level (2 + n) (if x then ↑ b A else ↑ a B) | |
+ if-2+n : (x : Bool) → H-level (2 + n) (if x then ↑ b A else ↑ a B) | |
if-2+n true = respects-surjection | |
(_↔_.surjection $ Bijection.inverse ↑↔) | |
(2 + n) hA | |
diff --git a/src/Quotient.agda b/src/Quotient.agda | |
index a85dc73..4e1c09a 100644 | |
--- a/src/Quotient.agda | |
+++ b/src/Quotient.agda | |
@@ -694,7 +694,8 @@ module _ {a} {A : Set a} {R : A → A → Set a} where | |
inverse currying) (λ _ → | |
F.id) ⟩ | |
(∃ λ (f : (x : A) → (∃ λ P → R x ≡ P) → B) → | |
- ∀ P → Constant (λ { (x , eq) → f x (P , eq) })) ↝⟨ inverse $ | |
+ ∀ P → Constant {A = ∃ λ x → R x ≡ P} (λ { (x , eq) → f x (P , eq) })) | |
+ ↝⟨ inverse $ | |
Σ-cong (Bij.inverse $ | |
∀-cong (lower-extensionality _ _ ext) λ _ → | |
drop-⊤-left-Π (lower-extensionality _ _ ext) $ | |
diff --git a/src/Univalence-axiom/Isomorphism-is-equality/Simple.agda b/src/Univalence-axiom/Isomorphism-is-equality/Simple.agda | |
index d0a5eca..44b0377 100644 | |
--- a/src/Univalence-axiom/Isomorphism-is-equality/Simple.agda | |
+++ b/src/Univalence-axiom/Isomorphism-is-equality/Simple.agda | |
@@ -291,7 +291,8 @@ module Class (Univ : Universe) where | |
eq) | |
(Σ-map ≡⇒≃ f (Σ-≡,≡←≡ (proj₁ (Σ-≡,≡←≡ {A = ∃ (El a)} | |
- (cong (λ { (C , (x , p)) → (C , x) , p }) | |
+ (cong {A = ∃ λ _ → ∃ _} | |
+ (λ { (C , (x , p)) → (C , x) , p }) | |
(refl (C , x , p)))))) ≡⟨ cong (Σ-map ≡⇒≃ f ∘ Σ-≡,≡←≡ ∘ proj₁ ∘ Σ-≡,≡←≡) $ | |
cong-refl {A = Instance (a , P)} | |
(λ { (C , (x , p)) → (C , x) , p }) ⟩ | |
@@ -1273,7 +1274,7 @@ private | |
+-comm *-comm *+ +0 *1 +- 0≢1 = | |
_⇔_.from propositional⇔irrelevant irr | |
where | |
- irr : ∀ x y → x ≡ y | |
+ irr : (x y : ∃ λ _ → ∃ _) → x ≡ y | |
irr (inv , inv₁ , inv₂) (inv′ , inv₁′ , inv₂′) = | |
_↔_.to (ignore-propositional-component | |
(×-closure 1 (Π-closure ext 1 λ _ → | |
diff --git a/src/Lambda/Partiality-monad/Inductive/Interpreter.agda b/src/Lambda/Partiality-monad/Inductive/Interpreter.agda | |
index 441d226..47e589b 100644 | |
--- a/src/Lambda/Partiality-monad/Inductive/Interpreter.agda | |
+++ b/src/Lambda/Partiality-monad/Inductive/Interpreter.agda | |
@@ -136,7 +136,7 @@ module Interpreter₂ where | |
⟦_⟧ : ∀ {n} → Tm n → Env n → M Value | |
run (⟦ t ⟧ ρ) = | |
- fixP (λ { (_ , t , ρ) → run (⟦ t ⟧′ ρ) }) (_ , t , ρ) | |
+ fixP {A = ∃ λ _ → ∃ _} (λ { (_ , t , ρ) → run (⟦ t ⟧′ ρ) }) (_ , t , ρ) | |
------------------------------------------------------------------------ | |
-- The two interpreters are pointwise equal | |
diff --git a/src/Bisimilarity/Classical.agda b/src/Bisimilarity/Classical.agda | |
index 98f9ec6..907cd71 100644 | |
--- a/src/Bisimilarity/Classical.agda | |
+++ b/src/Bisimilarity/Classical.agda | |
@@ -175,15 +175,16 @@ transitive-∼ p∼q q∼r with _⇔_.to (Bisimilarity↔ _) p∼q | |
| _⇔_.to (Bisimilarity↔ _) q∼r | |
... | R₁ , R-is₁ , pR₁q | R₂ , R-is₂ , qR₂r = | |
⟨ R₁ ⊙ R₂ | |
- , ⟪ (λ { (q , pR₁q , qR₂r) p⟶p′ → | |
+ , ⟪_,_⟫ | |
+ {R = λ _ → ∃ λ _ → ∃ _} | |
+ (λ { (q , pR₁q , qR₂r) p⟶p′ → | |
let q′ , q⟶q′ , p′R₁q′ = left-to-right R-is₁ pR₁q p⟶p′ | |
r′ , r⟶r′ , q′R₂r′ = left-to-right R-is₂ qR₂r q⟶q′ | |
in r′ , r⟶r′ , (q′ , p′R₁q′ , q′R₂r′) }) | |
- , (λ { (q , pR₁q , qR₂r) r⟶r′ → | |
+ (λ { (q , pR₁q , qR₂r) r⟶r′ → | |
let q′ , q⟶q′ , q′R₂r′ = right-to-left R-is₂ qR₂r r⟶r′ | |
p′ , p⟶p′ , p′R₁q′ = right-to-left R-is₁ pR₁q q⟶q′ | |
in p′ , p⟶p′ , (q′ , p′R₁q′ , q′R₂r′) }) | |
- ⟫ | |
, (_ , pR₁q , qR₂r) | |
⟩ | |
@@ -240,7 +241,9 @@ bisimulation-up-to-∼⇒bisimulation : | |
Bisimulation-up-to-bisimilarity R → | |
Bisimulation (Bisimilarity ⊙ R ⊙ Bisimilarity) | |
bisimulation-up-to-∼⇒bisimulation R-is = | |
- ⟪ (λ { (q , p∼q , r , qRr , r∼s) p⟶p′ → | |
+ ⟪_,_⟫ | |
+ {R = λ _ → ∃ λ _ → ∃ λ _ → ∃ λ _ → ∃ _} | |
+ (λ { (q , p∼q , r , qRr , r∼s) p⟶p′ → | |
let q′ , q⟶q′ , p′∼q′ = | |
left-to-right bisimilarity-is-a-bisimulation p∼q p⟶p′ | |
r′ , r⟶r′ , (q″ , q′∼q″ , r″ , q″Rr″ , r″∼r′) = | |
@@ -252,7 +255,7 @@ bisimulation-up-to-∼⇒bisimulation R-is = | |
, transitive-∼ p′∼q′ q′∼q″ | |
, r″ , q″Rr″ | |
, transitive-∼ r″∼r′ r′∼s′ }) | |
- , (λ { (q , p∼q , r , qRr , r∼s) s⟶s′ → | |
+ (λ { (q , p∼q , r , qRr , r∼s) s⟶s′ → | |
let r′ , r⟶r′ , r′∼s′ = | |
right-to-left bisimilarity-is-a-bisimulation r∼s s⟶s′ | |
q′ , q⟶q′ , (q″ , q′∼q″ , r″ , q″Rr″ , r″∼r′) = | |
@@ -264,7 +267,6 @@ bisimulation-up-to-∼⇒bisimulation R-is = | |
, transitive-∼ p′∼q′ q′∼q″ | |
, r″ , q″Rr″ | |
, transitive-∼ r″∼r′ r′∼s′ }) | |
- ⟫ | |
-- If R is a bisimulation up to bisimilarity, then R is contained in | |
-- bisimilarity. | |
diff --git a/src/Free-variables.agda b/src/Free-variables.agda | |
index ffdd957..57b701a 100644 | |
--- a/src/Free-variables.agda | |
+++ b/src/Free-variables.agda | |
@@ -117,7 +117,7 @@ mutual | |
subst-∈FV x (lambda y e) (lambda x′≢y p) | yes x≡y = inj₁ (lambda x′≢y p , x′≢y ∘ flip trans x≡y) | |
subst-∈FV x (lambda y e) (lambda x′≢y p) | no _ = ⊎-map (Σ-map (lambda x′≢y) id) id (subst-∈FV x e p) | |
subst-∈FV x (case e bs) (case-head p) = ⊎-map (Σ-map case-head id) id (subst-∈FV x e p) | |
- subst-∈FV x (case e bs) (case-body p ps x′∉xs) = ⊎-map (Σ-map (λ p → let _ , _ , _ , ps , p , ∉ = p in | |
+ subst-∈FV x (case e bs) (case-body p ps x′∉xs) = ⊎-map (Σ-map (λ (p : ∃ λ _ → ∃ λ _ → ∃ λ _ → ∃ λ _ → ∃ _) → let _ , _ , _ , ps , p , ∉ = p in | |
case-body p ps ∉) | |
id) | |
id | |
diff -rN -u old-dependent-lenses/src/Lens/Non-dependent/Alternative.agda new-dependent-lenses/src/Lens/Non-dependent/Alternative.agda | |
--- old-dependent-lenses/src/Lens/Non-dependent/Alternative.agda 2018-01-05 11:39:25.769594364 +0100 | |
+++ new-dependent-lenses/src/Lens/Non-dependent/Alternative.agda 2018-01-05 11:39:25.769594364 +0100 | |
@@ -953,7 +953,7 @@ | |
(∥ B ∥ × | |
(∃ λ (f : B → R) → Constant f) × | |
- (∃ λ (g : B → B) → B → ∀ b → b ≡ g b)) ↔⟨ (∃-cong λ ∥b∥ → ∃-cong λ { (f , _) → ∃-cong λ _ → inverse $ | |
+ (∃ λ (g : B → B) → B → ∀ b → b ≡ g b)) ↔⟨ (∃-cong λ ∥b∥ → ∃-cong {A = ∃ _} λ { (f , _) → ∃-cong λ _ → inverse $ | |
→-intro ext (λ _ → B-set f ∥b∥ _ _) }) ⟩ | |
(∥ B ∥ × | |
(∃ λ (f : B → R) → Constant f) × |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment