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
{-# OPTIONS --without-K #-} | |
module A where | |
infixl 4 _≡_ | |
data _≡_ {A : Set} (x : A) : A → Set where | |
refl : x ≡ x | |
J : (A : Set) (C : (x y : A) → x ≡ y → Set) | |
→ ((x : A) → C x x refl) | |
→ (x y : A) (P : x ≡ y) | |
→ C x y P | |
J A C b x .x refl = b x | |
-- K : (A : Set) (x : A) (C : x ≡ x → Set) | |
-- → C refl | |
-- → (loop : x ≡ x) | |
-- → C loop | |
-- K A x C b p = {! p !} | |
-- lemma-2-1-1: inversion of paths | |
infix 6 ¬_ | |
¬_ : {A : Set} {x y : A} → x ≡ y → y ≡ x | |
¬_ {A} {x} {y} p = J A D d x y p | |
where | |
D : (x y : A) (p : x ≡ y) → Set | |
D x y p = y ≡ x | |
d : (x : A) → D x x refl | |
d x = refl | |
-- lemma-2-1-2: concatenation of paths | |
infixl 5 _∙_ | |
_∙_ : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z | |
_∙_ {A} {x} {y} {z} p q = J A D d x y p z q | |
where | |
-- the predicate | |
D : (x y : A) (p : x ≡ y) → Set | |
D x y p = (z : A) (q : y ≡ z) → x ≡ z | |
-- base case | |
d : (x z : A) (q : x ≡ z) → x ≡ z | |
d x z q = q | |
-- lemma-2-1-4-i: identity of path concatenation | |
∙-identityʳ : {A : Set} {x y : A} (p : x ≡ y) → p ≡ p ∙ refl | |
∙-identityʳ {A} {x} {y} p = J A D d x y p | |
where | |
-- the predicate | |
D : (x y : A) (p : x ≡ y) → Set | |
D x y p = p ≡ p ∙ refl | |
-- base case | |
d : (x : A) → D x x refl | |
d x = refl | |
∙-identityˡ : {A : Set} {x y : A} (p : x ≡ y) → p ≡ refl ∙ p | |
∙-identityˡ {A} {x} {y} p = J A D d x y p | |
where | |
-- the predicate | |
D : (x y : A) (p : x ≡ y) → Set | |
D x y p = p ≡ refl ∙ p | |
-- base case | |
d : (x : A) → D x x refl | |
d x = refl | |
-- lemma-2-1-4-ii: identity of path inversion | |
¬-identityʳ : {A : Set} {x y : A} (p : x ≡ y) → ¬ p ∙ p ≡ refl | |
¬-identityʳ {A} {x} {y} p = J A D d x y p | |
where | |
-- the predicate | |
D : (x y : A) (p : x ≡ y) → Set | |
D x y p = ¬ p ∙ p ≡ refl | |
-- base case | |
d : (x : A) → D x x refl | |
d x = refl | |
¬-identityˡ : {A : Set} {x y : A} (p : x ≡ y) → p ∙ ¬ p ≡ refl | |
¬-identityˡ {A} {x} {y} p = J A D d x y p | |
where | |
-- the predicate | |
D : (x y : A) (p : x ≡ y) → Set | |
D x y p = p ∙ ¬ p ≡ refl | |
-- base case | |
d : (x : A) → D x x refl | |
d x = refl | |
-- lemma-2-1-4-iii: involution of path inversion | |
involution : {A : Set} {x y : A} (p : x ≡ y) → ¬ ¬ p ≡ p | |
involution {A} {x} {y} p = J A D d x y p | |
where | |
-- the predicate | |
D : (x y : A) (p : x ≡ y) → Set | |
D x y p = ¬ ¬ p ≡ p | |
-- base case | |
d : (x : A) → D x x refl | |
d x = refl | |
-- lemma-2-1-4-iv: associativity of path concatenation | |
∘-assoc : {A : Set} {w x y z : A} | |
→ (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) | |
→ p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r | |
∘-assoc {A} {w} {x} {y} {z} p q r = J A D d w x p y q z r | |
where | |
-- the predicate | |
D : (w x : A) (p : w ≡ x) → Set | |
D w x p = (y : A) (q : x ≡ y) | |
→ (z : A) (r : y ≡ z) | |
→ p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r | |
-- base case | |
d : (x : A) → D x x refl | |
d x y q z r = refl | |
_⋆_ : {A : Set} {a b c : A} {p q : a ≡ b} {r s : b ≡ c} | |
→ (α : p ≡ q) (β : r ≡ s) | |
→ p ∙ r ≡ q ∙ s | |
_⋆_ {A} {a} {b} {c} {p} {q} {r} {s} α β = {! !} | |
where | |
infixl 6 _∙r_ | |
_∙r_ : {A : Set} {a b c : A} {p q : a ≡ b} | |
→ (α : p ≡ q) (r : b ≡ c) | |
→ p ∙ r ≡ q ∙ r | |
_∙r_ {A} {a} {b} {c} {p} {q} α r = J A D d b c r a p q α | |
where | |
-- the predicate | |
D : (b c : A) (r : b ≡ c) → Set | |
D b c r = (a : A) (p q : a ≡ b) (α : p ≡ q) | |
→ p ∙ r ≡ q ∙ r | |
-- base case | |
d : (x : A) → D x x refl | |
d x a p q α = ¬ (∙-identityʳ p) ∙ (α ∙ ∙-identityʳ q) | |
ru : {A : Set} {x y : A} (p : x ≡ y) → p ≡ p ∙ refl | |
ru {A} {x} {y} p = ∙-identityʳ p | |
lemma1 : ∀ {A : Set} {a b c : A} | |
→ {p q : a ≡ b} {c : b ≡ c} | |
→ {α : p ≡ q} | |
→ α ∙r refl ≡ ¬ ru p ∙ α ∙ ru q | |
lemma1 = {! !} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment