fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Changes in CwF

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 14:13:55 +01:00
parent 5796b791b8
commit 39284b8d99
1 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/Cat/CwF.agda
View file

@ -28,21 +28,21 @@ module _ {ℓa ℓb : Level} where
private
module T = Functor T
Type : (Γ : Object ℂ) → Set ℓa
Type Γ = proj₁ (T.func* Γ)
Type Γ = proj₁ (proj₁ (T.func* Γ))
module _ {Γ : Object ℂ} {A : Type Γ} where
module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
k : Σ (proj₁ (func* T B) → proj₁ (func* T A))
(λ f →
{x : proj₁ (func* T B)} →
proj₂ (func* T B) x → proj₂ (func* T A) (f x))
k = T.func→ γ
k₁ : proj₁ (func* T B) → proj₁ (func* T A)
k₁ = proj₁ k
k₂ : ({x : proj₁ (func* T B)} →
proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
k₂ = proj₂ k
-- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
-- k : Σ (proj₁ (func* T B) → proj₁ (func* T A))
-- (λ f →
-- {x : proj₁ (func* T B)} →
-- proj₂ (func* T B) x → proj₂ (func* T A) (f x))
-- k = T.func→ γ
-- k₁ : proj₁ (func* T B) → proj₁ (func* T A)
-- k₁ = proj₁ k
-- k₂ : ({x : proj₁ (func* T B)} →
-- proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
-- k₂ = proj₂ k
record ContextComprehension : Set (ℓa ⊔ ℓb) where
field