Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

finish library revisions

  • Loading branch information...
commit 11914dd8dd01c16398101e77268c40e4a91ccdaa 1 parent c06ab31
@dlicata335 authored
Showing with 1,868 additions and 1,235 deletions.
  1. +9 −9 README
  2. +32 −0 computational-interp/JFromSubst.agda
  3. +99 −0 computational-interp/ProdHigherBetaEta.agda
  4. +114 −0 homotopy/HigherHomotopyAbelian.agda
  5. +49 −0 homotopy/Hopf.agda
  6. +62 −0 homotopy/Pi1Either.agda
  7. +160 −0 homotopy/Pi1S1.agda
  8. +90 −0 homotopy/Pi1T.agda
  9. +88 −45 lib/AdjointEquiv.agda
  10. +7 −5 lib/BasicTypes.agda
  11. +32 −31 lib/Bool.agda
  12. +10 −0 lib/First.agda
  13. +88 −89 lib/Functions.agda
  14. +52 −35 lib/Int.agda
  15. +17 −15 lib/List.agda
  16. +35 −35 lib/Monoid.agda
  17. +4 −2 lib/Nat.agda
  18. +252 −380 lib/Paths.agda
  19. +104 −158 lib/Prods.agda
  20. +11 −13 lib/Univalence.agda
  21. +14 −11 lib/WEq.agda
  22. +5 −5 lib/spaces/1Sphere2.agda
  23. +3 −3 lib/spaces/2Sphere1.agda
  24. +9 −9 lib/spaces/2Sphere2.agda
  25. +2 −2 lib/spaces/3Sphere1.agda
  26. +17 −17 lib/spaces/3Sphere2.agda
  27. +72 −53 lib/spaces/Circle.agda
  28. +16 −16 lib/spaces/Interval.agda
  29. +1 −2  lib/spaces/Spaces.agda
  30. +267 −263 lib/spaces/Torus.agda
  31. +39 −37 polymorphism/SubsetModel.agda
  32. +108 −0 programming/Sequence.agda
View
18 README
@@ -1,18 +1,18 @@
oldlib
a bunch of stuff using an older version of lib/
- some of this needs to be resuccitated
+ some of this needs to be resuccitated, like joseph's code in applications/torus2
lib
basic constructions of homotopy type theory
-applications
- applications of homotopy type theory to proving/formalizing/reasoning
- Currently includes:
- (1) a proof that higher fundamental groups are abelian
+homotopy
+ applications of homotopy type theory to formalizing homotopy theory
+
+programming
+ applications of homotopy type theory to programming
+
+computational-interp
+ code having to do with the computational interpretation or 2tt
misc
miscellaneous little experiments
- Currently includes:
- (1) a proof that set extensionality (univalence) implies functional extensionality
- (2) a start at a translation of Voevodsky's basic definitions into Agda
- (3) working out the contradiction between univalence and UIP
View
32 computational-interp/JFromSubst.agda
@@ -0,0 +1,32 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open Paths
+
+module computational-interp.JFromSubst where
+
+ j-transport : {A : Set} {M : A} (C : (x : A) -> Path M x -> Set)
+ -> {N : A} -> (P : Path M N)
+ -> (C M id)
+ -> C N P
+ j-transport {A}{M}C {N} α =
+ transport (\ (p : Σ \ y -> Path M y) -> C (fst p) (snd p))
+ (pair≃ α (transport-Path-right α id))
+
+
+ j-transport-compute : {A : Set} {M : A} (C : (x : A) -> Path M x -> Set)
+ -> (M0 : C M id)
+ -> j-transport C id M0 ≃ M0
+ j-transport-compute {A}{M} C M0 =
+ transport (λ (p : Σ (λ y Path M y)) C (fst p) (snd p))
+ (pair≃ id (transport-Path-right id id)) M0 ≃〈 id 〉 -- transport-Path-post id id ≡ id
+ transport (λ (p : Σ (λ y Path M y)) C (fst p) (snd p))
+ (pair≃ id id) M0 ≃〈 id 〉 -- pair≃ id id ≃ id
+ transport (λ (p : Σ (λ y Path M y)) C (fst p) (snd p))
+ id M0 ≃〈 id 〉
+ M0 ∎
+
+
+
+
+
View
99 computational-interp/ProdHigherBetaEta.agda
@@ -0,0 +1,99 @@
+
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude hiding (_×_ ; fst ; snd; _,_; fst≃; snd≃; pair≃ ; transport-×; ×≃η; ×≃β1; ×≃β2; ∘-×)
+open Paths
+
+module computational-interp.ProdHigherBetaEta where
+
+ -- derived form
+ record _×_ (A : Set) (B : Set) : Set where
+ constructor _,_
+ field
+ fst : A
+ snd : B
+ open _×_
+
+ transport-× : {Γ : Set} {θ1 θ2 : Γ} (δ : θ1 ≃ θ2)
+ (A : Γ -> Set) (B : (γ : Γ) -> Set)
+ -> transport (\ γ -> A γ × B γ) δ
+ ≃ (\ p -> (transport A δ (fst p) , transport B δ (snd p)))
+ transport-× id A B = id
+
+ fst≃ : {A B : Set} {p q : A × B} -> p ≃ q -> (fst p) ≃ (fst q)
+ fst≃ = ap fst
+
+ snd≃ : {A B : Set} {p q : A × B} -> p ≃ q -> (snd p) ≃ (snd q)
+ snd≃ = ap snd
+
+ pair≃ : {A B : Set} {p q : A × B} -> (fst p) ≃ (fst q) -> (snd p) ≃ (snd q) -> p ≃ q
+ pair≃ a b = ap2 _,_ a b
+
+ ap-ap2-o : {A B C D : Set} (g : C -> D) (f : A -> B -> C)
+ {M N : A} (α : M ≃ N)
+ {M' N' : B} (β : M' ≃ N')
+ -> ap2 (\ x y -> g (f x y)) α β ≃ ap g (ap2 f α β)
+ ap-ap2-o _ _ id id = id
+
+ ap2-ap-o : {A B C A' : Set} (f : A -> B -> C) (g1 : A' -> A) (g2 : A' -> B)
+ {M N : A'} (α : M ≃ N)
+ -> ap (\ x -> f (g1 x) (g2 x)) α ≃ ap2 f (ap g1 α) (ap g2 α)
+ ap2-ap-o _ _ _ id = id
+
+ ×≃η : {A B : Set} {p q : A × B} -> (α : p ≃ q) -> (pair≃ (fst≃ α) (snd≃ α)) ≃ α
+ ×≃η α = ap-id _ ∘ ! (ap2-ap-o _,_ fst snd α)
+
+ ×≃β1 : {A B : Set} {p q : A × B}
+ (α : Id (fst p) (fst q))
+ (β : Id (snd p) (snd q))
+ -> Id (fst≃ (pair≃ α β)) α
+ ×≃β1 α β = ap2-β1 α β ∘ ! (ap-ap2-o fst _,_ α β)
+
+ ×≃β2 : {A B : Set} {p q : A × B}
+ (α : Id (fst p) (fst q))
+ (β : Id (snd p) (snd q))
+ -> (snd≃ (pair≃ α β)) ≃
+ β
+ ×≃β2 {p = x , y} {q = .x , .y} id id = id
+
+ ∘-× : {A : Set} {M N P Q R S : A} (a : N ≃ P) (b : R ≃ S) (c : M ≃ N) (d : Q ≃ R)
+ -> pair≃ a b ∘ pair≃ c d ≃ pair≃ (a ∘ c) (b ∘ d)
+ ∘-× id id id id = id
+
+ -- ap-×-fst : {A B : Set} {N M : A} -> (f : A -> B) -> (y : B) -> (α : M ≃ N) ->
+ -- ap (λ x → f (x) , y) α ≃
+ -- nondep-pair≃ (ap (λ x → f x) α) (ap (λ _ → y) α)
+ -- ap-×-fst _ _ id = id
+
+ -- ap-×-snd : {A B : Set} {N M : A} -> (f : A -> B) -> (y : B) -> (α : M ≃ N) ->
+ -- ap (λ x → y , f (x)) α ≃
+ -- nondep-pair≃ (ap (λ _ → y) α) (ap (λ x → f (x)) α)
+ -- ap-×-snd _ _ id = id
+
+ module ThreeCells where
+
+ pair≃3 : {A B : Set} {p q : A × B}
+ {α1 α2 : Id (fst p) (fst q)}
+ {β1 β2 : Id (snd p) (snd q)}
+ -> α1 ≃ α2
+ -> β1 ≃ β2
+ -> (pair≃ α1 β1) ≃ (pair≃ α2 β2)
+ pair≃3 a b = ap2 pair≃ a b
+
+ fst≃3 : {A B : Set} {p q : A × B} {α β : p ≃ q}
+ -> α ≃ β
+ -> fst≃ α ≃ fst≃ β
+ fst≃3 a = ap fst≃ a
+
+ snd≃3 : {A B : Set} {p q : A × B} {α β : p ≃ q}
+ -> α ≃ β
+ -> snd≃ α ≃ snd≃ β
+ snd≃3 a = ap snd≃ a
+
+ ×β3-1 : {A B : Set} {p q : A × B}
+ {α1 α2 : Id (fst p) (fst q)}
+ {β1 β2 : Id (snd p) (snd q)}
+ (γ : α1 ≃ α2)
+ (γ' : β1 ≃ β2)
+ -> fst≃3 (pair≃3 γ γ') ≃ ! (×≃β1 α2 β2) ∘ γ ∘ ×≃β1 α1 β1
+ ×β3-1 γ γ' = {!ap2-ap (λ≃ \ x -> λ≃ \ y -> ×≃β1 x y) γ γ' !} ∘ ! (ap-ap2-o fst≃ pair≃ γ γ')
View
114 homotopy/HigherHomotopyAbelian.agda
@@ -0,0 +1,114 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open Paths
+open
+
+module homotopy.HigherHomotopyAbelian (A : Set) (base : A) where
+
+ Ω1 : Set
+ Ω1 = base ≃ base
+
+ Ω2 : Set
+ Ω2 = Path{Ω1} id id
+
+ _⊙_ : Ω2 Ω2 Ω2
+ a ⊙ b = ap∘ a b
+
+ ⊙-unit-l : (p : Ω2) (id ⊙ p) ≃ p
+ ⊙-unit-l p = ∘-unit-l p ∘ ap∘-unit-l p -- because we know the base is id, the adjustment cancels
+
+ ⊙-unit-r : (a : Ω2) (a ⊙ id) ≃ a
+ ⊙-unit-r a = ap∘-unit-r a
+
+ interchange : (a b c d : _) ((a ∘ b) ⊙ (c ∘ d)) ≃ ((a ⊙ c) ∘ (b ⊙ d))
+ interchange a b c d = ichange-type d c b a
+
+ same : (a b : Ω2) (a ∘ b) ≃ (a ⊙ b)
+ same a b = (( a ∘ b) ≃〈 ap (λ x x ∘ b) (! (⊙-unit-r a)) 〉
+ ((a ⊙ id) ∘ b) ≃〈 ap (λ x (a ⊙ id) ∘ x) (! (⊙-unit-l b)) 〉
+ ((a ⊙ id) ∘ (id ⊙ b)) ≃〈 ! (interchange a id id b) 〉
+ ((a ∘ id) ⊙ (id ∘ b)) ≃〈 ap (λ x x ⊙ (id ∘ b)) (∘-unit-r a) 〉
+ (a ⊙ (id ∘ b)) ≃〈 ap (λ x a ⊙ x) (∘-unit-l b) 〉
+ (a ⊙ b)
+ ∎)
+
+ abelian : (a b : Ω2) (a ∘ b) ≃ (b ∘ a)
+ abelian a b = (a ∘ b) ≃〈 ap (λ x x ∘ b) (! (⊙-unit-l a)) 〉
+ ((id ⊙ a) ∘ b) ≃〈 ap (λ x (id ⊙ a) ∘ x) (! (⊙-unit-r b)) 〉
+ ((id ⊙ a) ∘ (b ⊙ id)) ≃〈 ! (interchange id b a id) 〉
+ ((id ∘ b) ⊙ (a ∘ id)) ≃〈 ap (λ x x ⊙ (a ∘ id)) (∘-unit-l b) 〉
+ (b ⊙ (a ∘ id)) ≃〈 ap (λ x b ⊙ x) (∘-unit-r a) 〉
+ (b ⊙ a) ≃〈 ! (same b a) 〉
+ (b ∘ a)
+ ∎
+
+ {-
+ -- for reference, this is the minimal generalization of the IH that goes through
+ -- for proving the interchange law
+ ichange : (p q : Ω1)
+ → (a : Path p q) (r : Ω1) (b : Path q r) (p' q' : Ω1)
+ (c : Path p' q') (r' : Ω1) (d : Path q' r')
+ → Path (aptrans (trans a b) (trans c d)) (trans (aptrans a c) (aptrans b d))
+ ichange p q a = jay
+ (λ p' q' a' →
+ (r : Ω1) (b : Path q' r) (p0 q0 : Ω1) (c : Path p0 q0) (r' : Ω1)
+ (d : Path q0 r') →
+ Path (aptrans (trans a' b) (trans c d))
+ (trans (aptrans a' c) (aptrans b d)))
+ a
+ (λ pq r b →
+ jay
+ (λ pq' r' b' →
+ (p' q' : Ω1) (c : Path p' q') (r0 : Ω1) (d : Path q' r0) →
+ Path (aptrans (trans id b') (trans c d))
+ (trans (aptrans id c) (aptrans b' d)))
+ b
+ (λ pqr p' q' c →
+ jay
+ (λ p0 q0 c' →
+ (r' : Ω1) (d : Path q0 r') →
+ Path (aptrans id (trans c' d))
+ (trans (aptrans id c') (aptrans id d)))
+ c
+ (λ p'q' r' d →
+ jay
+ (λ p'q0 r0 d' →
+ Path (aptrans id (trans id d'))
+ (trans id (aptrans id d')))
+ d (λ _ → id))))
+ -}
+
+ -- ENH: can you relax the restriction that the base point is identity?
+ -- abelian' : {loop : Path base base} {a b : Path loop loop} → Path (trans a b) (trans b a)
+
+ -- shorter proof by Favonia
+ module BifunctorLemma where
+
+ bifunctor-lemma : {A B C : Set}
+ (f : A -> B -> C)
+ {a a' : A} {b b' : B}
+ (α : a ≃ a') (β : b ≃ b')
+ -> (ap (\ x -> f a' x) β ∘ ap (\ x -> f x b) α)
+ ≃ (ap (\ x -> f x b') α ∘ ap (\ x -> f a x) β)
+ bifunctor-lemma f id id = id
+
+ bifunctor-lemma-∘ : (α β : Ω2)
+ -> (ap (\ x -> id ∘ x) β ∘ ap (\ x -> x ∘ id) α)
+ ≃ (ap (\ x -> x ∘ id) α ∘ ap (\ x -> id ∘ x) β)
+ bifunctor-lemma-∘ α β = bifunctor-lemma _∘_ {id} {id} {id} {id} α β
+
+ commute : (α β : Ω2) -> (α ∘ β) ≃ (β ∘ α)
+ commute α β = α ∘ β ≃〈 ap (λ f f α ∘ β) (! is-id-ap-2) 〉
+ ap (λ x x ∘ id) α ∘ β ≃〈 ap (λ f ap (λ x x ∘ id) α ∘ f β) (! is-id-ap-1) 〉
+ ap (λ x x ∘ id) α ∘ ap (λ x id ∘ x) β ≃〈 ! (bifunctor-lemma-∘ α β) 〉
+ ap (λ x id ∘ x) β ∘ ap (\ x -> x ∘ id) α ≃〈 ap (λ f f β ∘ ap (λ x x ∘ id) α) is-id-ap-1
+ β ∘ ap (\ x -> x ∘ id) α ≃〈 ap (λ f β ∘ f α) is-id-ap-2
+ β ∘ α ∎ where
+ is-id-ap-1 : ap (\ (x : Ω1) -> id ∘ x) ≃ (\ (x : Ω2) -> x)
+ is-id-ap-1 = λ≃ (\ x ∘-unit-l x ∘ ap-by-id (\ y ! (∘-unit-l y)) x)
+
+ is-id-ap-2 : ap (\ (x : Ω1) -> x ∘ id) ≃ (\ (x : Ω2) -> x)
+ is-id-ap-2 = λ≃ ap-id -- cancels definitionally on this side
+
+
View
49 homotopy/Hopf.agda
@@ -0,0 +1,49 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open import homotopy.HigherHomotopyAbelian
+open Paths
+
+module homotopy.Hopf where
+
+ module S² =1
+ open S²1
+
+ module A1 = homotopy.HigherHomotopyAbelian S² base
+
+ module Four where
+ ichange : Path {Path {Path base base} id id}
+ (ap∘ (loop ∘ loop) (loop ∘ loop))
+ (ap∘ loop loop ∘ ap∘ loop loop)
+ ichange = ichange-type loop loop loop loop
+
+ loop4 = ((loop ∘ loop) ∘ (loop ∘ loop))
+
+ nontriv-loop4 : loop4 ≃ loop4
+ nontriv-loop4 = loop4 ≃〈 A1.same (loop ∘ loop) (loop ∘ loop) 〉
+ ap∘ (loop ∘ loop) (loop ∘ loop) ≃〈 ichange 〉
+ ap∘ loop loop ∘ ap∘ loop loop ≃〈 ap2 _∘_ (! (A1.same loop loop)) (! (A1.same loop loop)) 〉
+ loop4 ∎
+
+ ap∘-inv-r : (a : id{_}{base} ≃ id{_}{base})
+ -> ap∘ a (! a) ≃ id
+ ap∘-inv-r a = !-inv-r a ∘ ! (A1.same a (! a))
+
+ ap∘-inv-l : (a : id{_}{base} ≃ id{_}{base})
+ -> ap∘ (! a) a ≃ id
+ ap∘-inv-l a = !-inv-l a ∘ ! (A1.same (! a) a)
+
+ nontriv : Path {Path {Path base base} id id} id id
+ nontriv = id ≃〈 ! (ap2 ap∘ (!-inv-r loop) (!-inv-r loop)) 〉
+ ap∘ (loop ∘ ! loop) (loop ∘ ! loop) ≃〈 ichange-type (! loop) loop (! loop) loop 〉
+ ap∘ loop loop ∘ ap∘ (! loop) (! loop) ≃〈 ! (ap2 (λ x y x ∘ y) (A1.same loop loop) (A1.same (! loop) (! loop))) 〉
+ (loop ∘ loop) ∘ ! loop ∘ ! loop ≃〈 ap (λ x (loop ∘ loop) ∘ x) (! (!-∘ loop loop)) 〉
+ (loop ∘ loop) ∘ ! (loop ∘ loop) ≃〈 !-inv-r (loop ∘ loop) 〉
+ (id ∎)
+
+ module S³ =1
+ openusing (S³)
+
+ hopf-map : S³ -> S²
+ hopf-map = S³.S³-rec S².base nontriv
+
View
62 homotopy/Pi1Either.agda
@@ -0,0 +1,62 @@
+
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open Paths
+
+module homotopy.Pi1Either where
+
+module CaseForInl (A : Type) (B : Type) (a : A) where
+
+ Cover : Either A B -> Type
+ Cover (Inl a') = Path a a'
+ Cover (Inr _) = Void
+
+ encode : {e : Either A B} -> Path (Inl a) e -> Cover e
+ encode α = transport Cover α id
+
+ inj : {a' : A} Path (Inl a) (Inl a') Path a a'
+ inj {a'} = encode {Inl a'}
+
+ dis : {b : B} Path (Inl a) (Inr b) Void
+ dis {b} = encode {Inr b}
+
+ decode : {e : Either A B} Cover e Path (Inl a) e
+ decode {Inl a'} α = ap Inl α
+ decode {Inr _} ()
+
+ encode-decode : {e : Either A B} (c : Cover e)
+ encode{e} (decode{e} c) ≃ c
+ encode-decode {Inl a'} α =
+ encode{Inl a'} (decode{Inl a'} α) -- (1)
+ ≃〈 id 〉
+ transport Cover (ap Inl α) id -- (2)
+ ≃〈 ap≃ (! (transport-ap-assoc' Cover Inl α)) 〉
+ transport (Cover o Inl) α id -- (3)
+ ≃〈 id 〉
+ transport (λ a' Id a a') α id -- (4)
+ ≃〈 transport-Path-right α id 〉
+ α ∘ id -- (5)
+ ≃〈 id 〉
+ α ∎ -- (6)
+ encode-decode {Inr _} ()
+
+ decode-encode : {e : Either A B} (α : Path (Inl a) e)
+ Path (decode{e} (encode{e} α)) α
+ decode-encode {e} α =
+ path-induction
+ (λ e' α' -> Path (decode{e'} (encode{e'} α')) α')
+ id α
+
+ eq : {e : Either A B} -> Path (Path (Inl a) e) (Cover e)
+ eq{e} = ua (improve
+ (hequiv encode decode
+ decode-encode (encode-decode{e})))
+
+ injEquiv : {a' : A}
+ Path (Path{Either A B} (Inl a) (Inl a')) (Path a a')
+ injEquiv = eq
+
+ disEquiv : {b : B}
+ Path (Path{Either A B} (Inl a) (Inr b)) Void
+ disEquiv = eq
View
160 homotopy/Pi1S1.agda
@@ -0,0 +1,160 @@
+
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open Paths
+open
+open Int
+
+module homotopy.Pi1S1 where
+
+ Cover : Type
+ Cover x = S¹-rec Int (ua succEquiv) x
+
+ transport-Cover-loop : Path (transport Cover loop) succ
+ transport-Cover-loop =
+ transport Cover loop
+ ≃〈 transport-ap-assoc Cover loop 〉
+ transport (λ x x) (ap Cover loop)
+ ≃〈 ap (transport (λ x x))
+ (βloop/rec Int (ua succEquiv)) 〉
+ transport (λ x x) (ua succEquiv)
+ ≃〈 transport-ua _ 〉
+ succ ∎
+
+ transport-Cover-!loop : Path (transport Cover (! loop)) pred
+ transport-Cover-!loop =
+ transport Cover (! loop)
+ ≃〈 transport-ap-assoc Cover (! loop) 〉
+ transport (λ x x) (ap Cover (! loop))
+ ≃〈 ap (transport (λ x x)) (ap-! Cover loop)〉
+ transport (λ x x) (! (ap Cover loop))
+ ≃〈 ap (λ y transport (λ x x) (! y))
+ (βloop/rec Int (ua succEquiv)) 〉
+ transport (λ x x) (! (ua succEquiv))
+ ≃〈 ap (transport (λ x x)) (!-ua succEquiv) 〉
+ transport (λ x x) (ua (!equiv succEquiv))
+ ≃〈 transport-ua _ 〉
+ pred ∎
+
+ encode : {x : S¹} Path base x Cover x
+ encode α = transport Cover α Zero
+
+ encode' : Path base base Int
+ encode' α = encode {base} α
+
+ loop^ : Int Path base base
+ loop^ Zero = id
+ loop^ (Pos One) = loop
+ loop^ (Pos (S n)) = loop ∘ loop^ (Pos n)
+ loop^ (Neg One) = ! loop
+ loop^ (Neg (S n)) = ! loop ∘ loop^ (Neg n)
+
+ loop^-preserves-pred
+ : (n : Int) Path (loop^ (pred n)) (! loop ∘ loop^ n)
+ loop^-preserves-pred (Pos One) = ! (!-inv-l loop)
+ loop^-preserves-pred (Pos (S y)) =
+ ! (∘-assoc (! loop) loop (loop^ (Pos y)))
+ ∘ ! (ap (λ x x ∘ loop^ (Pos y)) (!-inv-l loop))
+ ∘ ! (∘-unit-l (loop^ (Pos y)))
+ loop^-preserves-pred Zero = id
+ loop^-preserves-pred (Neg One) = id
+ loop^-preserves-pred (Neg (S y)) = id
+
+ decode : {x : S¹} Cover x Path base x
+ decode {x} =
+ S¹-induction
+ (λ x' Cover x' Path base x')
+ loop^
+ (transport (λ x' Cover x' Path base x') loop loop^ ≃〈 transport-→ Cover (Path base) loop loop^ 〉
+
+ transport (λ x' Path base x') loop
+ o loop^
+ o transport Cover (! loop) ≃〈 λ≃ (λ y transport-Path-right loop (loop^ (transport Cover (! loop) y))) 〉
+
+ (λ p loop ∘ p)
+ o loop^
+ o transport Cover (! loop) ≃〈 λ≃ (λ y ap (λ x' loop ∘ loop^ x') (ap≃ transport-Cover-!loop)) 〉
+
+ (λ p loop ∘ p)
+ o loop^
+ o pred ≃〈 id 〉
+
+ (λ n loop ∘ (loop^ (pred n))) ≃〈 λ≃ (λ y move-left-! _ loop (loop^ y) (loop^-preserves-pred y)) 〉
+
+ (λ n loop^ n)
+ ∎)
+ x
+
+ encode-loop^ : (n : Int) Path (encode (loop^ n)) n
+ encode-loop^ Zero = id
+ encode-loop^ (Pos One) = ap≃ transport-Cover-loop
+ encode-loop^ (Pos (S n)) =
+ encode (loop^ (Pos (S n)))
+ ≃〈 id 〉
+ transport Cover (loop ∘ loop^ (Pos n)) Zero
+ ≃〈 ap≃ (transport-∘ Cover loop (loop^ (Pos n))) 〉
+ transport Cover loop
+ (transport Cover (loop^ (Pos n)) Zero)
+ ≃〈 ap≃ transport-Cover-loop 〉
+ succ (transport Cover (loop^ (Pos n)) Zero)
+ ≃〈 id 〉
+ succ (encode (loop^ (Pos n)))
+ ≃〈 ap succ (encode-loop^ (Pos n)) 〉
+ succ (Pos n) ∎
+ encode-loop^ (Neg One) = ap≃ transport-Cover-!loop
+ encode-loop^ (Neg (S n)) =
+ transport Cover (! loop ∘ loop^ (Neg n)) Zero
+ ≃〈 ap≃ (transport-∘ Cover (! loop) (loop^ (Neg n))) 〉
+ transport Cover (! loop) (transport Cover (loop^ (Neg n)) Zero)
+ ≃〈 ap≃ transport-Cover-!loop 〉
+ pred (transport Cover (loop^ (Neg n)) Zero)
+ ≃〈 ap pred (encode-loop^ (Neg n)) 〉
+ pred (Neg n) ∎
+
+ encode-decode : {x : S¹} (c : Cover x)
+ Path (encode (decode{x} c)) c
+ encode-decode {x} = S¹-induction
+ (\ (x : S¹) (c : Cover x)
+ Path (encode{x} (decode{x} c)) c)
+ encode-loop^ hedberg x where
+ postulate hedberg : _
+
+ decode-encode : {x : S¹} (α : Path base x)
+ Path (decode (encode α)) α
+ decode-encode {x} α =
+ path-induction
+ (λ (x' : S¹) (α' : Path base x')
+ Path (decode (encode α')) α')
+ id α
+
+ all-loops : (α : Path base base) Path α (loop^ (encode α))
+ all-loops α = ! (decode-encode α)
+
+ Ω₁[S¹]-is-Int : HEquiv (Path base base) Int
+ Ω₁[S¹]-is-Int =
+ hequiv encode decode decode-encode encode-loop^
+
+ loop^-preserves-succ : (n : Int)
+ Path (loop^ (succ n)) (loop ∘ loop^ n)
+ loop^-preserves-succ n =
+ loop^ (succ n)
+ ≃〈 move-right-! loop (loop^ (succ n)) _
+ (! (loop^-preserves-pred (succ n))) 〉
+ loop ∘ (loop^ (pred (succ n)))
+ ≃〈 ap (λ x loop ∘ loop^ x) (pred-succ n) 〉
+ loop ∘ (loop^ n) ∎
+
+ preserves-composition : (n m : Int)
+ Path (loop^ (n + m)) (loop^ n ∘ loop^ m)
+ preserves-composition (Pos One) m = loop^-preserves-succ m
+ preserves-composition (Pos (S n)) m =
+ ∘-assoc loop (loop^ (Pos n)) (loop^ m)
+ ∘ ap (λ x loop ∘ x) (preserves-composition (Pos n) m)
+ ∘ loop^-preserves-succ (Pos n + m)
+ preserves-composition Zero m = ! (∘-unit-l _)
+ preserves-composition (Neg One) m = loop^-preserves-pred m
+ preserves-composition (Neg (S n)) m =
+ ∘-assoc (! loop) (loop^ (Neg n)) (loop^ m)
+ ∘ ap (λ x ! loop ∘ x) (preserves-composition (Neg n) m)
+ ∘ loop^-preserves-pred (Neg n + m)
View
90 homotopy/Pi1T.agda
@@ -0,0 +1,90 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open Paths
+open T
+open Int
+
+module homotopy.Pi1T where
+
+ U = Set
+
+ C : T -> U
+ C = T-rec (Int × Int) (ap (λ x x × Int) (ua succEquiv)) (ap (λ y Int × y) (ua succEquiv)) {!!}
+
+{-
+ subst-C-loop : subst C loop ≃ succ
+ subst-C-loop =
+ subst C loop ≃〈 subst-resp C loop 〉
+ subst (λ x → x) (resp C loop) ≃〈 resp (subst (λ x → x)) (βloop/rec Int succ≃) 〉
+ subst (λ x → x) succ≃ ≃〈 subst-univ _ 〉
+ succ ∎
+
+ subst-C-!loop : subst C (! loop) ≃ pred
+ subst-C-!loop =
+ subst C (! loop) ≃〈 subst-resp C (! loop) 〉
+ subst (λ x → x) (resp C (! loop)) ≃〈 resp (subst (λ x → x)) (resp-! C loop)〉
+ subst (λ x → x) (! (resp C loop)) ≃〈 resp (λ y → subst (λ x → x) (! y)) (βloop/rec Int succ≃) 〉
+ subst (λ x → x) (! succ≃) ≃〈 resp (subst (λ x → x)) succ≃-! 〉
+ subst (λ x → x) pred≃ ≃〈 subst-univ _ 〉
+ pred ∎
+-}
+
+ _^_ : (base ≃ base) -> Int -> base ≃ base
+ α ^ Zero = id
+ α ^ (Pos One) = α
+ α ^ (Pos (S n)) = α ∘ (α ^ (Pos n))
+ α ^ (Neg One) = ! α
+ α ^ (Neg (S n)) = ! α ∘ (α ^ (Neg n))
+
+ decode' : (Int × Int) -> base ≃ base
+ decode' (m , n) = (loop₁ ^ m) ∘ (loop₂ ^ n)
+
+ encode : {x : T} -> base ≃ x -> C x
+ encode p = transport C p (Zero , Zero)
+
+ encode-loop^ : (p : Int × Int) -> encode (decode' p) ≃ p
+ encode-loop^ (m , n) = {!!} ∘ ap≃ (transport-∘ C (loop₁ ^ m) (loop₂ ^ n)) {Zero , Zero}
+
+ -- stuck : {p : base ≃ base} -> p ≃ loop^ (encode p)
+ -- stuck = {!!} -- no way to use J directly; need to generalize
+
+{-
+ shift : (n : Int) -> (loop ∘ (loop^ (pred n))) ≃ loop^ n
+ shift (Pos Z) = Refl
+ shift (Pos (S y)) = Refl
+ shift Zero = !-inv-r loop
+ shift (Neg Z) =
+ ∘-unit-l _ ∘
+ resp (\ x → x ∘ ! loop) (!-inv-r loop)
+ ∘ ∘-assoc loop (! loop) (! loop)
+ shift (Neg (S y)) =
+ loop ∘ ! loop ∘ ! loop ∘ loop^ (Neg y) ≃〈 ∘-assoc loop (! loop) (! loop ∘ loop^ (Neg y)) 〉
+ (loop ∘ ! loop) ∘ ! loop ∘ loop^ (Neg y) ≃〈 resp (λ x → x ∘ ! loop ∘ loop^ (Neg y)) (!-inv-r loop) 〉
+ Refl ∘ ! loop ∘ loop^ (Neg y) ≃〈 ∘-unit-l _ 〉
+ (! loop ∘ loop^ (Neg y) ∎)
+-}
+
+ decode : {x : T} -> C x -> base ≃ x
+ decode {a} =
+ T-elim {\ x -> C x -> base ≃ x}
+ decode'
+ c1
+ c2
+ {!!}
+ a where
+ postulate
+ c1 : _
+ c2 : _
+
+ decode-encode : {a} -> (p : base ≃ a) -> decode (encode p) ≃ p
+ decode-encode {a} p =
+ path-induction (λ a' (p' : base ≃ a') decode (encode p') ≃ p') id p
+
+{-
+ theorem : Id base base ≃ Int
+ theorem = ua (isoToAdj (encode , isiso decode encode-loop^ decode-encode))
+-}
+
+
+
View
133 lib/AdjointEquiv.agda
@@ -1,62 +1,105 @@
{-# OPTIONS --type-in-type --without-K #-}
+open import lib.First
open import lib.Paths
open import lib.Prods
open Paths
module lib.AdjointEquiv where
- -- FIXME: clean up the notation here
-
- record IsAEq {A B : Set} (f : A -> B) : Set where
- constructor isadj
- field
- g : B -> A
- α : (y : _) -> Id (f (g y)) y
- β : (x : _) -> Id (g (f x)) x
- γ : (x : _) Id (α (f x)) (resp fx))
-
- AEq : Set -> Set -> Set
- AEq A B = Σ \ (f : A -> B) -> IsAEq f
-
- _·⊢_ : {A B} -> AEq A B -> A -> B
- _·⊢_ = fst
-
- _·⊣_ : {A B} -> AEq A B -> B -> A
- (_ , isadj g _ _ _) ·⊣ x = g x
-
- record IsIso {A B : Set} (f : A -> B) : Set where
- constructor isiso
- field
- g : B -> A
- α : (y : _) -> Id (f (g y)) y
- β : (x : _) -> Id (g (f x)) x
-
- Iso : Set -> Set -> Set
- Iso A B = Σ \ (f : A -> B) -> IsIso f
-
- isoToAdj : {A B} -> Iso A B -> AEq A B
- isoToAdj (f , isiso g α β) = (f , isadj g α improveβ improveδ) where
- postulate improveβ : _
- improveδ : _
-
- id⊣ : {A} -> AEq A A
- id⊣ = ( (\ x -> x) , isadj (λ x x) (\ _ -> Refl) (\ _ -> Refl) (\ _ -> Refl))
-
- comp : {A B C} -> AEq A B -> AEq B C -> AEq A C
- comp a1 a2 = (λ x a2 ·⊢ (a1 ·⊢ x)) , isadj (λ y a1 ·⊣ (a2 ·⊣ y)) FIXME1 FIXME2 FIXME3 where
+ record IsEquiv {A B : Type} (f : A → B) : Type where
+ constructor isequiv
+ field
+ g : B A
+ α : (x : A) Path (g (f x)) x
+ β : (y : B) Path (f (g y)) y
+ γ : (x : A) Path (β (f x)) (ap f (α x)) -- coherence condition necessary for higher spaces
+ -- also satifies:
+ -- (y : B) → Path (α (g y)) (ap gy));
+ -- this is just γ with f<→g and α<→β, so we'll prove this in
+ -- the process of defining !-equiv below
+
+ Equiv : Type -> Type -> Type
+ Equiv A B = Σ (IsEquiv{A}{B})
+
+ equiv : {A B : Type}
+ (f : A B)
+ (g : B A)
+ (α : (x : A) Path (g (f x)) x)
+ : (y : B) Path (f (g y)) y)
+ (γ : (x : A) Path (β (f x)) (ap f (α x)))
+ Equiv A B
+ equiv f g α β γ = f , isequiv g α β γ
+
+ inverses-natural : {A B} (f : A B) (g : B A) (η : (x : A) Path (g (f x)) x)
+ {x : A}
+ Path (η (g (f x))) (ap (g o f) (η x))
+ inverses-natural f g η {x} =
+ (∘-unit-l _ ∘ ap (λ y y ∘ ap (λ x' g (f x')) (η x)) (!-inv-l (η x))) ∘
+ ap (λ a (! a ∘ η x) ∘ ap (g o f) (η x)) (ap-id (η x)) ∘
+ move-right-right-! (η (g (f x))) (ap (λ x' g (f x')) (η x)) _
+ (move-right (ap (λ x' x') (η x)) (η (g (f x)) ∘ ! (ap (λ x' g (f x')) (η x))) _
+ (apd η (η x) ∘ ! (transport-Path (g o f) (λ x' x') (η x) (η (g (f x))))))
+
+ id-equiv : {A} -> Equiv A A
+ id-equiv = ( (\ x -> x) , isequiv (λ x x) (\ _ -> id) (\ _ -> id) (\ _ -> id))
+
+ _∘equiv_ : {A B C} -> Equiv B C Equiv A B -> Equiv A C
+ _∘equiv_ (f , isequiv g α β γ) (f' , isequiv g' α' β' γ') = (f o f') , isequiv (g' o g) FIXME1 FIXME2 FIXME3 where
postulate
FIXME1 : _
FIXME2 : _
FIXME3 : _
- aeq-inv : {A B} -> AEq A B -> AEq B A
- aeq-inv (f , isadj g α β δ) = g , isadj f β α FIXME1 where
- postulate
- FIXME1 : _
+ !equiv : {A B} Equiv A B Equiv B A
+ !equiv (f , isequiv g α β γ) =
+ equiv g f β α
+ (λ y α (g y) ≃〈 ! (∘-assoc (α (g y)) (ap (λ x g (f x)) (α (g y))) (! (α (g (f (g y)))))) ∘ move-right-right-! (α (g y)) (! (α (g (f (g y))))) _ (move-right-! (α (g y)) (α (g y) ∘ ! (! (α (g (f (g y)))))) _ (! (ap-by-id (λ x ! (α x)) (α (g y))))) 〉
+ α (g y) ∘ ap (g o f) (α (g y)) ∘ ! (α (g (f (g y)))) ≃〈 ap (λ a α (g y) ∘ a ∘ ! (α (g (f (g y))))) (ap (ap g) (! (γ (g y))) ∘ ap-o g f (α (g y))) 〉
+ α (g y) ∘ ap g (β (f (g y))) ∘ ! (α (g (f (g y)))) ≃〈 ap (λ a α (g y) ∘ ap g a ∘ ! (α (g (f (g y))))) (inverses-natural g f β) 〉
+ α (g y) ∘ ap g (ap (f o g) (β y)) ∘ ! (α (g (f (g y)))) ≃〈 ap (λ a α (g y) ∘ a ∘ ! (α (g (f (g y))))) (ap-o (g o f) g (β y) ∘ ! (ap-o g (f o g) (β y))) 〉
+ α (g y) ∘ ap (g o f) (ap g (β y)) ∘ ! (α (g (f (g y)))) ≃〈 ap (λ a α (g y) ∘ a ∘ ! (α (g (f (g y))))) (ap (λ a ! (α (g y)) ∘ ap g (β y) ∘ a) (!-invol (α (g (f (g y))))) ∘ ap-by-id (λ x ! (α x)) (ap g (β y))) 〉
+ α (g y) ∘ (! (α (g y)) ∘ (ap g (β y)) ∘ α (g (f (g y)))) ∘ ! (α (g (f (g y)))) ≃〈 rassoc-1-3-1 (α (g y)) (! (α (g y))) (ap g (β y)) (α (g (f (g y)))) (! (α (g (f (g y)))))〉
+ α (g y) ∘ ! (α (g y)) ∘ (ap g (β y)) ∘ α (g (f (g y))) ∘ ! (α (g (f (g y)))) ≃〈 !-inv-r-front _ _ 〉
+ (ap g (β y)) ∘ α (g (f (g y))) ∘ ! (α (g (f (g y)))) ≃〈 !-inv-r-back (ap g (β y)) (α (g (f (g y)))) 〉
+ (ap g (β y) ∎))
+
+
+ record IsHEquiv {A B : Type} (f : A → B) : Type where
+ constructor ishequiv
+ field
+ g : B A
+ α : (x : A) Path (g (f x)) x
+ β : (y : B) Path (f (g y)) y
+
+ HEquiv : Type Type Type
+ HEquiv A B = Σ (IsHEquiv{A}{B})
+
+ hequiv : {A B : Type}
+ (f : A B)
+ (g : B A)
+ (α : (x : A) Path (g (f x)) x)
+ (β : (y : B) Path (f (g y)) y)
+ HEquiv A B
+ hequiv f g α β = f , ishequiv g α β
+
+ improve : {A B : Type} HEquiv A B Equiv A B
+ improve (f , ishequiv g η ξ) =
+ equiv f g
+ η
+ (λ x ξ x ∘ ap f (η (g x)) ∘ ap (f o g) (! (ξ x)))
+ (λ x ξ (f x) ∘ ap f (η (g (f x))) ∘ ap (f o g) (! (ξ (f x))) ≃〈 ap (λ a ξ (f x) ∘ ap f a ∘ ap (f o g) (! (ξ (f x)))) (inverses-natural f g η) 〉
+ ξ (f x) ∘ ap f (ap (g o f) (η x)) ∘ ap (f o g) (! (ξ (f x))) ≃〈 ap (λ a ξ (f x) ∘ a ∘ ap (f o g) (! (ξ (f x)))) (ap-o (f o g) f (η x) ∘ ! (ap-o f (g o f) (η x))) 〉
+ ξ (f x) ∘ ap (f o g) (ap f (η x)) ∘ ap (f o g) (! (ξ (f x))) ≃〈 ap (λ a ξ (f x) ∘ a ∘ ap (f o g) (! (ξ (f x)))) (ap (λ a ! (ξ (f x)) ∘ ap f (η x) ∘ a) (!-invol (ξ (f (g (f x))))) ∘ ap-by-id (λ x' ! (ξ x')) (ap f (η x))) 〉
+ ξ (f x) ∘ (! (ξ (f x)) ∘ (ap f (η x)) ∘ ξ (f (g (f x)))) ∘ ap (f o g) (! (ξ (f x))) ≃〈 rassoc-1-3-1 (ξ (f x)) (! (ξ (f x))) (ap f (η x)) (ξ (f (g (f x)))) (ap (f o g) (! (ξ (f x)))) 〉
+ ξ (f x) ∘ ! (ξ (f x)) ∘ (ap f (η x)) ∘ ξ (f (g (f x))) ∘ ap (f o g) (! (ξ (f x))) ≃〈 !-inv-r-front (ξ (f x)) (ap f (η x) ∘ ξ (f (g (f x))) ∘ ap (f o g) (! (ξ (f x)))) 〉
+ (ap f (η x)) ∘ ξ (f (g (f x))) ∘ ap (f o g) (! (ξ (f x))) ≃〈 ap (λ a ap f (η x) ∘ a ∘ ap (f o g) (! (ξ (f x)))) (inverses-natural g f ξ) 〉
+ (ap f (η x)) ∘ ap (f o g) (ξ ((f x))) ∘ ap (f o g) (! (ξ (f x))) ≃〈 ap (λ a ap f (η x) ∘ ap (f o g) (ξ (f x)) ∘ a) (ap-! (f o g) (ξ (f x))) 〉
+ (ap f (η x)) ∘ ap (f o g) (ξ ((f x))) ∘ ! (ap (f o g) (ξ (f x))) ≃〈 ap (λ a ap f (η x) ∘ a) (!-inv-r (ap (f o g) (ξ (f x)))) 〉
+ (ap f (η x) ∎))
- subst-is-AEq : {A B : Set} (α : A ≃ B) -> IsAEq (subst (\ x -> x) α)
- subst-is-AEq Refl = snd id
+ transport-is-Equiv : {A B : Set} (α : A ≃ B) -> IsEquiv (transport (\ x -> x) α)
+ transport-is-Equiv id = snd id-equiv
-- depending on where in the computational interpretation this happens,
-- we might need to write this out by hand, but that works too
-- isadj (subst (λ x → x) (! α)) {!!} {!!} {!!}
View
12 lib/BasicTypes.agda
@@ -2,17 +2,19 @@
module lib.BasicTypes where
+ open import lib.First public
open import lib.Paths public
- open import lib.AdjointEquiv public
- open import lib.Univalence public
- open import lib.WEq public
open import lib.Prods public
- open import lib.Bool public
open import lib.Functions public
+ open import lib.AdjointEquiv public
+ open import lib.Sums public
+ open import lib.Bool public
open import lib.Nat public
open import lib.Int public
open import lib.Maybe public
- open import lib.Sums public
open import lib.List public
open import lib.Monoid public
+ open import lib.WEq public
+ open import lib.Univalence public
+
View
63 lib/Bool.agda
@@ -1,5 +1,6 @@
{-# OPTIONS --type-in-type #-}
+open import lib.First
open import lib.Paths
open import lib.Prods
open import lib.Functions
@@ -8,62 +9,62 @@ open Paths
module lib.Bool where
- data Bool : Set where
+ data Bool : Type where
True : Bool
False : Bool
{-# COMPILED_DATA Bool Bool True False #-}
module BoolM where
- if_/_then_else : (p : Bool -> Set) -> (b : Bool) -> p True -> p False -> p b
+ if_/_then_else : (p : Bool -> Type) -> (b : Bool) -> p True -> p False -> p b
if _ / True then b1 else b2 = b1
if _ / False then b1 else b2 = b2
- aborttf : {A : Set}
+ aborttf : {A : Type}
-> True ≃ False -> A
- aborttf{A} α = subst
+ aborttf{A} α = transport
(λ x
- if (λ _ Set) / x then Unit else A)
+ if (λ _ Type) / x then Unit else A)
α <>
- subst-if : {A B : Set} {M N : Bool} ->
- subst (\ x -> if (\ _ -> Set) / x then A else B)
+ transport-if : {A B : Type} {M N : Bool} ->
+ transport (\ x -> if (\ _ -> Type) / x then A else B)
≃ (if
(λ M'
M' ≃ N ->
- if (λ _ Set) / M' then A else B
- if (λ _ Set) / N then A else B)
+ if (λ _ Type) / M' then A else B
+ if (λ _ Type) / N then A else B)
/ M
- then if (λ N' Id True N' A if (λ _ Set) / N' then A else B) / N
+ then if (λ N' Path True N' A if (λ _ Type) / N' then A else B) / N
then (λ _ x x)
else (λ α _ aborttf α)
- else (if (λ N' Id False N' B if (λ _ Set) / N' then A else B) / N
+ else (if (λ N' Path False N' B if (λ _ Type) / N' then A else B) / N
then (λ α _ aborttf (! α))
else (λ _ x x)))
- subst-if {A}{B}{M}{N}= λ≃ pf where
- pf : {M N} -> (α : Id M N)
- -> Id (subst (λ x if (λ _ Set) / x then A else B) α)
+ transport-if {A}{B}{M}{N}= λ≃ pf where
+ pf : {M N} -> (α : Path M N)
+ -> Path (transport (λ x if (λ _ Type) / x then A else B) α)
((if
(λ M'
M' ≃ N ->
- if (λ _ Set) / M' then A else B
- if (λ _ Set) / N then A else B)
+ if (λ _ Type) / M' then A else B
+ if (λ _ Type) / N then A else B)
/ M
- then if (λ N' Id True N' A if (λ _ Set) / N' then A else B) / N
+ then if (λ N' Path True N' A if (λ _ Type) / N' then A else B) / N
then (λ _ x x)
else (λ α _ aborttf α)
- else (if (λ N' Id False N' B if (λ _ Set) / N' then A else B) / N
+ else (if (λ N' Path False N' B if (λ _ Type) / N' then A else B) / N
then (λ α _ aborttf (! α))
else (λ _ x x))) α)
- pf {M} {.M} Refl with M
- ... | True = Refl
- ... | False = Refl
+ pf {M} {.M} id with M
+ ... | True = id
+ ... | False = id
- Check : Bool -> Set
+ Check : Bool -> Type
Check True = Unit
Check False = Void
- check : (b : Bool) -> Either (Check b) (Id b False)
- check False = Inr Refl
+ check : (b : Bool) -> Either (Check b) (Path b False)
+ check False = Inr id
check True = Inl <>
_andalso_ : Bool -> Bool -> Bool
@@ -82,8 +83,8 @@ module lib.Bool where
check-andE {False} ()
check-andE {True} {False} ()
- check-id-not : {b1 : Bool} -> Id b1 False -> Check (if (\ _ -> Bool) / b1 then False else True)
- check-id-not Refl = _
+ check-id-not : {b1 : Bool} -> Path b1 False -> Check (if (\ _ -> Bool) / b1 then False else True)
+ check-id-not id = _
check-noncontra : (b : Bool) -> Check b -> Check (if (\ _ -> Bool) / b then False else True) -> Void
check-noncontra True _ v = v
@@ -94,11 +95,11 @@ module lib.Bool where
{-# BUILTIN FALSE False #-}
{-
- respif : {Γ : Set} {θ1 θ2 : Γ} {P : Id θ1 θ2} {C : Γ -> Bool -> Set} {M : Γ -> Bool} {M1 : (x : Γ) -> C x True} {M2 : (x : Γ) -> C x False}
- -> Id (respd (\ x -> if C x / (M x) then (M1 x) else (M2 x)) P)
- {!!} -- (if {!\ y -> Id (subst (\ x -> C x True)!} / M N' then respd M1 P else (respd M2 P))
+ respif : {Γ : Type} {θ1 θ2 : Γ} {P : Path θ1 θ2} {C : Γ -> Bool -> Type} {M : Γ -> Bool} {M1 : (x : Γ) -> C x True} {M2 : (x : Γ) -> C x False}
+ -> Path (respd (\ x -> if C x / (M x) then (M1 x) else (M2 x)) P)
+ {!!} -- (if {!\ y -> Path (transport (\ x -> C x True)!} / M N' then respd M1 P else (respd M2 P))
respif = {!!}
-}
--- true branch: Id (subst (λ x → C x True) P (M1 N)) (M1 N')
--- false branch: Id (subst (λ x → C x False) P (M2 N)) (M2 N')
+-- true branch: Path (transport (λ x → C x True) P (M1 N)) (M1 N')
+-- false branch: Path (transport (λ x → C x False) P (M2 N)) (M2 N')
View
10 lib/First.agda
@@ -0,0 +1,10 @@
+
+module lib.First where
+
+ -- Agda uses the word "Set" in a way that I want to suppress
+ Type = Set
+
+ _o_ : {A B C : Type} (B C) (A B) A C
+ g o f = \ x g (f x)
+ infixr 10 _o_
+
View
177 lib/Functions.agda
@@ -1,14 +1,11 @@
{-# OPTIONS --type-in-type --without-K --allow-unsolved-metas #-}
+open import lib.First
open import lib.Paths
open import lib.Prods
open Paths
module lib.Functions where
-
- _o_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
- g o f = \ x -> g (f x)
- infixr 10 _o_
-- interchange law for the type theory as a whole:
-- objects = types
@@ -19,137 +16,139 @@ module lib.Functions where
1' θ2' θ3' : Γ2 -> Γ3}
1 : θ1 ≃ θ2) (δ2 : θ2 ≃ θ3)
1' : θ1' ≃ θ2') (δ2' : θ2' ≃ θ3')
- -> resp2 _o_ (δ2' ∘ δ1') (δ2 ∘ δ1) ≃ resp2 _o_ δ2' δ2resp2 _o_ δ1' δ1
- ichange-theory Refl Refl Refl Refl = Refl
+ -> ap2 _o_ (δ2' ∘ δ1') (δ2 ∘ δ1) ≃ ap2 _o_ δ2' δ2ap2 _o_ δ1' δ1
+ ichange-theory id id id id = id
+ ap≃ : {A} {B : A Type} {f g : (x : A) B x}
+ Path f g {x : A} Path (f x) (g x)
+ ap≃ α {x} = ap (\ f f x) α
- app≃ : {A} {B : A -> Set} {f g : (x : A) -> B x}
- -> Id f g -> ({x : A} -> Id (f x) (g x))
- app≃ α {x} = resp (\ f -> f x) α
+ ap≃i : {A} {B : A -> Set} {f g : {x : A} -> B x}
+ -> Path (\ {x} -> f {x}) (\ {x} -> g {x}) -> ({x : A} -> Path (f {x}) (g {x}))
+ ap≃i α {x} = ap (\ f -> f {x}) α
- app≃i : {A} {B : A -> Set} {f g : {x : A} -> B x}
- -> Id (\ {x} -> f {x}) (\ {x} -> g {x}) -> ({x : A} -> Id (f {x}) (g {x}))
- app≃i α {x} = resp (\ f -> f {x}) α
+ -- apply a path to a 1-cell (path)
+ ap≃₁ : {A} {B : A -> Set} {f g : (x : A) -> B x}
+ -> Path f g -> ({x y : A} -> (α : Path x y) -> Path (transport B α (f x)) (g y))
+ ap≃₁ {A} {B} {f} {.f} id id = id
- app≃2 : {A} {B : A -> Set} {f g : (x : A) -> B x}
- -> Id f g -> ({x y : A} -> (α : Id x y) -> Id (subst B α (f x)) (g y))
- app≃2 {A} {B} {f} {.f} Refl Refl = Refl
-
- app≃2' : {A} {B : A -> Set} {f g : (x : A) -> B x}
- -> Id f g -> ({x y : A} -> (α : Id x y) -> Id (f x) (subst B (! α) (g y)))
- app≃2' {A} {B} {f} {.f} Refl Refl = Refl
+ ap≃₁' : {A} {B : A -> Set} {f g : (x : A) -> B x}
+ -> Path f g -> ({x y : A} -> (α : Path x y) -> Path (f x) (transport B (! α) (g y)))
+ ap≃₁' {A} {B} {f} {.f} id id = id
postulate
- λ≃ : {A} {B : A -> Set} {f g : (x : A) -> B x} -> ((x : A) -> Id (f x) (g x)) -> Id f g
+ λ≃ : {A} {B : A -> Set} {f g : (x : A) -> B x} -> ((x : A) -> Path (f x) (g x)) -> Path f g
Π≃η : {A} {B : A -> Set} {f g : (x : A) -> B x}
- -> (α : Id f g)
- -> α ≃ λ≃ (\ x -> app≃ α {x})
- Π≃β : {A} {B : A -> Set} {f g : (x : A) -> B x} -> (α : (x : A) -> Id (f x) (g x)) {N : A}
- -> app≃ (λ≃ α) {N} ≃ (α N)
-
- λ≃i : {A} {B : A -> Set} {f g : {x : A} -> B x} -> ((x : A) -> Id (f {x}) (g {x})) -> Id{ {x : A} -> B x } f g
-
- subst-→ : {Γ} (A B : Γ -> Set) {θ1 θ2 : Γ} (δ : θ1 ≃ θ2) (f : (A θ1) -> B θ1)
- -> subst (\ γ -> (A γ) -> B γ) δ f ≃ (\ y -> subst B δ (f (subst A (! δ) y)))
- subst-→ _ _ Refl f = Refl
-
- subst-→-pre : {C A B : Set} (δ : A ≃ B) (f : A -> C)
- -> subst (\ X -> X -> C) δ f ≃ (f o (subst (\ X -> X) (! δ)))
- subst-→-pre Refl f = Refl
-
- -- substitution extension for Γ,x:A⁻ in DTT
+ -> (α : Path f g)
+ -> α ≃ λ≃ (\ x -> ap≃ α {x})
+ Π≃β : {A} {B : A -> Set} {f g : (x : A) -> B x} -> (α : (x : A) -> Path (f x) (g x)) {N : A}
+ -> ap≃ (λ≃ α) {N} ≃ (α N)
+
+ λ≃i : {A} {B : A -> Set} {f g : {x : A} -> B x} -> ((x : A) -> Path (f {x}) (g {x})) -> Path{ {x : A} -> B x } f g
+
+ transport-→ : {Γ : Type} (A B : Γ Type) {θ1 θ2 : Γ}
+ (δ : θ1 ≃ θ2) (f : A θ1 B θ1)
+ Path (transport (\ γ (A γ) B γ) δ f)
+ (transport B δ o f o (transport A (! δ)))
+ transport-→ _ _ id f = id
+
+ transport-→-pre : {C A B : Set} (δ : A ≃ B) (f : A -> C)
+ -> transport (\ X -> X -> C) δ f ≃ (f o (transport (\ X -> X) (! δ)))
+ transport-→-pre id f = id
+
+ -- transportitution extension for Γ,x:A⁻ in DTT
pair≃⁻ : {A : Set} {B : A -> Set} {p q : Σ B}
- -> (α : (fst p) ≃ (fst q)) -> (snd p) ≃ subst B (! α) (snd q)
+ -> (α : (fst p) ≃ (fst q)) -> (snd p) ≃ transport B (! α) (snd q)
-> p ≃ q
pair≃⁻ {A}{B}{p}{q} α β =
- pair≃ α (app≃ (resp (λ x subst B x) (!-inv-r α) ∘ ! (subst-∘ B α (! α))) ∘ resp (subst B α) β)
+ pair≃ α (ap≃ (ap (λ x transport B x) (!-inv-r α) ∘ ! (transport-∘ B α (! α))) ∘ ap (transport B α) β)
- subst : {Γ} (A : Γ -> Set) (B : (γ : Γ) -> A γ -> Set)
+ transport : {Γ} (A : Γ -> Set) (B : (γ : Γ) -> A γ -> Set)
1 θ2 : Γ} (δ : θ1 ≃ θ2) (f : (x : A θ1) -> B θ1 x)
- -> subst (\ γ -> (x : A γ) -> B γ x) δ f ≃
- (\ x -> subst (\ (p : Σ \ (γ : Γ) -> A γ) -> B (fst p) (snd p))
- (pair≃⁻ δ Refl)
- (f (subst A (! δ) x)))
- subst-Π _ _ Refl f = Refl
+ -> transport (\ γ -> (x : A γ) -> B γ x) δ f ≃
+ (\ x -> transport (\ (p : Σ \ (γ : Γ) -> A γ) -> B (fst p) (snd p))
+ (pair≃⁻ δ id)
+ (f (transport A (! δ) x)))
+ transport-Π _ _ id f = id
- subst-Πi : {Γ} (A : Γ -> Set) (B : (γ : Γ) -> A γ -> Set)
+ transport-Πi : {Γ} (A : Γ -> Set) (B : (γ : Γ) -> A γ -> Set)
1 θ2 : Γ} (δ : θ1 ≃ θ2) (f : {x : A θ1} -> B θ1 x)
- -> Id{ {x : A θ2} -> B θ2 x}
- (subst (\ γ -> {x : A γ} -> B γ x) δ f)
- (\ {x} -> subst (\ (p : Σ \ (γ : Γ) -> A γ) -> B (fst p) (snd p))
- (pair≃⁻ δ Refl)
- (f {(subst A (! δ) x)}))
- subst-Πi _ _ Refl f = Refl
+ -> Path{ {x : A θ2} -> B θ2 x}
+ (transport (\ γ -> {x : A γ} -> B γ x) δ f)
+ (\ {x} -> transport (\ (p : Σ \ (γ : Γ) -> A γ) -> B (fst p) (snd p))
+ (pair≃⁻ δ id)
+ (f {(transport A (! δ) x)}))
+ transport-Πi _ _ id f = id
-- only the range depends on the predicate
- subst-Π2 : {Γ} (A : Set) (B : (γ : Γ) -> A -> Set)
+ transport-Π2 : {Γ} (A : Set) (B : (γ : Γ) -> A -> Set)
1 θ2 : Γ} (δ : θ1 ≃ θ2) (f : (x : A) -> B θ1 x)
- -> subst (\ γ -> (x : A) -> B γ x) δ f ≃
- (\ x -> subst (\ γ -> B γ x) δ (f x))
- subst2 _ _ Refl f = Refl
+ -> transport (\ γ -> (x : A) -> B γ x) δ f ≃
+ (\ x -> transport (\ γ -> B γ x) δ (f x))
+ transport2 _ _ id f = id
- subst-Π2i : {Γ} (A : Set) (B : (γ : Γ) -> A -> Set)
+ transport-Π2i : {Γ} (A : Set) (B : (γ : Γ) -> A -> Set)
1 θ2 : Γ} (δ : θ1 ≃ θ2) (f : {x : A} -> B θ1 x)
- -> Id{ {x : A} -> B θ2 x }
- (subst (\ γ -> {x : A} -> B γ x) δ f)
- (\ {x} -> subst (\ γ -> B γ x) δ (f {x}))
- subst-Π2i _ _ Refl f = Refl
+ -> Path{ {x : A} -> B θ2 x }
+ (transport (\ γ -> {x : A} -> B γ x) δ f)
+ (\ {x} -> transport (\ γ -> B γ x) δ (f {x}))
+ transport-Π2i _ _ id f = id
- resp : {Γ : Set} {θ1 θ2 : Γ} {δ : θ1 ≃ θ2}
+ ap : {Γ : Set} {θ1 θ2 : Γ} {δ : θ1 ≃ θ2}
{A : Γ -> Set} {B : (γ : Γ) -> A γ -> Set}
{M : (γ : Γ) -> (x : A γ) -> B γ x}
- -> (respd (\ γ -> (λ x -> M γ x)) δ)
- ≃ λ≃ (λ γ respd (λ (p : Σ (λ (γ' : Γ) A γ')) M (fst p) (snd p))
- (pair≃⁻ δ Refl))
- ∘ subst-Π A B δ (M θ1)
- resp-λ {δ = Refl} = Π≃η Refl
+ -> (apd (\ γ -> (λ x -> M γ x)) δ)
+ ≃ λ≃ (λ γ apd (λ (p : Σ (λ (γ' : Γ) A γ')) M (fst p) (snd p))
+ (pair≃⁻ δ id))
+ ∘ transport-Π A B δ (M θ1)
+ ap-λ {δ = id} = Π≃η id
- subst-com-for-resp-app :
+ transport-com-for-ap-app :
{Γ : Set} {θ1 θ2 : Γ} (δ : θ1 ≃ θ2)
(A : Γ -> Set) (B : (γ : Γ) -> A γ -> Set)
(F : (γ : Γ) -> (x : A γ) -> B γ x)
(M : (γ : Γ) -> A γ)
- -> Id (subst (λ z B z (M z)) δ (F θ1 (M θ1)))
- (subst (λ z B θ2 z) (respd M δ)
- (subst (λ z (x : A z) B z x) δ (F θ1)
- (subst (λ z A z) δ (M θ1))))
- subst-com-for-resp-app Refl _ _ _ _ = Refl
+ -> Path (transport (λ z B z (M z)) δ (F θ1 (M θ1)))
+ (transport (λ z B θ2 z) (apd M δ)
+ (transport (λ z (x : A z) B z x) δ (F θ1)
+ (transport (λ z A z) δ (M θ1))))
+ transport-com-for-ap-app id _ _ _ _ = id
- resp-app : {Γ : Set} {θ1 θ2 : Γ} {δ : θ1 ≃ θ2}
+ ap-app : {Γ : Set} {θ1 θ2 : Γ} {δ : θ1 ≃ θ2}
{A : Γ -> Set} {B : (γ : Γ) -> A γ -> Set}
{F : (γ : Γ) -> (x : A γ) -> B γ x}
{M : (γ : Γ) -> A γ}
- -> respd (\ γ -> (F γ) (M γ)) δ
- ≃ app≃2 (respd F δ) (respd M δ) ∘ subst-com-for-resp-app δ A B F M
- resp-app {δ = Refl} = Refl
+ -> apd (\ γ -> (F γ) (M γ)) δ
+ ≃ ap≃₁ (apd F δ) (apd M δ) ∘ transport-com-for-ap-app δ A B F M
+ ap-app {δ = id} = id
- resp-app-1-nd : {Γ A B : Set} {θ1 θ2 : Γ} {δ : θ1 ≃ θ2}
+ ap-app-1-nd : {Γ A B : Set} {θ1 θ2 : Γ} {δ : θ1 ≃ θ2}
{F : Γ -> A -> B}
{M : A}
- -> resp (\ x -> (F x) M) δ
- ≃ app≃ (resp F δ) {M}
- resp-app-1-nd {δ = Refl} = Refl
+ -> ap (\ x -> (F x) M) δ
+ ≃ ap≃ (ap F δ) {M}
+ ap-app-1-nd {δ = id} = id
naturality1 : {A B : Set} {F G : A -> B}
-> (β : G ≃ F)
-> {M N : A} (α : M ≃ N)
- -> resp G α ≃ ! (app≃ β {N}) ∘ resp F α ∘ app≃ β {M}
- naturality1 Refl Refl = Refl
+ -> ap G α ≃ ! (ap≃ β {N}) ∘ ap F α ∘ ap≃ β {M}
+ naturality1 id id = id
uncurry : {A B C : Set} -> (A -> B -> C) -> A × B -> C
uncurry f = \ x -> f (fst x) (snd x)
- resp-uncurry : {A B C : Set} (f : A -> B -> C) -> {M M' N N'} ->
+ ap-uncurry : {A B C : Set} (f : A -> B -> C) -> {M M' N N'} ->
(α : M ≃ M') (β : N ≃ N')
- -> resp (uncurry f) (NDPair.nondep-pair≃ α β)
- ≃ resp2 f α β
- resp-uncurry f Refl Refl = Refl
+ -> ap (uncurry f) (pair×≃ α β)
+ ≃ ap2 f α β
+ ap-uncurry f id id = id
{-
λ≃-refl : ∀ {A B} {f : A -> B} ->
- Id{Id {A -> B} f f}
- (λ≃ (\ x -> Refl{_}{f x}))
- (Refl{_}{f})
+ Path{Path {A -> B} f f}
+ (λ≃ (\ x -> id{_}{f x}))
+ (id{_}{f})
λ≃-refl = {!!}
-}
View
87 lib/Int.agda
@@ -1,49 +1,66 @@
{-# OPTIONS --type-in-type --without-K #-}
-open import lib.Nat public
+open import lib.First public
open import lib.Paths public
+open import lib.AdjointEquiv public
open Paths
module lib.Int where
- data Int : Set where
- Pos : Nat -> Int
+module Int where
+ data Positive : Type where
+ One : Positive
+ S : (n : Positive) Positive
+
+ data Int : Type where
+ Pos : (n : Positive) Int
Zero : Int
- Neg : Nat -> Int
-
- succ : Int -> Int
- succ Zero = Pos Z
+ Neg : (n : Positive) Int
+
+ succ : Int Int
+ succ Zero = Pos One
succ (Pos n) = Pos (S n)
- succ (Neg Z) = Zero
+ succ (Neg One) = Zero
succ (Neg (S n)) = Neg n
-
- pred : Int -> Int
- pred Zero = Neg Z
+
+ pred : Int Int
+ pred Zero = Neg One
pred (Pos (S n)) = Pos n
- pred (Pos Z) = Zero
+ pred (Pos One) = Zero
pred (Neg n) = Neg (S n)
+
+ _+_ : Int Int Int
+ Zero + m = m
+ (Pos One) + m = succ m
+ (Pos (S n)) + m = succ (Pos n + m)
+ (Neg One) + m = pred m
+ (Neg (S n)) + m = pred (Neg n + m)
+
+ succ-pred : (n : Int) Path (succ (pred n)) n
+ succ-pred (Pos One) = id
+ succ-pred (Pos (S y)) = id
+ succ-pred (Zero) = id
+ succ-pred (Neg y) = id
+
+ pred-succ : (n : Int) Path (pred (succ n)) n
+ pred-succ (Pos y) = id
+ pred-succ (Zero) = id
+ pred-succ (Neg One) = id
+ pred-succ (Neg (S y)) = id
+
+ succ-pred-triangle : (x : _) Id (succ-pred (succ x)) (ap succ (pred-succ x))
+ succ-pred-triangle (Pos y) = id
+ succ-pred-triangle Zero = id
+ succ-pred-triangle (Neg One) = id
+ succ-pred-triangle (Neg (S y)) = id
+
+ pred-succ-triangle : (x : _) Id (pred-succ (pred x)) (ap pred (succ-pred x))
+ pred-succ-triangle (Pos One) = id
+ pred-succ-triangle (Pos (S _)) = id
+ pred-succ-triangle Zero = id
+ pred-succ-triangle (Neg y) = id
+
+ succEquiv : Equiv Int Int
+ succEquiv = improve (hequiv succ pred pred-succ succ-pred)
- succ-pred : n -> succ (pred n) ≃ n
- succ-pred (Pos Z) = Refl
- succ-pred (Pos (S y)) = Refl
- succ-pred (Zero) = Refl
- succ-pred (Neg y) = Refl
-
- pred-succ : n -> pred (succ n) ≃ n
- pred-succ (Pos y) = Refl
- pred-succ (Zero) = Refl
- pred-succ (Neg Z) = Refl
- pred-succ (Neg (S y)) = Refl
-
- succ-pred-triangle : (x : _) Id (succ-pred (succ x)) (resp succ (pred-succ x))
- succ-pred-triangle (Pos y) = Refl
- succ-pred-triangle Zero = Refl
- succ-pred-triangle (Neg Z) = Refl
- succ-pred-triangle (Neg (S y)) = Refl
-
- pred-succ-triangle : (x : _) Id (pred-succ (pred x)) (resp pred (succ-pred x))
- pred-succ-triangle (Pos Z) = Refl
- pred-succ-triangle (Pos (S _)) = Refl
- pred-succ-triangle Zero = Refl
- pred-succ-triangle (Neg y) = Refl
View
32 lib/List.agda
@@ -1,12 +1,14 @@
{-# OPTIONS --type-in-type #-}
+open import lib.First
open import lib.Paths
+open Paths
open import lib.Nat
open import lib.Maybe
module lib.List where
- data List (a : Set) : Set where
+ data List (a : Type) : Type where
[] : List a
_::_ : a -> List a -> List a
@@ -20,54 +22,54 @@ module lib.List where
module ListM where
-- we expand this out, rather than using (Somewhere (\x -> Id x a) l)
-- so that we don't have to write the silly identity proof in the deBruijn index
- data _∈_ {A : Set} : A -> List A -> Set where
+ data _∈_ {A : Type} : A -> List A -> Type where
i0 : {x : A} {xs : List A} -> x ∈ (x :: xs )
iS : {x y : A} {xs : List A} -> y ∈ xs -> y ∈ (x :: xs)
infix 10 _∈_
- data Everywhere {A : Set} (P : A -> Set) : List A -> Set where
+ data Everywhere {A : Type} (P : A -> Type) : List A -> Type where
E[] : Everywhere P []
_E::_ : forall {x xs} -> P x -> Everywhere P xs -> Everywhere P (x :: xs)
infixr 98 _E::_
- [_] : {A : Set} -> A -> List A
+ [_] : {A : Type} -> A -> List A
[_] x = x :: []
- append : {A : Set} -> List A -> List A -> List A
+ append : {A : Type} -> List A -> List A -> List A
append [] l2 = l2
append (x :: xs) l2 = x :: (append xs l2)
- _++_ : {A : Set} -> List A -> List A -> List A
+ _++_ : {A : Type} -> List A -> List A -> List A
_++_ = append
infixr 20 _++_
- length : {a : Set} -> List a -> Nat
+ length : {a : Type} -> List a -> Nat
length [] = 0
length (x :: xs) = S (length xs)
- fold : {a b : Set} -> b -> (a -> b -> b) -> List a -> b
+ fold : {a b : Type} -> b -> (a -> b -> b) -> List a -> b
fold n c [] = n
fold n c (x :: xs) = c x (fold n c xs)
- map : {a b : Set} -> (a -> b) -> List a -> List b
+ map : {a b : Type} -> (a -> b) -> List a -> List b
map f [] = []
map f (x :: xs) = f x :: (map f xs)
- nth : {A : Set} -> List A -> Nat -> Maybe A
+ nth : {A : Type} -> List A -> Nat -> Maybe A
nth [] _ = None
nth (x :: xs) 0 = Some x
nth (x :: xs) (S n) = nth xs n
- tabulate' : {A : Set} -> (Nat -> A) -> Nat -> Nat -> List A
+ tabulate' : {A : Type} -> (Nat -> A) -> Nat -> Nat -> List A
tabulate' f 0 cur = []
tabulate' f (S n) cur = f cur :: tabulate' f n (S cur)
- tabulate : {A : Set} -> (Nat -> A) -> Nat -> List A
+ tabulate : {A : Type} -> (Nat -> A) -> Nat -> List A
tabulate f n = tabulate' f n 0
- fuse-map : {A B C : Set} {f : A -> B} {g : B -> C} (l : List A) ->
+ fuse-map : {A B C : Type} {f : A -> B} {g : B -> C} (l : List A) ->
map g (map f l)
≃ map (\ x -> g (f x)) l
- fuse-map [] = Refl
- fuse-map {f = f} {g = g} (x :: xs) = Paths.resp (\ xs -> (g (f x)) :: xs) (fuse-map xs)
+ fuse-map [] = id
+ fuse-map {f = f} {g = g} (x :: xs) = ap (\ xs -> (g (f x)) :: xs) (fuse-map xs)
View
70 lib/Monoid.agda
@@ -17,9 +17,9 @@ module lib.Monoid where
MonoidB : {A B} -> (α : Id A B) -> (M : Monoid A) -> Monoid B
MonoidB {A}{B} α M =
- record { _⊙_ = subst (λ A' A' A' A') α (Monoid._⊙_ M);
- `1 = subst (λ A' A') α (Monoid.`1 M);
- assoc = subst{Σ (λ (A' : Set) (A' A' A') × A')}
+ record { _⊙_ = transport (λ A' A' A' A') α (Monoid._⊙_ M);
+ `1 = transport (λ A' A') α (Monoid.`1 M);
+ assoc = transport{Σ (λ (A' : Set) (A' A' A') × A')}
(λ (p : Σ (λ (A' : Set) (A' A' A') × A'))
let A' : Set
A' = fst p
@@ -29,10 +29,10 @@ module lib.Monoid where
`1 = snd (snd p)
in {x y z : A'} (x ⊙ y) ⊙ z ≃ x ⊙ (y ⊙ z))
{(A , Monoid._⊙_ M , Monoid.`1 M)}
- {(B , subst (λ A' A' A' A') α (Monoid._⊙_ M) , subst (λ A' A') α (Monoid.`1 M))}
- (pair≃ α (app≃ (NDPair.subst-× α (λ A' A' A' A') (λ A' A'))))
+ {(B , transport (λ A' A' A' A') α (Monoid._⊙_ M) , transport (λ A' A') α (Monoid.`1 M))}
+ (pair≃ α (ap≃ (transport-× α (λ A' A' A' A') (λ A' A'))))
(Monoid.assoc M);
- unitl = subst {Σ (λ (A' : Set) (A' A' A') × A')}
+ unitl = transport {Σ (λ (A' : Set) (A' A' A') × A')}
(λ (p : Σ (λ (A' : Set) (A' A' A') × A'))
let A' : Set
A' = fst p
@@ -43,12 +43,12 @@ module lib.Monoid where
in {x : A'} `1 ⊙ x ≃ x)
{A , Monoid._⊙_ M , Monoid.`1 M}
{B ,
- subst (λ A' A' A' A') α (Monoid._⊙_ M) ,
- subst (λ A' A') α (Monoid.`1 M)}
+ transport (λ A' A' A' A') α (Monoid._⊙_ M) ,
+ transport (λ A' A') α (Monoid.`1 M)}
(pair≃ α
- (app≃ (NDPair.subst-× α (λ A' A' A' A') (λ A' A'))))
+ (ap≃ (transport-× α (λ A' A' A' A') (λ A' A'))))
(Monoid.unitl M);
- unitr = subst {Σ (λ (A' : Set) (A' A' A') × A')}
+ unitr = transport {Σ (λ (A' : Set) (A' A' A') × A')}
(λ (p : Σ (λ (A' : Set) (A' A' A') × A'))
let A' : Set
A' = fst p
@@ -59,41 +59,41 @@ module lib.Monoid where
in {x : A'} x ⊙ `1 ≃ x)
{A , Monoid._⊙_ M , Monoid.`1 M}
{B ,
- subst (λ A' A' A' A') α (Monoid._⊙_ M) ,
- subst (λ A' A') α (Monoid.`1 M)}
+ transport (λ A' A' A' A') α (Monoid._⊙_ M) ,
+ transport (λ A' A') α (Monoid.`1 M)}
(pair≃ α
- (app≃ (NDPair.subst-× α (λ A' A' A' A') (λ A' A'))))
+ (ap≃ (transport-× α (λ A' A' A' A') (λ A' A'))))
(Monoid.unitr M) }
- subst-Monoid : {A B} -> (α : Id A B) ->
- subst Monoid α
+ transport-Monoid : {A B} -> (α : Id A B) ->
+ transport Monoid α
≃ MonoidB α
- subst-Monoid Refl = Refl
+ transport-Monoid id = id
- -- snd-pair≃⁻-Refl : {A : Set} {B : A -> Set} {x q : Σ B}
+ -- snd-pair≃⁻-id : {A : Set} {B : A -> Set} {x q : Σ B}
-- -> (α : x ≃ (fst q))
-- -> respd (snd{A}{B}) (pair≃⁻ α () ≃ {!β!}
- -- snd-pair≃⁻-Refl = {!!}
+ -- snd-pair≃⁻-id = {!!}
{-
roughly (modulo adjustments)
- Refl at backmap
+ id at backmap
∘ resp blah (Monoid.unitl M)
respd snd
(pair≃⁻
(pair≃ α
(resp (λ f → f ((λ v v' → Monoid._⊙_ M v v') , Monoid.`1 M))
- (NDPair.subst-× α (λ A' → A' → A' → A') (λ A' → A'))))
- Refl)
+ (NDPair.transport-× α (λ A' → A' → A' → A') (λ A' → A'))))
+ id)
resp
- (subst (λ z → fst (fst z))
+ (transport (λ z → fst (fst z))
(pair≃⁻
(pair≃ α
(resp (λ f → f ((λ v v' → Monoid._⊙_ M v v') , Monoid.`1 M))
- (NDPair.subst-× α (λ A' → A' → A' → A') (λ A' → A'))))
- Refl))
+ (NDPair.transport-× α (λ A' → A' → A' → A') (λ A' → A'))))
+ id))
(Monoid.unitl M)
!
@@ -101,31 +101,31 @@ respd snd
(pair≃⁻
(pair≃ α
(resp (λ f → f ((λ v v' → Monoid._⊙_ M v v') , Monoid.`1 M))
- (NDPair.subst-× α (λ A' → A' → A' → A') (λ A' → A'))))
- Refl))
+ (NDPair.transport-× α (λ A' → A' → A' → A') (λ A' → A'))))
+ id))
-}
{-
- subst-unitl : ∀ {A B} (α : A ≃ B) (M : Monoid A) ->
+ transport-unitl : ∀ {A B} (α : A ≃ B) (M : Monoid A) ->
Id{ {x : B} -> (Monoid._⊙_ (MonoidB α M) (Monoid.`1 (MonoidB α M)) x) ≃ x }
(Monoid.unitl (MonoidB α M))
(Monoid.unitl (MonoidB α M))
- subst-unitl {A}{B} α M = {!!} ∘
- λ≃i (λ x → subst-Id-d{Σ \ (p : Σ \ (A : Set) -> (A -> A -> A) × A) -> fst p}
+ transport-unitl {A}{B} α M = {!!} ∘
+ λ≃i (λ x → transport-Id-d{Σ \ (p : Σ \ (A : Set) -> (A -> A -> A) × A) -> fst p}
(λ p → fst (snd (fst p)) (snd (snd (fst p))) (snd p))
snd (pair≃⁻
(pair≃ α
- (app≃ (NDPair.subst-× α (λ A' → A' → A' → A') (λ A' → A'))))
- (Refl {_})) (Monoid.unitl M))
- -- (λ≃i (λ x → subst-Id (λ p → fst (snd (fst p)) (snd (snd (fst p))) (snd p))
+ (ap≃ (NDPair.transport-× α (λ A' → A' → A' → A') (λ A' → A'))))
+ (id {_})) (Monoid.unitl M))
+ -- (λ≃i (λ x → transport-Id (λ p → fst (snd (fst p)) (snd (snd (fst p))) (snd p))
-- snd
- -- (pair≃⁻ (pair≃ α (app≃ (NDPair.subst-× α (λ A' → A' → A' → A') (λ A' → A')))) (Refl {_}))
+ -- (pair≃⁻ (pair≃ α (ap≃ (NDPair.transport-× α (λ A' → A' → A' → A') (λ A' → A')))) (id {_}))
-- (Monoid.unitl M {x})))
-subst-Πi{Σ \ (A : Set) -> (A -> A -> A) × A}
+transport-Πi{Σ \ (A : Set) -> (A -> A -> A) × A}
fst
(λ p x → fst (snd p) (snd (snd p)) x ≃ x)
(pair≃ α
- (app≃ (NDPair.subst-× α (λ A' → A' → A' → A') (λ A' → A')))) (Monoid.unitl M)
+ (ap≃ (NDPair.transport-× α (λ A' → A' → A' → A') (λ A' → A')))) (Monoid.unitl M)
-}
View
6 lib/Nat.agda
@@ -1,9 +1,11 @@
{-# OPTIONS --type-in-type --without-K #-}
+open import lib.First
+
module lib.Nat where
- data Nat : Set where
+ data Nat : Type where
Z : Nat
S : Nat -> Nat
@@ -13,7 +15,7 @@ module lib.Nat where
module NatM where
- natrec : {p : Nat -> Set} ->
+ natrec : {p : Nat -> Type} ->
p Z ->
((n : Nat) -> p n -> p (S n)) ->
(n : Nat) -> p n
View
632 lib/Paths.agda
@@ -3,457 +3,329 @@
-- identity types that never use K
-- homotopically, Id M N is thought of as a path from M to N
--- we also use M ≃ N and Paths M N as notation for Id M N
+-- we also use M ≃ N and Path M N as notation for Id M N
+
+open import lib.First
module lib.Paths where
- data Id {A : Set} : A -> A -> Set where
- Refl : {a : A} -> Id a a
- _≃_ : {A : Set} -> A -> A -> Set
- _≃_ = Id
+ data Id {A : Type} : A A → Type where
+ id : {M : A} Id M M
- infix 9 _≃_
+ Path : {A : Type} A A Type
+ Path = Id
- Paths : {A : Set} -> A -> A -> Set
- Paths = Id
+ _≃_ : {A : Type} A A Type
+ _≃_ = Path
+
+ infix 9 _≃_
-- type-indepdendent operations on paths
module Paths where
- -- define the operations using pattern-matching
- -- this version makes it much easier to read normalized goals
+ -- induction
- jay : {A : Set} (C : (x y : A) -> Id x y -> Set)
- -> {M N : A} -> (P : Id M N)
- -> ((x : A) -> C x x Refl)
+ jay : {A : Type} (C : (x y : A) -> Path x y -> Type)
+ -> {M N : A} -> (P : Path M N)
+ -> ((x : A) -> C x x id)
-> C M N P
- jay _ Refl b = b _
-
- jay1 : {A : Set} {M : A} (C : (x : A) -> Id M x -> Set)
- -> {N : A} -> (P : Id M N)
- -> (C M Refl)
- -> C N P
- jay1 _ Refl b = b
-
- subst : {A : Set} (p : A -> Set) {x y : A} -> Id x y -> p x -> p y
- subst C Refl = λ x' x'
+ jay _ id b = b _
- resp : {A C : Set} {M N : A} (f : A -> C) -> Id M N -> Id (f M) (f N)
- resp f Refl = Refl
+ path-induction : {A : Type} {M : A}
+ (C : (x : A) Path M x Type)
+ (C M id)
+ {N : A} (P : Path M N)
+ C N P
+ path-induction _ b id = b
- respd : {A : Set} {C : A -> Set} {M N : A} (f : (x : A) -> C x) -> (p : Id M N) -> Id (subst C p (f M)) (f N)
- respd f Refl = Refl
-
- trans : {A : Set} {M N P : A} -> Id M N -> Id N P -> Id M P
- trans Refl p = p
-
- _∘_ : {A : Set} {M N P : A} -> Id N P -> Id M N -> Id M P
- β ∘ Refl = β
+ -- groupoid
+ ! : {A : Type} {M N : A} Path M N Path N M
+ ! id = id
+
+ _∘_ : {A : Type} {M N P : A} Path N P Path M N Path M P
+ β ∘ id = β
+
infixr 10 _∘_
-
+
infix 2 _∎
infixr 2 _≃〈_〉_
- _≃〈_〉_ : {A : Set} (x : A) {y z : A} Id x y Id y z Id x z
+ _≃〈_〉_ : {A : Type} (x : A) {y z : A} Path x y Path y z Path x z
_ ≃〈 p1 〉 p2 = (p2 ∘ p1)
-
- _∎ : {A : Set} (x : A) Id x x
- _∎ _ = Refl
-
- sym : {a : Set} {x y : a} -> Id x y -> Id y x
- sym Refl = Refl
-
- ! : {a : Set} {x y : a} -> Id x y -> Id y x
- ! Refl = Refl
-
- trans-unit-l : {A : Set} {M N : A} -> (p : Id M N) -> Id (trans Refl p) p
- trans-unit-l Refl = Refl
-
- trans-unit-r : {A : Set} {M N : A} -> (p : Id M N) -> Id (trans p Refl) p
- trans-unit-r Refl = Refl
-
- ∘-unit-l : {A : Set} {M N : A} -> (p : Id M N) -> Id (Refl ∘ p) p
- ∘-unit-l Refl = Refl
-
- ∘-unit-r : {A : Set} {M N : A} -> (p : Id M N) -> Id (p ∘ Refl) p
- ∘-unit-r Refl = Refl
-
- trans-assoc : {A : Set} {M N P Q : A} -> (p : Id M N) (q : Id N P) (r : Id P Q) -> Id (trans (trans p q) r) (trans p (trans q r))
- trans-assoc Refl Refl Refl = Refl
-
- ∘-assoc : {A : Set} {M N P Q : A} -> (r : Id P Q) (q : Id N P) (p : Id M N) -> Id (r ∘ (q ∘ p)) ((r ∘ q) ∘ p)
- ∘-assoc Refl Refl Refl = Refl
-
- sym-inv : {A : Set} {M N : A} (p : Id M N) -> Id (trans p (sym p)) Refl
- sym-inv Refl = Refl
-
- sym-inv2 : {A : Set} {M N : A} (p : Id M N) -> Id (trans (sym p) p) Refl
- sym-inv2 Refl = Refl
-
- !-inv-l : {A : Set} {M N : A} (p : Id M N) -> Id ((! p) ∘ p) Refl
- !-inv-l Refl = Refl
-
- !-inv-r : {A : Set} {M N : A} (p : Id M N) -> Id (p ∘ (! p)) Refl
- !-inv-r Refl = Refl
-
- sym-invol : {A : Set} {M N : A} (p : Id M N) -> Id (sym (sym p)) p
- sym-invol Refl = Refl
-
- !-invol : {A : Set} {M N : A} (p : Id M N) -> Id (! (! p)) p
- !-invol Refl = Refl
-
- !-∘ : {A : Set} {M N P : A} -> (q : Id N P) -> (p : Id M N)
- -> (! (q ∘ p)) ≃ ! p ∘ ! q
- !-∘ Refl Refl = Refl
-
- -- Moving ! between sides of an Id
- !-left : {X : Set} {M N : X} -> (p : Id M N) -> (q : Id M M) -> (r : Id N N)
- -> Id (p ∘ q ∘ ! p) r ≃ Id (p ∘ q) (r ∘ p)
- !-left Refl q r = Refl
-
- move-right : {X : Set} {M N P : X} -> (q : Id N P) (p : Id M N) -> (r : Id M P)
- -> Id (q ∘ p) r ≃ Id q (r ∘ ! p)
- move-right q Refl r = Refl
-
- move-left : {X : Set} {M N P : X} -> (q : Id N P) (p : Id M N) -> (r : Id M P)
- -> Id r (q ∘ p) ≃ Id (r ∘ ! p) q
- move-left q Refl r = Refl
- subst-Id : {Γ A : Set} (f g : Γ -> A) {M N : Γ} (p : Id M N)
- -> (p' : _) -> Id (subst (\ x -> Id (f x) (g x)) p p') ((resp g p) ∘ p' ∘ (! (resp f p)))
- subst-Id _ _ Refl p' = ! (∘-unit-l p')
+ _∎ : {A : Type} (x : A) Path x x
+ _∎ _ = id
+
+ ∘-unit-l : {A : Type} {M N : A} (α : Path M N)
+ Path (id ∘ α) α
+ ∘-unit-l id = id
+
+ ∘-assoc : {A : Type} {M N P Q : A}
+ (γ : Path P Q) (β : Path N P) (α : Path M N)
+ Path (γ ∘ (β ∘ α)) ((γ ∘ β) ∘ α)
+ ∘-assoc id id id = id
+
+ !-inv-l : {A : Type} {M N : A} (α : Path M N)
+ Path (! α ∘ α) id
+ !-inv-l id = id
+
+ ∘-unit-r : {A : Type} {M N : A} (α : Path M N)
+ Path (α ∘ id) α
+ ∘-unit-r id = id
+
+ !-inv-r : {A : Type} {M N : A} (α : Path M N) Path (α ∘ (! α)) id
+ !-inv-r id = id
+
+ !-inv-r-front : {A : Type} {M N P : A} (p : Path P N) (q : Path M N) Path (p ∘ (! p) ∘ q) q
+ !-inv-r-front id id = id
+
+ !-inv-r-back : {A : Type} {M N P : A} (q : Path N M) (p : Path P N) Path (q ∘ (p ∘ ! p)) q
+ !-inv-r-back id id = id
+
+ !-invol : {A : Type} {M N : A} (p : Path M N) Path (! (! p)) p
+ !-invol id = id
+
+ !-∘ : {A : Type} {M N P : A} (q : Path N P) (p : Path M N)
+ (! (q ∘ p)) ≃ ! p ∘ ! q
+ !-∘ id id = id
+
+ move-right : {A : Type} {M N P : A}
+ (β : Path N P) (α : Path M N) (γ : Path M P)
+ Path (β ∘ α) γ
+ Path α (! β ∘ γ)
+ move-right id id γ x = ! (∘-unit-l γ) ∘ x
+
+ move-left-! : {A : Type} {M N P : A}
+ (α : Path M N) (β : Path N P) (γ : Path M P)
+ Path α (! β ∘ γ)
+ Path (β ∘ α) γ
+ move-left-! id id γ x = ∘-unit-l γ ∘ x
+
+ move-right-! : {A : Type} {M N P : A}
+ (β : Path P N) (α : Path M N) (γ : Path M P)
+ Path (! β ∘ α) γ
+ Path α (β ∘ γ)
+ move-right-! id id γ x = ! (∘-unit-l γ) ∘ x
+
+ move-right-right-! : {A : Type} {M N P : A}
+ (β : Path N P) (α : Path N M) (γ : Path M P)
+ Path (β ∘ ! α) γ
+ Path β (γ ∘ α)
+ move-right-right-! id id γ x = x
+
+ rassoc-1-3-1 : {A} {M1 M2 M3 M4 M5 M6 : A}
+ (a56 : Path M5 M6) (a45 : Path M4 M5) (a34 : Path M3 M4) (a23 : Path M2 M3) (a12 : Path M1 M2)
+ Path (a56 ∘ (a45 ∘ a34 ∘ a23) ∘ a12) (a56 ∘ a45 ∘ a34 ∘ a23 ∘ a12)
+ rassoc-1-3-1 id id id id id = id
- subst-Id-post : {A : Set} {M N P : A} (p' : Id N P) (p : Id M N)
- -> Id (subst (\ x -> Id M x) p' p) (p' ∘ p)
- subst-Id-post Refl Refl = Refl -- FIXME J
- subst-Id-pre : {A : Set} {M N P : A} (p' : Id N M) (p : Id N P)
- -> Id (subst (\ x -> Id x P) p' p) (p ∘ ! p')
- subst-Id-pre Refl Refl = Refl -- FIXME J
+ -- transport and ap
+
+ transport : {B : Type} (E : B Type)
+ {b1 b2 : B} Path b1 b2 (E b1 E b2)
+ transport C id = λ x x
+
+ transport-Path-right : {A : Type} {M N P : A}
+ (α' : Path N P) (α : Path M N)
+ Path (transport (\ x Path M x) α' α) (α' ∘ α)
+ transport-Path-right id id = id
+
+ ap : {A B : Type} {M N : A}
+ (f : A B) Path{A} M N Path{B} (f M) (f N)
+ ap f id = id
+
+ apd : {B : Type} {E : B Type} {b₁ b₂ : B}
+ (f : (x : B) E x) (β : Path b₁ b₂)
+ Path (transport E β (f b₁)) (f b₂)
+ apd f id = id
+
+ transport-∘ : {A : Type} (C : A Type) {M N P : A} (β : Path N P) (α : Path M N)
+ Path (transport C (β ∘ α)) (\ x transport C β (transport C α x))
+ transport-∘ _ id id = id
+
+ transport-ap-assoc : {A : Type} (C : A Type) {M N : A} (α : Path M N) Path (transport C α) (transport (\ x x) (ap C α))
+ transport-ap-assoc C id = id
+
+ transport-ap-assoc' : {A B : Type} (C : B Type) (f : A B) {M N : A} (α : Path M N)
+ Path (transport (\ x -> C (f x)) α) (transport C (ap f α))
+ transport-ap-assoc' C f id = id
- subst-resp : {A : Set} (C : A -> Set) {M N : A} (α : Id M N) -> Id (subst C α) (subst (\ x -> x) (resp C α))
- subst-resp C Refl = Refl
+ coe : {A B : Type} -> Path A B -> A -> B
+ coe = transport (\ x -> x)
- subst-resp' : {A A' : Set} (C : A' -> Set) (f : A -> A')
- {M N : A} (α : Id M N) -> Id (subst C (resp f α)) (subst (\ x -> C (f x)) α)
- subst-resp' C f Refl = Refl
+ coe-inv-2 : {A B : Type} -> (α : Path A B) -> {M : _} -> coe α (coe (! α) M) ≃ M
+ coe-inv-2 id = id
- subst-∘ : {A : Set} (C : A -> Set) {M N P : A} (β : Id N P) (α : Id M N)
- -> Id (subst C (β ∘ α)) (\ x -> subst C β (subst C α x))
- subst-∘ _ Refl Refl = Refl
+ coe-inv-1 : {A B : Type} -> (α : Path A B) -> {M : _} -> coe (! α) (coe α M) ≃ M
+ coe-inv-1 id = id
- subst-o : {A B : Set} (C : B -> Set) (f : A -> B)
- {M N : A} (α : M ≃ N)
- -> subst (\ x -> C (f x)) α ≃ subst C (resp f α)
- subst-o _ f Refl = Refl
+ transport-inv-1 : {A : Type} (B : A -> Type) {M N : A} (α : M ≃ N) -> (\y -> transport B (! α) (transport B α y)) ≃ (\ x -> x)
+ transport-inv-1 _ id = id
- -- fire-subst-d : {Γ : Set} {A : Γ -> Set} (f g : (x : Γ) -> A x) {M N : Γ} {p : Id M N}
- -- -> {p' : Id (f M) (g M)} -> Id (subst (\ x -> Id (f x) (g x)) p p') (trans (sym (respd f p)) (trans (resp (subst A p) p') (respd g p)))
- -- fire-subst-d _ _ {p = Refl} {p'} = {!!}
+ transport-inv-2 : {A : Type} (B : A -> Type) {M N : A} (α : M ≃ N) -> (\y -> transport B α (transport B (! α) y)) ≃ (\ x -> x)
+ transport-inv-2 _ id = id
- swap-left : {A : Set} {M N P : A} {p1 : Id M N} {p2 : Id M P} {p3 : Id N P}
- -> Id p3 ((trans (sym p1)) p2)
- -> Id (trans p1 p3) p2
- swap-left {p1 = Refl} p = trans (trans-unit-l _) (trans p (trans-unit-l _))
+ ap-o : {A B C : Type} (g : B C) (f : A B)
+ {M N : A} (α : Path M N)
+ ap (\ x g (f x)) α ≃ ap g (ap f α)
+ ap-o g f id = id
+
+ ap-id : {A : Type} {M N : A} (α : Path M N)
+ Path (ap (\ x x) α) α
+ ap-id id = id
+
+ ap-! : {A B : Type} (F : A B) {M N : A} (α : Path M N)
+ Path (ap F (! α)) (! (ap F α))
+ ap-! _ id = id
+
+ ap-∘ : {A B : Type} (F : A B) {M N P : A} (β : Path N P) (α : Path M N)
+ Path (ap F (β ∘ α)) (ap F β ∘ ap F α)
+ ap-∘ _ _ id = id
+
+ apd-∘ : {A : Type} {B : A -> Type} (F : (x : A) -> B x) {M N P : A} (β : Path N P) (α : Path M N)
+ -> Path (apd F (β ∘ α)) (apd F β ∘ ap (λ x transport B β x) (apd F α) ∘ ap (λ f f (F M)) (transport-∘ B β α))
+ apd-∘ _ id id = id
- resp-constant : {A C : Set} {M N : A} (v : C) -> (p : Id M N) -> Id (resp (\ _ -> v) p) Refl
- resp-constant v Refl = Refl
+ ap-by-id : {A : Type} {f : A A}
+ (αf : (x : _) x ≃ f x)
+ {M N : A} (α : M ≃ N)
+ (ap f α ≃ αf N ∘ α ∘ ! (αf M))
+ ap-by-id αf id = ap (λ x αf _ ∘ x) (! (∘-unit-l (! (αf _)))) ∘ ! (!-inv-r (αf _))
- subst-constant : {A C : Set} {M N : A} -> (p : Id M N) -> Id (subst (\ _ -> C) p) (\ x -> x)
- subst-constant Refl = Refl
+ ap-constant : {A C : Type} {M N : A} (v : C) -> (p : Path M N) -> Path (ap (\ _ -> v) p) id
+ ap-constant v id = id
- resp-! : {A B : Set} (F : A -> B) {M N : A} (α : Id M N)
- -> Id (resp F (! α)) (! (resp F α))
- resp-! _ Refl = Refl
+ transport-constant : {A C : Type} {M N : A} -> (p : Path M N) -> Path (transport (\ _ -> C) p) (\ x -> x)
+ transport-constant id = id
- resp-∘ : {A B : Set} (F : A -> B) {M N P : A} (β : Id N P) (α : Id M N)
- -> Id (resp F (β ∘ α)) (resp F β ∘ resp F α)
- resp-∘ _ _ Refl = Refl
+ transport-Path : {Γ A : Type} (f g : Γ A) {M N : Γ} (p : Path M N)
+ (p' : _) Path (transport (\ x Path (f x) (g x)) p p')
+ ((ap g p) ∘ p' ∘ (! (ap f p)))
+ transport-Path _ _ id p' = ! (∘-unit-l p')
- respd-∘ : {A : Set} {B : A -> Set} (F : (x : A) -> B x) {M N P : A} (β : Id N P) (α : Id M N)
- -> Id (respd F (β ∘ α)) (respd F β ∘ resp (λ x subst B β x) (respd F α) ∘ resp (λ f f (F M)) (subst-∘ B β α))
- respd-∘ _ Refl Refl = Refl
+ transport-Path-d : {Γ : Type} {A : Γ -> Type} (f g : (x : Γ) -> A x) {M N : Γ} (p : Path M N)
+ -> (p' : f M ≃ g M)
+ -> Path (transport (\ x -> Path (f x) (g x)) p p')
+ (apd g p ∘ ap (transport A p) p' ∘ ! (apd f p))
+ transport-Path-d _ _ id p' = ! (∘-unit-l p' ∘ ap (λ x id ∘ x) (ap-id p'))
- resp-id : {A : Set} {M N : A} (α : Id M N)
- -> Id (resp (\ x -> x) α) α
- resp-id Refl = Refl
+ transport-Path-pre : {A : Type} {M N P : A} (p' : Path N M) (p : Path N P)
+ -> Path (transport (\ x -> Path x P) p' p) (p ∘ ! p')
+ transport-Path-pre id id = id -- FIXME J
- resp-o : {A B C : Set} (g : B -> C) (f : A -> B)
- {M N : A} (α : M ≃ N)
- -> resp (\ x -> g (f x)) α ≃ resp g (resp f α)
- resp-o g f Refl = Refl
+ transport-com-for-ap-of-transport :
+ {Γ : Type} {θ1 θ2 : Γ} (δ : θ1 ≃ θ2)
+ (A : Γ -> Type) (C : (γ : Γ) -> A γ -> Type)
+ (M1 M2 : (γ : Γ) -> A γ)
+ (α : (γ : Γ) -> M1 γ ≃ M2 γ)
+ (M : (γ : Γ) -> C γ (M1 γ))
+ -> Path (transport (λ z C z (M2 z)) δ (transport (C θ1) (α θ1) (M θ1)))
+ (transport (λ _ C θ2 (M2 θ2)) (apd M δ)
+ (transport (C θ2) (α θ2) (transport (λ z C z (M1 z)) δ (M θ1))))
+ transport-com-for-ap-of-transport id A C M1 M2 α M = id
- resp-by-id : {A : Set} {f : A -> A}
- (αf : (x : _) -> x ≃ f x)
- -> {M N : A} (α : M ≃ N)
- -> (resp f α ≃ αf N ∘ α ∘ ! (αf M))
- resp-by-id αf Refl = resp (λ x αf _ ∘ x) (! (∘-unit-l (! (αf _)))) ∘ ! (!-inv-r (αf _))
+ ap-of-transport : {Γ : Type} {θ1 θ2 : Γ} {δ : θ1 ≃ θ2}
+ {A : Γ -> Type} {C : (γ : Γ) -> A γ -> Type}
+ {M1 M2 : (γ : Γ) -> A γ}
+ {α : (γ : Γ) -> M1 γ ≃ M2 γ}
+ {M : (γ : Γ) -> C γ (M1 γ)}
+ -> apd (\ γ -> transport (C γ) (α γ) (M γ)) δ
+ ≃ apd (λ x transport (C θ2) (α θ2) x) (apd M δ)
+ ∘ transport-com-for-ap-of-transport δ A C M1 M2 α M
+ ap-of-transport {δ = id} = id
- resp2 : {A B C} {M N : A} {M' N' : B} (f : A -> B -> C) -> Id M N -> Id M' N' -> Id (f M M') (f N N')
- resp2 f Refl Refl = Refl
+ ap2 : {A B C} {M N : A} {M' N' : B} (f : A -> B -> C) -> Path M N -> Path M' N' -> Path (f M M') (f N N')
+ ap2 f id id = id
- resp2-resps-1 : {A B C} {M N : A} {M' N' : B} (f : A -> B -> C) -> (α : Id M N) (β : Id M' N')
- -> Id (resp2 f α β) (resp (λ x f x N') α ∘ resp (λ y f M y) β)
- resp2-resps-1 f Refl Refl = Refl
+ ap2-aps-1 : {A B C} {M N : A} {M' N' : B} (f : A -> B -> C) -> (α : Path M N) (β : Path M' N')
+ -> Path (ap2 f α β) (ap (λ x f x N') α ∘ ap (λ y f M y) β)
+ ap2-aps-1 f id id = id
- resp2-resps-2 : {A B C} {M N : A} {M' N' : B} (f : A -> B -> C) -> (α : Id M N) (β : Id M' N')
- -> Id (resp2 f α β) (resp (λ y f N y) β ∘ resp (λ x f x M') α)
- resp2-resps-2 f Refl Refl = Refl
+ ap2-aps-2 : {A B C} {M N : A} {M' N' : B} (f : A -> B -> C) -> (α : Path M N) (β : Path M' N')
+ -> Path (ap2 f α β) (ap (λ y f N y) β ∘ ap (λ x f x M') α)
+ ap2-aps-2 f id id = id
- resp2-β1 : {A B} {M N : A} {M' N' : B} -> (α : Id M N) -> (β : Id M' N')
- -> Id (resp2 (\ x y -> x) α β) α
- resp21 Refl Refl = Refl
+ ap2-β1 : {A B} {M N : A} {M' N' : B} -> (α : Path M N) -> (β : Path M' N')
+ -> Path (ap2 (\ x y -> x) α β) α
+ ap21 id id = id
- resp : {A : Set} {x y z : A} {p q : Id x y} {p' q' : Id y z}
- -> Id p' q' -> Id p q -> Id (p' ∘ p) (q' ∘ q)
- resp∘ a b = resp2 _∘_ a b
+ ap : {A : Type} {x y z : A} {p q : Path x y} {p' q' : Path y z}
+ -> Path p' q' -> Path p q -> Path (p' ∘ p) (q' ∘ q)
+ ap∘ a b = ap2 _∘_ a b
- resp-resp : {A B : Set} {f g : A -> B}
+ ap-ap : {A B : Type} {f g : A -> B}
(α : f ≃ g)
-> {M N : A} (β : M ≃ N)
- -> (resp f β ≃ ! (resp (\ f -> f N) α) ∘ resp g β ∘ resp (\ f -> f M) α)
- resp-resp Refl Refl = Refl
+ -> (ap f β ≃ ! (ap (\ f -> f N) α) ∘ ap g β ∘ ap (\ f -> f M) α)
+ ap-ap id id = id
- resp2-resp : {A B C : Set} {f g : A -> B -> C}
+ ap2-ap : {A B C : Type} {f g : A -> B -> C}
(α : f ≃ g)
-> {M N : A} (β : M ≃ N)
-> {M' N' : B} (β' : M' ≃ N')
- -> (resp2 f β β' ≃ ! (resp (\ f -> f N N') α) ∘ resp2 g β β' ∘ resp (\ f -> f M M') α)
- resp2-resp Refl Refl Refl = Refl
+ -> (ap2 f β β' ≃ ! (ap (\ f -> f N N') α) ∘ ap2 g β β' ∘ ap (\ f -> f M M') α)
+ ap2-ap id id id = id
- resp∘-unit-r : {A : Set} {x y : A} {p q : Id x y}
- -> (a : Id p q) -> Id (resp∘ a (Refl{_}{Refl})) a -- definitional equalities work out such that this works unadjusted
- resp∘-unit-r a = jay (λ _ _ p Id (resp∘ p (Refl {_} {Refl})) p) a (λ _ Refl)
+ ap∘-unit-r : {A : Type} {x y : A} {p q : Path x y}
+ -> (a : Path p q) -> Path (ap∘ a (id{_}{id})) a -- definitional equalities work out such that this works unadjusted
+ ap∘-unit-r a = jay (λ _ _ p Path (ap∘ p (id {_} {id})) p) a (λ _ id)
- resp∘-unit-l : {A : Set} {x y : A} {p q : Id x y}
- -> (a : Id p q) -> Id (resp∘ (Refl{_}{Refl}) a)
+ ap∘-unit-l : {A : Type} {x y : A} {p q : Path x y}
+ -> (a : Path p q) -> Path (ap∘ (id{_}{id}) a)
(! (∘-unit-l q) ∘ a ∘ ∘-unit-l p)
-- definitional equalities work out such that you need an adjustment on the right
- resp∘-unit-l {A}{x}{y}{p}{.p} Refl = lemma p where
- lemma : {x y : A} (q : Id x y) -> Id Refl (! (∘-unit-l q) ∘ Refl ∘ ∘-unit-l q)
- lemma Refl = Refl
-
- subst-Id-d : {Γ : Set} {A : Γ -> Set} (f g : (x : Γ) -> A x) {M N : Γ} (p : Id M N)
- -> (p' : f M ≃ g M)
- -> Id (subst (\ x -> Id (f x) (g x)) p p')
- (respd g p ∘ resp (subst A p) p' ∘ ! (respd f p))
- subst-Id-d _ _ Refl p' = ! (∘-unit-l p' ∘ resp (λ x Refl ∘ x) (resp-id p'))
-
-
- subst-com-for-resp-of-subst :
- {Γ : Set} {θ1 θ2 : Γ} (δ : θ1 ≃ θ2)
- (A : Γ -> Set) (C : (γ : Γ) -> A γ -> Set)
- (M1 M2 : (γ : Γ) -> A γ)
- (α : (γ : Γ) -> M1 γ ≃ M2 γ)
- (M : (γ : Γ) -> C γ (M1 γ))
- -> Id (subst (λ z C z (M2 z)) δ (subst (C θ1) (α θ1) (M θ1)))
- (subst (λ _ C θ2 (M2 θ2)) (respd M δ)
- (subst (C θ2) (α θ2) (subst (λ z C z (M1 z)) δ (M θ1))))
- subst-com-for-resp-of-subst Refl A C M1 M2 α M = Refl
-
- resp-of-subst : {Γ : Set} {θ1 θ2 : Γ} {δ : θ1 ≃ θ2}
- {A : Γ -> Set} {C : (γ : Γ) -> A γ -> Set}
- {M1 M2 : (γ : Γ) -> A γ}
- {α : (γ : Γ) -> M1 γ ≃ M2 γ}
- {M : (γ : Γ) -> C γ (M1 γ)}
- -> respd (\ γ -> subst (C γ) (α γ) (M γ)) δ
- ≃ respd (λ x subst (C θ2) (α θ2) x) (respd M δ)
- ∘ subst-com-for-resp-of-subst δ A C M1 M2 α M
- resp-of-subst {δ = Refl} = Refl
+ ap∘-unit-l {A}{x}{y}{p}{.p} id = lemma p where
+ lemma : {x y : A} (q : Path x y) -> Path id (! (∘-unit-l q) ∘ id ∘ ∘-unit-l q)
+ lemma id = id
-- interchange law for a particular type A
-- objects = terms of type A
- -- morphisms = Id{A}
- -- 2-cells = Id{Id}
+ -- morphisms = Path{A}
+ -- 2-cells = Path{Path}
--
-- see Functions.agda for the interchange law for the type theory as a whole,
-- viewed as a higher category
- ichange-type : {A : Set} {x y z : A}
- {p q r : Id x y} {p' q' r' : Id y z}
- -> (a : Id p q) (b : Id q r) (c : Id p' q') (d : Id q' r')
- -> Id (resp∘ (d ∘ c) (b ∘ a)) (resp∘ d b ∘ resp∘ c a)
- ichange-type Refl Refl Refl Refl = Refl
-
- coe : {A B : Set} -> Id A B -> A -> B
- coe = subst (\ x -> x)
+ ichange-type : {A : Type} {x y z : A}
+ {p q r : Path x y} {p' q' r' : Path y z}
+ -> (a : Path p q) (b : Path q r) (c : Path p' q') (d : Path q' r')
+ -> Path (ap∘ (d ∘ c) (b ∘ a)) (ap∘ d b ∘ ap∘ c a)
+ ichange-type id id id id = id
- coe-inv-2 : {A B : Set} -> (α : Id A B) -> {M : _} -> coe α (coe (! α) M) ≃ M
- coe-inv-2 Refl = Refl
-
- coe-inv-1 : {A B : Set} -> (α : Id A B) -> {M : _} -> coe (! α) (coe α M) ≃ M
- coe-inv-1 Refl = Refl
-
- subst-inv-1 : {A : Set} (B : A -> Set) {M N : A} (α : M ≃ N) -> (\y -> subst B (! α) (subst B α y)) ≃ (\ x -> x)
- subst-inv-1 _ Refl = Refl
-
- subst-inv-2 : {A : Set} (B : A -> Set) {M N : A} (α : M ≃ N) -> (\y -> subst B α (subst B (! α) y)) ≃ (\ x -> x)
- subst-inv-2 _ Refl = Refl
+ -- interderivability
module PaulinMohring where
- jayfrompm : {A : Set} (C : (x y : A) -> Id x y -> Set)
- -> {M N : A} -> (P : Id M N)
- -> ((x : A) -> C x x Refl)
+ jayfrompm : {A : Type} (C : (x y : A) -> Path x y -> Type)
+ -> {M N : A} -> (P : Path M N)
+ -> ((x : A) -> C x x id)
-> C M N P
- jayfrompm {A} C {M}{N} P b = jay1 (λ x (p : Id M x) C M x p) P (b M)
+ jayfrompm {A} C {M}{N} P b = path-induction (λ x (p : Path M x) C M x p) (b M) P
- pmfromjay : {A : Set} {M : A} (C : (N' : A) -> Id M N' -> Set)
- -> {N : A} -> (P : Id M N)
- -> (C M Refl)
+ pmfromjay : {A : Type} {M : A} (C : (N' : A) -> Path M N' -> Type)
+ -> {N : A} -> (P : Path M N)
+ -> (C M id)
-> C N P
pmfromjay {A}{M} C {N} P b =
- (jay (λ M' N' (P' : Id M' N') (C' : (N'' : A) Id M' N'' Set) C' M' Refl C' N' P')
+ (jay (λ M' N' (P' : Path M' N') (C' : (N'' : A) Path M' N'' Type) C' M' id C' N' P')
P
(λ M' C' b' b'))
C b
- jayfrompm2 : {A : Set} (C : (x y : A) -> Id x y -> Set)
- -> {M N : A} -> (P : Id M N)
- -> ((x : A) -> C x x Refl)
+ jayfrompm2 : {A : Type} (C : (x y : A) -> Path x y -> Type)
+ -> {M N : A} -> (P : Path M N)
+ -> ((x : A) -> C x x id)
-> C M N P
- jayfrompm2 {A} C {M}{N} P b = subst (λ p C M N p) (sym-invol P)
- (jay1 (λ x p C x N (sym p)) {M} (sym P) (b N))
+ jayfrompm2 {A} C {M}{N} P b = transport (λ p C M N p) (!-invol P)
+ (path-induction (λ x p C x N (! p)) (b N) (! P))
- fire-jay-const1 : {A : Set} {B : Set}
- {M N : A} -> (P : Id M N)
+ fire-jay-const1 : {A : Type} {B : Type}
+ {M N : A} -> (P : Path M N)
-> (f : A -> B)
- -> Id (jayfrompm (\ _ _ _ -> B) P f) (f M)
- fire-jay-const1 {A}{B} P f = jay (λ x y p Id (jayfrompm (λ _ _ _ B) p f) (f x)) P (\ _ -> Refl)
+ -> Path (jayfrompm (\ _ _ _ -> B) P f) (f M)
+ fire-jay-const1 {A}{B} P f = jay (λ x y p Path (jayfrompm (λ _ _ _ B) p f) (f x)) P (\ _ -> id)
- fire-jay-const2 : {A : Set} {B : Set}
- {M N : A} -> (P : Id M N)
+ fire-jay-const2 : {A : Type} {B : Type}
+ {M N : A} -> (P : Path M N)
-> (f : A -> B)
- -> Id (jayfrompm2 (\ _ _ _ -> B) P f) (f N)
- fire-jay-const2 {A}{B} P f = jay (λ x y p Id (jayfrompm2 (λ _ _ _ B) p f) (f y)) P (\ _ -> Refl)
-
- module PathsOfficial where
- -- derive everything from J
-
- jay : {A : Set} (C : (x y : A) -> Id x y -> Set)
- -> {M N : A} -> (P : Id M N)
- -> ((x : A) -> C x x Refl)
- -> C M N P
- jay _ Refl b = b _
-
- subst : {A : Set} (p : A -> Set) {x y : A} -> Id x y -> p x -> p y
- subst C p = jay (λ x y _ C x C y) p (λ x λ x' x')
-
- resp : {A C : Set} {M N : A} (f : A -> C) -> Id M N -> Id (f M) (f N)
- resp {A}{C}{M}{N} f a = subst (\ x -> Id (f M) (f x)) a Refl
-
- resp2 : {A B C} {M N : A} {M' N' : B} (f : A -> B -> C) -> Id M N -> Id M' N' -> Id (f M M') (f N N')
- resp2 {A}{B}{C}{M}{N}{M'}{N'} f a b =
- subst (\ x -> Id (f M M') (f x N')) a (subst (λ x Id (f M M') (f M x)) b Refl)
-
- trans : {A : Set} {M N P : A} -> Id M N -> Id N P -> Id M P
- trans {A}{M}{N}{P} a b = subst (\ x -> Id M x) b a
-
- sym : {a : Set} {x y : a} -> Id x y -> Id y x
- sym p = jay (λ x y _ Id y x) p (λ _ Refl)
-
- trans-unit-l : {A : Set} {M N : A} -> (p : Id M N) -> Id (trans Refl p) p
- trans-unit-l p = jay (λ _ _ p' Id (trans Refl p') p') p (λ _ Refl)
-
- trans-unit-r : {A : Set} {M N : A} -> (p : Id M N) -> Id (trans p Refl) p
- trans-unit-r p = Refl
-
- sym-inv : {A : Set} {M N : A} (p : Id M N) -> Id (trans p (sym p)) Refl
- sym-inv p = jay (λ x y p' Id (trans p' (sym p')) Refl) p (\ _ -> Refl)
-
- resptrans : {A : Set} {x y z : A} {p q : Id x y} {p' q' : Id y z}
- -> Id p q -> Id p' q' -> Id (trans p p') (trans q q')
- resptrans a b = resp2 trans a b
-
- resptrans-unit-r : {A : Set} {x y : A} {p q : Id x y}
- -> (a : Id p q) -> Id (resptrans a (Refl{_}{Refl})) a -- definitional equalities work out such that this works unadjusted
- resptrans-unit-r a = jay (λ _ _ p Id (resptrans p (Refl {_} {Refl})) p) a (λ _ Refl)
-
- resptrans-unit-l : {A : Set} {x y : A} {p q : Id x y}
- -> (a : Id p q) -> Id (resptrans (Refl{_}{Refl}) a)
- ((trans (trans-unit-l p) (trans a (sym (trans-unit-l q)))) )
- -- definitional equalities work out such that you need an adjustment on the right
- resptrans-unit-l a = jay {_}
- (λ p' q' a'
- Id (resp (trans Refl) a')
- (trans (trans-unit-l p') (trans a' (sym (trans-unit-l q')))))
- {_} {_} a
- (λ x
- jay
- (λ xend _ x'
- Id Refl
- (subst (Id (subst (Id xend) x' Refl))
- (subst (Id x')
- (jay (λ x0 y _ Id y x0)
- (jay (λ _ _ p' Id (subst (Id _) p' Refl) p') x' (λ _ Refl))
- (λ _ Refl))
- Refl)
- (jay (λ _ _ p' Id (subst (Id _) p' Refl) p') x' (λ _ Refl))))
- x (λ _ Refl))
-
- -- would be a one-liner using pattern matching
- -- nothing about the interchange law depends on talking about loops
- trans-resptrans-ichange : {A : Set} {x y z : A}
- (p q : Id x y)
- -> (a : Id p q) (r : Id x y) (b : Id q r)
- (p' q' : Id y z) (c : Id p' q')
- (r' : Id y z) (d : Id q' r')
- -> Id (resptrans (trans a b) (trans c d)) (trans (resptrans a c) (resptrans b d))
- trans-resptrans-ichange {A}{x}{y}{z} p q a = jay
- (λ p' q' a'
- (r : Id x y) (b : Id q' r) (p0 q0 : Id y z) (c : Id p0 q0) (r' : Id y z)
- (d : Id q0 r')
- Id (resptrans (trans a' b) (trans c d))
- (trans (resptrans a' c) (resptrans b d)))
- a
- (λ pq r b
- jay
- (λ pq' r' b'
- (p' q' : Id y z) (c : Id p' q') (r0 : Id y z) (d : Id q' r0)
- Id (resptrans (trans Refl b') (trans c d))
- (trans (resptrans Refl c) (resptrans b' d)))
- b
- (λ pqr p' q' c
- jay
- (λ p0 q0 c'
- (r' : Id y z) (d : Id q0 r')
- Id (resptrans Refl (trans c' d))
- (trans (resptrans Refl c') (resptrans Refl d)))
- c
- (λ p'q' r' d
- jay
- (λ p'q0 r0 d'
- Id (resptrans Refl (trans Refl d'))
- (trans Refl (resptrans Refl d')))
- d (λ _ Refl))))
-
-
- {- more general interchange?
- hcomp : {Γ : Set} {Δ : Set} {θ1' θ2' : Γ -> Δ} {θ1 θ2 : Γ}
- -> (δ1 : Id θ1' θ2')
- -> (δ2 : Id θ1 θ2)
- -> Id (θ1' θ1) (θ2' θ2)
- hcomp δ1 δ2 = resp2 (λ x y → x y) δ1 δ2
-
- ichange : {Γ : Set} {Δ : Set} {θ1' θ2' θ3' : Γ -> Δ} {θ1 θ2 θ3 : Γ}
- -> (δ1' : Id θ1' θ2')
- -> (δ1 : Id θ1 θ2)
- -> (δ2' : Id θ2' θ3')
- -> (δ2 : Id θ2 θ3)
- -> Id (hcomp (trans δ1' δ2') (trans δ1 δ2)) (trans (hcomp δ1' δ1) (hcomp δ2' δ2))
- ichange δ1' δ1 δ2' δ2 = {!!}
- -}
-
- -- fire-subst : {Γ A : Set} (f g : Γ -> A) {M N : Γ} {p : Id M N}
- -- -> (p' : Id (f M) (g M)) -> Id (subst (\ x -> Id (f x) (g x)) p p') (trans (sym (resp f p)) (trans {!!} (resp g p)))
- -- fire-subst _ _ {p = Refl} p' = sym (trans (trans-unit-l (trans p' Refl)) (trans-unit-r _)) -- FIXME do with J
-