From 39284b8d99812c42f242b7762aa7e5cc918fb58e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 14:13:55 +0100
Subject: [PATCH] Changes in CwF

---
 src/Cat/CwF.agda | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/Cat/CwF.agda b/src/Cat/CwF.agda
index 5735ac3..3954ea5 100644
--- a/src/Cat/CwF.agda
+++ b/src/Cat/CwF.agda
@@ -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