Prove identity law for coercions.

This commit is contained in:
Frederik Hanghøj Iversen 2018-03-20 12:12:09 +01:00
parent 30725d71b6
commit 2188e690a0

View file

@ -28,21 +28,12 @@ sym≃ = Equivalence.symmetry
infixl 10 _⊙_ infixl 10 _⊙_
module _ { : Level} {A : Set } {a : A} where module _ { : Level} {A : Set } {a : A} where
-- "This follows from the propositional equiality for `J`" - Vezzosi.
id-coe : coe refl a a id-coe : coe refl a a
id-coe = begin id-coe = begin
coe refl a ≡⟨⟩ coe refl a ≡⟨⟩
-- pathJprop : pathJ _ refl ≡ d pathJ (λ y x A) _ A refl ≡⟨ pathJprop {x = a} (λ y x A) _
pathJ (λ y x A) scary A refl ≡⟨ pathJprop {x = scary} (λ y x A) scary _ ≡⟨ pathJprop {x = a} (λ y x A) _
scary ≡⟨ {!!}
-- pathJ (λ y x → A) scary A refl ≡⟨ pathJprop {A = A} (λ y x → A) scary ⟩
-- scary ≡⟨ {!!} ⟩
-- pathJ (λ y _ → B _ → B y) (λ x → x) _ p ≡⟨ {!!} ⟩
a a
where
scary : A
scary = (primComp (λ j A) i0 (λ j p[ a ] i0 (~ j)) a)
module _ { : Level} {A B : Set } {a : A} where module _ { : Level} {A B : Set } {a : A} where
inv-coe : (p : A B) coe (sym p) (coe p a) a inv-coe : (p : A B) coe (sym p) (coe p a) a