Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

some cleanup

  • Loading branch information...
commit b1f6fde056f6bc137d724e4622873703aea6705d 1 parent 86acbc3
@dlicata335 authored
View
33 homotopy/blakersmassey/ooTopos.agda
@@ -5,6 +5,11 @@ open FatPushout
open ConnectedMap
open Truncation
+-- P : X → Y → Type
+-- Z = Σ x,y.Z x y
+-- f = π1
+-- g = π1 o π2
+-- for each x:X, { y:Y & z:P x y } is i-connected
module homotopy.blakersmassey.ooTopos (Z X Y : Type)
(i' j' : _)
(f : ZX) (g : ZY)
@@ -88,9 +93,9 @@ module homotopy.blakersmassey.ooTopos (Z X Y : Type)
i+j = plus2 i' j'
- W = Pushout f g
+ W = Pushout f g -- TODO: pushout for predicate
- X×WY = Pullback{W} inl inr
+ X×WY = Pullback{W} inl inr -- ∀ (x , y) → P x y → inl x == inr y
gluelr : (z : Z) Path{W} (inl (f z)) (inr (g z))
gluelr z = gluer z ∘ gluel z
@@ -118,7 +123,7 @@ module homotopy.blakersmassey.ooTopos (Z X Y : Type)
codes-r : Z×XZ Z×WY
codes-r (z1 , z2 , p) = z1 , g z2 , (gluelr z2 ∘ ap inl p ∘ ! (gluel z1))
- codes-l : Z×YZ Z×WX
+ codes-l : Z×YZ Z×WX -- g z' = f z
codes-l (z1 , z2 , p) = z1 , f z2 , ! (gluelr z2) ∘ ap inr p ∘ gluer z1
-- source of Codes middle map
@@ -258,7 +263,7 @@ module homotopy.blakersmassey.ooTopos (Z X Y : Type)
(z1 , (z2 , p2) , z3 , p3) ∎
comp2 : (x : _) prod-pb (pb-prod x) ≃ x
- comp2
+ comp2 = {!!}
prod≃pb-l : PB-l ≃ Z×XZ×YZ
@@ -276,6 +281,7 @@ module homotopy.blakersmassey.ooTopos (Z X Y : Type)
→ Equiv (Trunc i+j (HFiber codes-l (f2 (z , z' , p))))
(Trunc i+j (HFiber codes-m (z , z' , p)))
eqvlm z z' p = {!!}
+-}
Codes : (z : Z) (w : W) Path (inm z) w Type
Codes z = Pushout-elim _
@@ -283,14 +289,15 @@ module homotopy.blakersmassey.ooTopos (Z X Y : Type)
(λ z' p Trunc i+j (HFiber codes-m (z , z' , p)))
(λ y p Trunc i+j (HFiber codes-r (z , y , p)))
{!!}
- (λ z' →
- λ≃
- (λ p →
- ap (λ p' → Trunc i+j (HFiber codes-r p')) (pair≃ id (pair≃ id (!-inv-r-front (gluer z') p))) ∘
- ua (Codes-glue.eqvmr z z' (! (gluer z') ∘ p)) ∘
- ap (λ p' → Trunc i+j (HFiber codes-m (z , z' , p')))
- (transport-Path-right (! (gluer z')) p))
- ∘ transport-→-pre' (λ z0 → Path (inm z) z0) (gluer z') _)
+ {!!}
+ -- (λ z' →
+ -- λ≃
+ -- (λ p →
+ -- ap (λ p' → Trunc i+j (HFiber codes-r p')) (pair≃ id (pair≃ id (!-inv-r-front (gluer z') p))) ∘
+ -- ua (Codes-glue.eqvmr z z' (! (gluer z') ∘ p)) ∘
+ -- ap (λ p' → Trunc i+j (HFiber codes-m (z , z' , p')))
+ -- (transport-Path-right (! (gluer z')) p))
+ -- ∘ transport-→-pre' (λ z0 → Path (inm z) z0) (gluer z') _)
{-
(λ z' → λ≃ (λ p → ua (Codes-gluer.eqv z z' p) ∘
ap (λ p' → Trunc i+j (HFiber codes-m (z , z' , p'))) (transport-Path-right (! (gluer z')) p))
@@ -355,4 +362,4 @@ module homotopy.blakersmassey.ooTopos (Z X Y : Type)
theorem : ConnectedMap i+j glue-map
theorem (x , y , p) = ntype (glue-map-connected x y p)
--}
+
View
2  homotopy/pinsn-paper/formalization.tex
@@ -0,0 +1,2 @@
+
+adjust trick
View
0  homotopy/BlakersMasseyInfTopos.agda → homotopy/scraps/BlakersMasseyInfTopos.agda
File renamed without changes
View
8 lib/Char.agda
@@ -3,6 +3,8 @@
open import lib.Nat
open import lib.Bool
+open import lib.Sums
+open import lib.First
module lib.Char where
@@ -28,3 +30,9 @@ module lib.Char where
equal : Char -> Char -> Bool
equal = primCharEquality
+ equals : (c d : Char) Either (c == d) (c == d Void)
+ equals c d with equal c d
+ ... | True = Inl FIXME where
+ postulate FIXME : {A : Set} A
+ ... | False = Inr (\ _ -> FIXME) where
+ postulate FIXME : {A : Set} A
View
7 lib/Sums.agda
@@ -1,6 +1,7 @@
{-# OPTIONS --type-in-type --without-K #-}
open import lib.First
+open import lib.Nat
module lib.Sums where
@@ -10,6 +11,10 @@ module lib.Sums where
Inl : a -> Either a b
Inr : b -> Either a b
+ data Fin : Nat → Set where
+ Z : {n} Fin (S n)
+ S : {n} Fin n Fin (S n)
+
module Sums where
case : {A B : Type} (C : Either A B Type)
((x : A) C (Inl x))
@@ -27,4 +32,4 @@ module lib.Sums where
abort : {A : Type} Void A
abort ()
-
+
View
81 programming/PartialBijection.agda
@@ -0,0 +1,81 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open Truncation
+
+module programming.PartialBijection where
+
+ _<->_ : Type Type Type
+ A <-> B = (A B) × (B A)
+
+ -- FIXME: need truncation?
+ InDom : {A B : Type} (f : A Maybe B) A Type
+ InDom f x = Trunc -1 (Σ \ y f x == Some y)
+
+ InIm : {A B : Type} (f : A Maybe B) B Type
+ InIm f y = Trunc -1 (Σ \ x f x == Some y)
+
+ HSet-Maybe : {A : Type} HSet A HSet (Maybe A)
+ HSet-Maybe = {!!}
+
+ module B (A B : Type)
+ (HSetA : HSet A) (HSetB : HSet B) -- FIXME: implied by below
+ (decA : DecPath A)
+ (decB : DecPath B) where
+
+ record IsPartialBijection (f : A → Maybe B) : Type where
+ constructor partialbij
+ field
+ g : B Maybe A
+ adjoint : (x : A) (y : B) (f x == Some y) <-> (Some x == g y)
+
+{-
+ record IsPartialBijection2 (f : A → Maybe B) : Type where
+ constructor partialbij2
+ field
+ g : Σ (InIm f) → A
+ adjoint : (x : A) (y : Σ (InIm f)) → (f x == Some (fst y)) <-> (x == g y)
+
+
+ tob : (f : A → Maybe B) → (pb : IsPartialBijection2 f) → Equiv (Σ (InDom f)) (Σ (InIm f))
+ tob f (partialbij2 g adj) = {!!} where
+ total-on-dom1 : Σ (InDom f) → Σ (InIm f)
+ total-on-dom1 (x , indom) with f x
+ ... | Some y = y , [ x , {!need inspect!} ]
+ ... | None = {!!} , Trunc-func (\ p → Sums.abort {!snd p!}) indom
+
+ on-im1 : (p : Σ (InIm f)) → (InDom f (g p))
+ on-im1 (y , p') = [ y , snd (adj (g (y , p')) (y , p')) id ]
+-}
+
+{-
+ works without truncations
+
+ toequiv : (f : A → Maybe B) → IsPartialBijection f → Equiv (Σ (InDom f)) (Σ (InIm f))
+ toequiv f (partialbij g adj) = improve (hequiv total-on-dom1 total-on-dom2 (λ _ → id) (λ _ → id)) where
+ total-on-dom1 : Σ (InDom f) → Σ (InIm f)
+ total-on-dom1 (x , y , eq) = y , x , eq
+
+ total-on-dom2 : Σ (InIm f) → Σ (InDom f)
+ total-on-dom2 (y , x , eq) = x , y , eq
+-}
+
+ fromequiv : (f : A Maybe B) (e : Equiv (Σ (InDom f)) (Σ (InIm f))) IsPartialBijection f
+ fromequiv f (f' , isequiv g' α β _) = partialbij {!!} {!!} where
+ g : B Maybe A
+ g b = Some (fst (g' (b , {!!})))
+
+{-
+ tob : (pb : PartialBijection) → Equiv (Σ (Dom (PartialBijection.f pb))) (Σ (Dom (PartialBijection.g pb)))
+ tob (partialbij f g adj) = improve (hequiv total-on-dom1 total-on-dom2 (λ x → pair≃ id (pair≃ id (HSet-UIP (HSet-Maybe HSetB) _ _ _ _))) (λ y → pair≃ id (pair≃ id (HSet-UIP (HSet-Maybe HSetA) _ _ _ _)))) where
+ total-on-dom1 : Σ (Dom f) → Σ (Dom g)
+ total-on-dom1 (x , y , eq) = y , x , ! (fst (adj x y) eq)
+
+ total-on-dom2 : Σ (Dom g) → Σ (Dom f)
+ total-on-dom2 (y , x , eq) = x , y , (snd (adj x y) (! eq))
+
+ fromb : (f : A → Maybe B) (g : B → Maybe A)
+ → Equiv (Σ (Dom f)) (Σ (Dom g))
+ → PartialBijection
+ fromb f g (f' , isequiv g' α β _) = partialbij f g (λ x y → (λ p → {! (α (x , y , p)) !}) , (λ q → {!!}))
+-}
View
15 programming/PartialBijection2.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+
+module programming.PartialBijection2 where
+
+ module B (A B : Type) (D : AType) (decD : (x : A) → Either (D x) (D xVoid)) where
+
+ run : Equiv (Σ D) B A Maybe B
+ run (f , _) x with decD x
+ ... | Inl indom = Some (f (x , indom))
+ ... | Inr _ = None
+
+
+
View
128 programming/Patch.agda
@@ -0,0 +1,128 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude hiding (id ; _∘_ ; !)
+
+module programming.Patch where
+
+ _∘p_ = lib.Prelude._∘_
+ !p = lib.Prelude.!
+ idp = \{A}{x} lib.Prelude.id{A}{x}
+
+ data Vec (A : Set) : Nat → Set where
+ [] : Vec A 0
+ _::_ : {n : Nat} A Vec A n Vec A (S n)
+
+ module R (n : Nat) where
+
+ data Patch : Set where
+ id : Patch
+ _∘_ : Patch Patch Patch
+ ! : Patch Patch
+ _↔_at_ : Char Char Fin n Patch
+
+ infixr 8 _∘_
+
+ swapchar : Char Char Char Char
+ swapchar a b c with Char.equals a c
+ ... | Inl _ = b
+ ... | Inr _ with Char.equals b c
+ ... | Inl _ = a
+ ... | Inr _ = c
+
+ swapchar-inv : (a b c : Char) swapchar a b (swapchar a b c) == c
+ swapchar-inv a b c with Char.equals a c
+ ... | Inl a=c with Char.equals a b
+ ... | Inl a=b = a=c ∘p !p a=b
+ ... | Inr p with Char.equals b b
+ ... | Inl _ = a=c
+ ... | Inr neq = Sums.abort (neq idp)
+ swapchar-inv a b c | Inr a!=c with Char.equals b c
+ ... | Inl b=c with Char.equals a a
+ ... | Inl _ = b=c
+ ... | Inr neq = Sums.abort (neq idp)
+ swapchar-inv a b c | Inr a!=c | Inr b!=c with Char.equals a c
+ ... | Inl eq = Sums.abort (a!=c eq)
+ ... | Inr _ with Char.equals b c
+ ... | Inl eq = Sums.abort (b!=c eq)
+ ... | Inr neq = idp
+
+ swapchar≃ : (a b : Char) Equiv Char Char
+ swapchar≃ a b = improve (hequiv (swapchar a b) (swapchar a b) (swapchar-inv a b) (swapchar-inv a b))
+
+ apply-at : {A : Set} {n : Nat} (f : A A) (i : Fin n) Vec A n Vec A n
+ apply-at f () []
+ apply-at f Z (x :: v) = f x :: v
+ apply-at f (S i) (x :: v) = x :: apply-at f i v
+
+ apply-at-inv : {A : Set} {n : Nat} (f : Equiv A A) (i : Fin n) (v : Vec A n)
+ (apply-at (fst f) i (apply-at (IsEquiv.g (snd f)) i v)) == v
+ apply-at-inv f () []
+ apply-at-inv f Z (x :: v) = ap (λ x₁ x₁ :: v) (IsEquiv.β (snd f) x)
+ apply-at-inv f (S i) (x :: v) = ap (λ xs x :: xs) (apply-at-inv f i v)
+
+ apply-at-equiv : {A : Set} {n : Nat} (f : Equiv A A) (i : Fin n) Equiv (Vec A n) (Vec A n)
+ apply-at-equiv f i = improve (hequiv (apply-at (fst f) i) (apply-at (IsEquiv.g (snd f)) i)
+ (apply-at-inv (!equiv f) i) (apply-at-inv f i))
+
+ -- swapat a b i v permutes a and b at position i in v
+ swapat : Char Char Fin n Vec Char n Vec Char n
+ swapat a b i = apply-at (swapchar a b) i
+
+ interp : Patch (Vec Char n Vec Char n) ×
+ (Vec Char n Vec Char n)
+ interp id = (λ x x) , (λ x x)
+ interp (q ∘ p) = fst (interp q) o fst (interp p) ,
+ snd (interp p) o snd (interp q)
+ interp (! p) = snd (interp p) , fst (interp p)
+ interp (a ↔ b at i) = swapat a b i , swapat a b i
+
+ mutual
+ interp-lr : (p : Patch) (v : Vec Char n) snd (interp p) (fst (interp p) v) == v
+ interp-lr id v = idp
+ interp-lr (q ∘ p) v = interp-lr p v ∘p
+ ap≃
+ (ap (λ x snd (interp p) o x o fst (interp p))
+ (λ≃ (λ x interp-lr q x)))
+ interp-lr (! p) v = interp-rl p v
+ interp-lr (a ↔ b at i) v = IsEquiv.α (snd (apply-at-equiv (swapchar≃ a b) i)) v
+
+ interp-rl : (p : Patch) (v : Vec Char n) fst (interp p) (snd (interp p) v) == v
+ interp-rl id v = idp
+ interp-rl (q ∘ p) v = interp-rl q v ∘p
+ ap≃
+ (ap (λ x fst (interp q) o x o snd (interp q))
+ (λ≃ (λ x interp-rl p x)))
+ interp-rl (! p) v = interp-lr p v
+ interp-rl (a ↔ b at i) v = IsEquiv.β (snd (apply-at-equiv (swapchar≃ a b) i)) v
+
+ module Infer where
+
+ Spec = Vec (Maybe Char) n
+
+ editc : Char Char Char Char
+ editc a b c with Char.equals a c
+ ... | Inl _ = b
+ ... | Inr _ = c
+
+ postulate
+ R : Type
+ mkr : Spec R
+ edit : (c d : Char) (i : Fin n) {φ : Spec}
+ (mkr (apply-at (\ _ -> Some d) i φ)) == (mkr (apply-at (\ _ -> Some d) i φ))
+
+ module Test where
+ module TestR = R 3
+ open TestR public
+
+ example : Vec Char 3
+ example = 'a' :: 'u' :: 's' :: []
+
+ patch = ('a' ↔ 'b' at Z) ∘ ('x' ↔ 'y' at (S Z)) ∘ ('s' ↔ 'b' at (S (S Z)))
+
+ open Infer
+ test : Path (mkr (apply-at (λ _ Some 'd') (S Z) (None :: None :: None :: [])))
+ (mkr (apply-at (λ _ Some 'b') Z _))
+ test = edit 'a' 'b' Z ∘p edit 'c' 'd' (S Z)
+
+ open Test
+
Please sign in to comment.
Something went wrong with that request. Please try again.