From a582f2555b7762cf0a6114dc08192697d3bfe5d7 Mon Sep 17 00:00:00 2001 From: Ambrus Kaposi Date: Tue, 1 Aug 2023 14:19:28 +0200 Subject: [PATCH] naming --- FFOL.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FFOL.lagda b/FFOL.lagda index 2058d2d..59a2a7a 100644 --- a/FFOL.lagda +++ b/FFOL.lagda @@ -16,7 +16,7 @@ module FFOL where infixr 5 _⊢_ field - -- We first make the base category with its final object + -- We first make the base category with its terminal object Con : Set ℓ¹ Sub : Con → Con → Set ℓ⁵ -- It makes a category _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ