From 56dbf845817c995fc100463f39f00641e3599ad3 Mon Sep 17 00:00:00 2001
From: Rahul Chhabra <rahul29112002@gmail.com>
Date: Wed, 15 May 2024 17:23:19 +0530
Subject: [PATCH] Remove files not caught in gitignore

---
 src/Realizability/PERs/#TerminalObject.agda# | 43 --------------------
 src/Realizability/PERs/.#TerminalObject.agda |  1 -
 2 files changed, 44 deletions(-)
 delete mode 100644 src/Realizability/PERs/#TerminalObject.agda#
 delete mode 120000 src/Realizability/PERs/.#TerminalObject.agda

diff --git a/src/Realizability/PERs/#TerminalObject.agda# b/src/Realizability/PERs/#TerminalObject.agda#
deleted file mode 100644
index b573343..0000000
--- a/src/Realizability/PERs/#TerminalObject.agda#
+++ /dev/null
@@ -1,43 +0,0 @@
-open import Realizability.ApplicativeStructure
-open import Realizability.CombinatoryAlgebra
-open import Realizability.PropResizing
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Structure using (⟨_⟩; str)
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Univalence
-open import Cubical.Foundations.Powerset
-open import Cubical.Functions.FunExtEquiv
-open import Cubical.Relation.Binary
-open import Cubical.Data.Sigma
-open import Cubical.Data.FinData
-open import Cubical.Data.Unit
-open import Cubical.Reflection.RecordEquiv
-open import Cubical.HITs.PropositionalTruncation as PT hiding (map)
-open import Cubical.HITs.PropositionalTruncation.Monad
-open import Cubical.HITs.SetQuotients as SQ
-open import Cubical.Categories.Category
-open import Cubical.Categories.Limits.Terminal
-
-module Realizability.PERs.TerminalObject 
-  {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
-
-open import Realizability.PERs.PER ca
-open CombinatoryAlgebra ca
-open Combinators ca renaming (i to Id; ia≡a to Ida≡a)
-open PERMorphism
-
-terminalPER : PER
-PER.relation terminalPER = (λ x y → Unit*) , λ x y → isPropUnit*
-fst (PER.isPER terminalPER) = λ a b x → tt*
-snd (PER.isPER terminalPER) = λ a b c x x₁ → tt*
-
-isTerminalTerminalPER : isTerminal PERCat terminalPER
-isTerminalTerminalPER X =
-  inhProp→isContr
-    (makePERMorphism (λ x → [ k ]) (return (Id , (λ a aXa → (eq/ k (Id ⨾ a) tt*) , tt*))))
-    λ x y → PERMorphism≡ x y (funExt λ q → {!effectiveOnDomain!})
-
-terminal : Terminal PERCat
-terminal = terminalPER , {!!}
diff --git a/src/Realizability/PERs/.#TerminalObject.agda b/src/Realizability/PERs/.#TerminalObject.agda
deleted file mode 120000
index 53126fa..0000000
--- a/src/Realizability/PERs/.#TerminalObject.agda
+++ /dev/null
@@ -1 +0,0 @@
-rahul@Rahuls-MacBook-Air.local.1114:1710392191
\ No newline at end of file