From f252e7753887e9d7db5bf9c50cb763ef6ed6d71e Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 26 Jan 2024 15:13:54 +0000
Subject: Redefine `Nil` in terms of `(^)`.

This makes some later inference work better.
---
 src/SOAS.idr | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/SOAS.idr')

diff --git a/src/SOAS.idr b/src/SOAS.idr
index 714ce15..befd53c 100644
--- a/src/SOAS.idr
+++ b/src/SOAS.idr
@@ -111,10 +111,6 @@ extend x {ctx2, ty} u theta =
 (src -<> tgt) ty ctx = {0 ctx' : type.Ctx} -> src ty ctx' ->
   tgt ty (ctx ++ ctx')
 
-0
-Nil : type.SortedFamily -> type.SortedFamily
-Nil f ty ctx = {0 ctx' : type.Ctx} -> ctx ~> ctx' -> f ty ctx'
-
 -- TODO: (Setoid) coalgebras
 
 0
@@ -122,6 +118,10 @@ Nil f ty ctx = {0 ctx' : type.Ctx} -> ctx ~> ctx' -> f ty ctx'
 (tgt ^ src) ty ctx =
   {0 ctx' : type.Ctx} -> src.subst ctx ctx' -> tgt ty ctx'
 
+0
+Nil : type.SortedFamily -> type.SortedFamily
+Nil f = f ^ Var
+
 hideCtx : {0 a : type.Ctx -> Type} ->
   ((0 ctx : type.Ctx) -> a ctx) -> {ctx : type.Ctx} -> a ctx
 hideCtx f {ctx} = f ctx
-- 
cgit v1.2.3