Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

stuff

  • Loading branch information...
commit d9078606d85bdccb4484fd7ce094cfba5e4efde5 1 parent 0b5915b
Dan Licata authored
9 .gitignore
View
@@ -1,3 +1,12 @@
+*.aux
+*.bbl
+*.blg
+*.dvi
+*.log
+*.toc
+*.ps
+*.pdf
+*.synctex.gz
*.agdai
TAGS
54 computational-interp/hcanon/HSetProof-PathOver.agda
View
@@ -1,4 +1,4 @@
-{-# OPTIONS --type-in-type --no-termination-check #-}
+{-# OPTIONS --type-in-type --no-termination-check #-}
{- BIG ISSUES:
(1) What to do about definitional equality.
@@ -316,15 +316,36 @@ module computational-interp.hcanon.HSetProof-PathOver where
id α)
(QOver-irrel _ _ B* _ _ (transportRQ _ B* _ rM1))
+ -- ----------------------------------------------------------------------
-- definitionally equal types give coercable R's
-- FIXME it's no longer true that these are actually definitionally equal,
-- because of the Q components of R_Pi---e.g. there are transportR's in different places
-- for different definitionally equal types (see the case for unlam, e.g.).
-- But maybe we can still get a coercion here?
+
+ {-
+ R-deq-bool : ∀ {Γ A θ M} (Γ* : Ctx Γ) (A1* : Ty Γ* A) → (eq : A == \ _ -> Bool) -- really only need equality, not paths
+ (rθ : RC Γ* θ) → R Γ* bool rθ M → R Γ* A1* rθ (coe (! (ap≃ eq)) M)
+ R-deq-bool Γ* bool eq rθ rM = {!!}
+ R-deq-bool Γ* prop eq rθ rM = {!!}
+ R-deq-bool Γ* (proof M₁) eq rθ rM = {!!}
+ R-deq-bool {θ = θ} Γ* (Π A1* A1*₁) eq rθ rM = {!ap≃ eq {θ}!}
+ R-deq-bool Γ* (subst A1* θ'*) eq rθ rM = {!!}
+ R-deq-bool Γ* (pathOver A1* δ* M* N*) eq rθ rM = {!!}
+ R-deq-bool .(Γ* , A1*) (w {Γ} {A} {B} {Γ*} A1* A1*₁) eq rθ rM = {!!}
+ R-deq-bool Γ* (subst1 A1*₁ M₁) eq rθ rM = {!!}
+ -}
+
postulate
R-deq : {Γ A θ M} (Γ* : Ctx Γ) (A* A1* : Ty Γ* A) (rθ : RC Γ* θ) R Γ* A* rθ M R Γ* A1* rθ M
-- R-deq Γ* A* A1* rθ = lib.PrimTrustMe.unsafe-cast
+ Q-deq : {Γ A θ1 θ2 δ M1 M2 α}
+ {Γ* : Ctx Γ} {rθ1 : RC Γ* θ1} {rθ2 : RC Γ* θ2} (rδ : QC Γ* rθ12 δ)
+ (A* A1* : Ty Γ* A) {rM1 : R Γ* A* rθ1 M1} {rM2 : R Γ* A* rθ2 M2}
+ QOver rδ A* rM1 rM2 α
+ QOver rδ A1* (R-deq _ A* A1* rθ1 rM1) (R-deq _ A* A1* rθ2 rM2) α
+
QOver-irrel rδ rδ' A* rM1 rM2 rα = fund-changeover rδ rδ' A* rM1 rM2 id rα
-- ----------------------------------------------------------------------
@@ -682,21 +703,14 @@ module computational-interp.hcanon.HSetProof-PathOver where
(fund-refl _ (subst A* θ*) _ (fund _ (subst A* θ*) _ M*))
fund .Γ* ._ rθ (tr{Γ}{A}{C}{Γ*}{Γ'*} C* {θ1}{θ2} δ N) = fund-transport Γ'* C* (funds Γ* Γ'* rθ θ1) (funds Γ* Γ'* rθ θ2) (fundps Γ* Γ'* rθ θ1 θ2 δ) (fund Γ* _ rθ N)
- fund {θ = θ} .Γ* ._ rθ (uap{Γ}{Γ*}{P}{Q} f* g*) = {!!} , {!!} -- FIXME avoid/deal with equality
-{-
- (λ x rx → transportP (fund Γ* prop rθ Q) _ id (interp f* (θ , x)) (coe (interp (uap{P = P}{Q = Q} f* g*) θ) x)
- (! (ap≃ (type≃β (interp-uap-eqv{P = P}{Q = Q} f* g* θ))))
- (fund (Γ* , proof P) (w (proof P) (proof Q)) (rθ , rx) f*)) ,
- (λ x rx → transportP (fund Γ* prop rθ P) _ id (interp g* (θ , x)) (coe (! (interp (uap{P = P}{Q = Q} f* g*) θ)) x)
- (! (ap≃ (type≃β! (interp-uap-eqv{P = P}{Q = Q} f* g* θ))))
- (fund (Γ* , proof Q) (w (proof Q) (proof P)) (rθ , rx) g*))
--}
- -- later fund Γ* ._ rθ (lam={A* = A*}{B* = B*} f* g* α*) = λ x rx → fund-lam= Γ* A* B* f* g* α* rθ x rx
-
+ fund {θ = θ} .Γ* ._ rθ (uap{Γ}{Γ*}{P}{Q} f* g*) = coe {!!} -- make lemma
+ (Q-deq _ prop (subst prop ·) {fund _ prop rθ P} {fund _ prop rθ Q} ((λ x rx transportP (fund Γ* prop rθ Q) _ _ _ _ {!univalenceβ!} (fund _ _ (rθ , rx) f*)) ,
+ {!FIXME symmetric!}))
fund .Γ* .A* rθ (deq{Γ}{A}{Γ*}{A1*}{A*} M) = R-deq Γ* A1* A* rθ (fund Γ* A1* rθ M)
fund Γ* ._ rθ <>⁺ = fund-<>⁺ Γ* rθ
fund Γ* ._ rθ (split1 C* M1 M) = fund-split1 Γ* C* M1 M rθ
-- fund ._ B* rθ (unlam {Γ* = Γ*} {A* = A*} M) = fst (fund Γ* (Π A* B*) (fst rθ) M) _ (snd rθ)
+ -- later fund Γ* ._ rθ (lam={A* = A*}{B* = B*} f* g* α*) = λ x rx → fund-lam= Γ* A* B* f* g* α* rθ x rx
fund-<> Γ* rθ = <>
fund-<>⁺ Γ* rθ = id
@@ -705,13 +719,11 @@ module computational-interp.hcanon.HSetProof-PathOver where
-- (fst (fund Γ* (Π A* B*) rθ g*) x rx) (! (Π≃β (λ x₁ → interp α* (_ , x₁))))
-- (fund (Γ* , A*) _ (rθ , rx) α*)
- fund-split1 {θ = θ} Γ* {C} C* M1 M rθ = {!FIXME!}
-{-
- transportR (Γ* , proof unit⁺) C* (rθ , (fund Γ* (proof unit⁺) rθ M)) (apd (split1⁺ (λ x → C (θ , x)) (interp M1 θ)) (! (fund Γ* (proof unit⁺) rθ M)))
- (fund-tr1-unit⁺ {α = ! (fund Γ* (proof unit⁺) rθ M)}
- Γ* C* rθ id (fund Γ* (proof unit⁺) rθ M) <> -- uses the fact that all paths are reducible in Prooff(-)
- (fund Γ* (subst1 C* <>⁺) rθ M1))
--}
+ fund-split1 {θ = θ} Γ* {C} C* M1 M rθ = transportR _ C* _ (apd (split1⁺ (λ x C (θ , x)) (interp M1 θ))
+ (! (fund Γ* (proof unit⁺) rθ M))
+ ∘ {!coh!})
+ (fund-tr1-unit⁺ {α = path-to-pathover (λ _ Unit⁺) (! (fund Γ* (proof unit⁺) rθ M))} Γ* C* rθ id (fund Γ* (proof unit⁺) rθ M) <>
+ (fund Γ* (subst1 C* <>⁺) rθ M1))
-- ----------------------------------------------------------------------
-- ap
@@ -734,7 +746,7 @@ module computational-interp.hcanon.HSetProof-PathOver where
fund-ap Γ* void rθ12= (λ x x₁ x₁) , (λ y x x)
fund-ap Γ* <> rθ12= <>
fund-ap Γ* <>⁺ rθ12= <>
- fund-ap Γ* (split1 C* f f₁) rθ12= {!FIXME!}
+ fund-ap Γ* (split1 C* f f₁) rθ12= {!fund _ (proof unit⁺) rθ1 f₁ !}
fund-ap Γ* (abort f) rθ12= Sums.abort (fund Γ* (proof void) rθ1 f)
fund-ap Γ* (if f f₁ f₂) rθ12= {!FIXME!}
fund-ap {δ = δ} Γ* (lam {A = A} {A* = A*} {B* = B*} f) rθ12=
@@ -775,7 +787,7 @@ module computational-interp.hcanon.HSetProof-PathOver where
(fund-ap Γ* M (fst rθ1) (fst rθ2) rδ1 _ (snd rθ2)))
fund-ap Γ* (lam= f f₁ f₂) rθ1 rθ2 rδ = <>
-}
- fund-ap Γ* (deq f) rθ12= {!fund-ap Γ* f rθ12!} -- FIXME
+ fund-ap Γ* (deq{A* = A*} {A'* = A'*} f) rθ12= Q-deq _ A* A'* (fund-ap Γ* f rθ12)
{-
example : Tm · (proof unit⁺)
2  computational-interp/hcanon/HSetProof.agda
View
@@ -609,7 +609,7 @@ module computational-interp.hcanon.HSetProof where
fund-ap Γ* (tr C* α f) rθ12= {!!}
fund-ap Γ* (uap f₂ f₃) rθ12= <>
-}
- fund-ap ._ (unlam {Γ* = Γ*} {A* = A*} {B* = B*} M) (rθ1 , rM1) (rθ2 , rM2) (δ1 , α1 , eq , rδ1 , rα1) = ?
+ fund-ap ._ (unlam {Γ* = Γ*} {A* = A*} {B* = B*} M) (rθ1 , rM1) (rθ2 , rM2) (δ1 , α1 , eq , rδ1 , rα1) = {!!}
-- transportQ (Γ* , A*) B* rθ2 _ _ {!!}
-- (fund-trans (Γ* , A*) B* rθ2 _ _ _ (fund-trans (Γ* , A*) B* rθ2 _ _ _ (coe {!!}
-- (fund-sym (Γ* , A*) B* _ _ _
23 lib/PathOver.agda
View
@@ -234,6 +234,29 @@ module lib.PathOver where
path-to-pathover : {Δ : Type} (A : Δ Type) {θ : Δ} {M N : A θ} M == N PathOver A id M N
path-to-pathover A id = id
+ apdo-split-def :{Δ : Type} {C : Δ Unit⁺ Type}
+ (f : (θ : Δ) C θ <>⁺)
+ (M : Δ Unit⁺)
+ {θ1 θ2 : Δ} (δ : θ1 == θ2)
+ (x y : Unit⁺) (α : PathOver (λ _ Unit⁺) δ x y)
+ PathOver (λ z C (fst z) (snd z)) (pair= δ α)
+ (split1⁺ (C θ1) (f θ1) x)
+ (split1⁺ (C θ2) (f θ2) y)
+ apdo-split-def {C = C} f M δ = split1⁺ _ (split1⁺ _ (λ α changeover (λ p C (fst p) (snd p)) FIXME -- need UIP for Unit⁺ and some massaging
+ (over-o-ap (λ p C (fst p) (snd p)) {θ1 = λ θ θ , <>⁺}
+ (apdo f δ))))
+ where postulate FIXME : {A : Type} -> A
+
+ postulate
+ apdo-split : {Δ : Type} {C : Δ Unit⁺ Type}
+ (f : (θ : Δ) C θ <>⁺)
+ (M : Δ Unit⁺)
+ {θ1 θ2 : Δ} (δ : θ1 == θ2)
+ coe PathOverΠ (apdo (\ θ split1⁺ (\ x (C θ x)) (f θ)) δ) ==
+ (\ x y α apdo-split-def {C = C} f M δ x y α)
+ -- apdo-split f M id = λ≃ (split1⁺ _ (λ≃ (split1⁺ _ (λ≃ (λ α → {!!})))))
+
+
Square : {Δ} {θ11 θ12 θ21 θ22 : Δ} 1- : θ11 == θ12) (δ2- : θ21 == θ22) (δ-1 : θ11 == θ21) (δ-2 : θ12 == θ22) Type
Square δ1- δ2- δ-1 δ-2 = δ-2 == δ2- ∘ δ-1 ∘ ! δ1-
Please sign in to comment.
Something went wrong with that request. Please try again.