finish szumi F0

IF.agda

@@ -5,7 +5,7 @@ module IF where
 open import Lib hiding (id; _∘_)
 
 infixl 3 _▶c_ _▶P_
-infixr 5 _$S_ _⇒P_
+infixr 5 _$S_ _⇒P_ _⇒̂S_
 infixl 7 _[_]T
 infixl 8 _[_]tP
 infixl 8 _[_]t

IFReindexing.agda

@@ -29,21 +29,33 @@ open IFW Ω ω
 ᴿc ε       = lift tt
 ᴿc (σ , t) = ᴿc σ , ᴿS t
 
-ᴿt : ∀{B}{Γc}(σ : Sub Ωc Γc)(t : Tm Γc B) → (t ᵃt) (ᴿc σ) ≡ ᴿS (t [ σ ]t)
-ᴿt (σ , s) (var vvz)     = refl
-ᴿt (σ , s) (var (vvs v)) = ᴿt σ (var v)
-ᴿt  ε      (t $S τ)      = happly (ᴿt ε t) τ
-ᴿt (σ , s) (t $S τ)      = happly (ᴿt (σ , s) t) τ
+ᴿt= : ∀{B}{Γc}(σ : Sub Ωc Γc)(t : Tm Γc B) → (t ᵃt) (ᴿc σ) ≡ ᴿS (t [ σ ]t)
+ᴿt= (σ , s) (var vvz)     = refl
+ᴿt= (σ , s) (var (vvs v)) = ᴿt= σ (var v)
+ᴿt=  ε      (t $S τ)      = happly (ᴿt= ε t) τ
+ᴿt= (σ , s) (t $S τ)      = happly (ᴿt= (σ , s) t) τ
 
-ᴿtid : ∀{B}(t : Tm Ωc B) → (t ᵃt) (ᴿc id) ≡ ᴿS t
-ᴿtid t = ᴿt id t
-{-# REWRITE ᴿtid #-}
+ᴿt=id : ∀{B}(t : Tm Ωc B) → (t ᵃt) (ᴿc id) ≡ ᴿS t
+ᴿt=id t = ᴿt= id t
+{-# REWRITE ᴿt=id #-}
 
-ᴿP : (A : TyP Ωc)(α : (ᴱP A ᵃP) ωc) → _ᵃP {suc zero} A (ᴿc id)
-ᴿP (El a)   α = α , {!!}
-ᴿP (Π̂P T A) ϕ = λ τ → ᴿP (A τ) (ϕ τ)
-ᴿP (a ⇒P A) ϕ = λ α → ᴿP A (ϕ (₁ α))
+ᴿv : ∀(v : Var Ωc U) α → ˢt (ᴱt (var v)) ωcˢ α
+ᴿv vvz α = {!!}
+ᴿv (vvs v) α = {!!}
+
+ᴿt : ∀{B}(t : Tm Ωc U) α → hdfill t (ˢt (ᴱt t) ωcˢ α)
+ᴿt t α = {!!}
+
+ᴿP : ∀ A (α : (ᴱP A ᵃP) ωc) (αˢ : ˢP (ᴱP A) ωcˢ (ʷP A α (Lift _ ⊤))) → _ᵃP {suc zero} A (ᴿc id)
+ᴿP (El a)   α αˢ = α , {!!} --coe (hdfill a & (αˢ ⁻¹)) {!!}
+ᴿP (Π̂P T A) ϕ ϕˢ = λ τ → ᴿP (A τ) (ϕ τ) (ϕˢ τ)
+ᴿP (a ⇒P A) ϕ ϕˢ = λ α → ᴿP A (ϕ (₁ α)) {!!}
+
+ᴿP' : ∀{A}(tP : TmP Ω A) → _ᵃP {suc zero} A (ᴿc id)
+ᴿP' {El a}   tP = (ᴱtP tP ᵃtP) ω , {!!}
+ᴿP' {Π̂P T A} tP = λ τ → ᴿP' (tP $̂P τ)
+ᴿP' {a ⇒P A} tP = λ { α → ᴿP' {A} (tP $P {!!}) } -- nope
 
 ᴿC : ∀{Γ}(σP : SubP Ω Γ) → _ᵃC {suc zero} Γ (ᴿc id)
 ᴿC εP                   = lift tt
-ᴿC (_,P_ {A = A} σP tP) = ᴿC σP , ᴿP A ((ᴱtP tP ᵃtP) ω)
+ᴿC (_,P_ {A = A} σP tP) = ᴿC σP , ᴿP A ((ᴱtP tP ᵃtP) ω) {!!} --(ˢtP (ᴱtP tP) ωˢ)

IFSzumi.agda

@@ -29,26 +29,61 @@ module El {Γc : SCon} {υc : Set} (υ : _ᵃC {zero} (CodC Γc) (_ , υc)) wher
   ElC (Γ ▶P A) = ElC Γ ▶P ElP A
 
 -- Functor from algebras to Szumified algebras
+-- F0 is the code part, F1 is the element part of the result
+F0S : TyS → Set
+F0S U        = ⊤
+F0S (T ⇒̂S B) = T × F0S B
+
 F0c : (Γc : SCon) → Set
 F0c ∙c        = ⊤
-F0c (Γc ▶c B) = F0c Γc ⊎ ⊤
+F0c (Γc ▶c B) = F0c Γc ⊎ F0S B
+
+hd : ∀{Γc B}(t : Tm Γc B) → TyS
+hd {B = B} (var v) = B
+hd        (t $S τ) = hd t 
+
+F0S' : (Γc : SCon)(B : TyS) → Set
+F0S' Γc U = F0c Γc
+F0S' Γc (T ⇒̂S B) = T → F0S' Γc B
+
+F0S'fun : ∀{Γc Γc'}(B : TyS)(f : F0c Γc → F0c Γc')
+          →  F0S' Γc B → F0S' Γc' B
+F0S'fun U        f γ = f γ
+F0S'fun (T ⇒̂S B) f γ = λ τ → F0S'fun B f (γ τ)
 
-F0t : ∀{Γc B} → Tm Γc B → F0c Γc
-F0t (var vvz)     = inr _
-F0t (var (vvs v)) = inl (F0t (var v))
-F0t (t $S τ)      = F0t t
+F0t : ∀{Γc B}(t : Tm Γc B) → F0S' Γc B
+F0t {B = U}      (var vvz) = inr _
+F0t {B = T ⇒̂S B} (var vvz) = λ τ → F0S'fun B (λ { (inl x) → inl x ;
+                                                  (inr x) → inr (τ , x) }) (F0t {B = B} (var vvz))
+F0t {Γc}{B}      (var (vvs x)) = F0S'fun B inl (F0t (var x))
+F0t              (t $S τ)      = F0t t τ
 
-F0P : ∀{υc}(α : υc)(B : TyS) → _ᵃP {zero} (CodS B) (_ , υc)
-F0P α U        = α
-F0P α (T ⇒̂S B) = λ _ → F0P α B
+F0P : ∀{Ωc B}(t : Tm Ωc B) → (CodS B ᵃP) (_ , F0c Ωc)
+F0P {B = U} t = F0t t
+F0P {B = T ⇒̂S B} t = λ τ → F0P {B = B} (t $S τ)
 
-F0C' : ∀{Ωc Γc : SCon}(σ : Sub Ωc Γc) → _ᵃC {zero} (CodC Γc) (_ , F0c Ωc)
-F0C'               ε       = _
-F0C' {Ωc}{Γc ▶c B} (σ , t) = F0C' σ , F0P (F0t t) B
+F0C' : ∀{Ωc Γc}(σ : Sub Ωc Γc) → _ᵃC {zero} (CodC Γc) (_ , F0c Ωc)
+F0C' ε       = _
+F0C' (σ , t) = F0C' σ , F0P t
 
 F0C : ∀{Γc} → _ᵃC {zero} (CodC Γc) (_ , F0c Γc)
 F0C {Γc} = F0C' {Γc} IF.id
 
+F1S : ∀{B}(α : _ᵃS {zero} B) → Set
+F1S {U}      α = α
+F1S {T ⇒̂S B} α = F1S {B} (α {!!})
+
+F1c : ∀{Γc}(γc : _ᵃc {zero} Γc) → F0c Γc → Set
+F1c {∙c}      γc       _        = ⊤
+F1c {Γc ▶c B} (γc , α) (inl υc) = F1c {Γc} γc υc
+F1c {Γc ▶c B} (γc , α) (inr _)  = F1S {B} α
+
+module F1 {Γc : SCon}{γc : _ᵃc {zero} Γc} where
+  open El {Γc}{F0c Γc}(F0C {Γc})
+
+  F1C : (Γ : Con Γc) → _ᵃC {zero} (ElC Γ) (_ , F1c γc)
+  F1C Γ = {!!}
+
 -- Functor from Szumified algebras to original algebras
 GS : ∀ B {υc}(α : _ᵃP {zero} (CodS B) (_ , υc)) → _ᵃS {zero} B
 GS U α = {!!}