72 lines
1.7 KiB
Agda
72 lines
1.7 KiB
Agda
{-# OPTIONS --cubical #-}
|
||
|
||
open import Cubical.Foundations.Prelude
|
||
open import Cubical.Foundations.Equiv
|
||
open import Cubical.Foundations.Isomorphism
|
||
open import Cubical.Foundations.Univalence
|
||
|
||
-- Path induction
|
||
|
||
path-ind : {A : Set}
|
||
→ (C : (x y : A) → x ≡ y → Set)
|
||
→ (c : (x : A) → C x x refl)
|
||
→ (x y : A) → (p : x ≡ y) → C x y p
|
||
path-ind C c x y p = {! !}
|
||
|
||
-- Lemma 2.1.1
|
||
|
||
-- TODO: Not sure if there's actually a way to express inductive principle of
|
||
-- identity in code?
|
||
lemma211 : {A : Set} → (x y : A) → (x ≡ y) → (y ≡ x)
|
||
lemma211 x y p = (λ i → p (~ i))
|
||
|
||
D : {A : Set} → (x y : A) → x ≡ y → Set
|
||
D x y p = y ≡ x
|
||
|
||
d : {A : Set} → (x : A) → D x x refl
|
||
d x = refl
|
||
|
||
-- Lemma 2.1.2
|
||
|
||
lemma212 : {A : Set} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
|
||
lemma212 p q = p ∙ q
|
||
-- (x ≡ z) i0 = x
|
||
-- (x ≡ z) i1 = z
|
||
--
|
||
-- if i = i0 then
|
||
-- p i0 = x
|
||
-- q i0 = y
|
||
--
|
||
-- if i = i1 then
|
||
-- p i1 = y
|
||
-- q i1 = z
|
||
--
|
||
-- overall
|
||
-- p i = i0 ∧ i
|
||
-- q i = i1 ∨ i
|
||
|
||
-- Lemma 2.11.1
|
||
|
||
ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
|
||
ap f p i = f (p i)
|
||
|
||
lemma2111 : {A B : Set} → (f : A → B) → (ie : isEquiv f) → {a a′ : A}
|
||
→ isEquiv (ap f)
|
||
lemma2111 f ie .equiv-proof y = {! !}
|
||
|
||
-- Lemma 2.11.2
|
||
|
||
lemma2112a : {A : Set} → (a : A) → {x₁ x₂ : A} → (p : x₁ ≡ x₂) → (q : a ≡ x₁)
|
||
→ transport {! !} p ≡ q ∙ p
|
||
lemma2112a a p q = {! !}
|
||
|
||
-- Lemma 2.11.3
|
||
|
||
lemma2113 : {A B : Set}
|
||
→ (f g : A → B)
|
||
→ {a a′ : A}
|
||
→ (p : a ≡ a′)
|
||
→ (q : f a ≡ g a)
|
||
→ Set
|
||
-- TODO:
|
||
-- → transport (λ i → f a′ ≡ g a′) x ≡ (sym (ap f p)) ∙ q ∙ (ap g p)
|