Skip to content

Commit a997e60

Browse files
tomdjongtomdjong
authored
Unused imports (#317)
* Remove unused imports in NotionsOfDecidability/ * Remove unused imports in Naturals/ * Remove unused imports in Modal/ * Remove unused imports in MLTT/ * Remove unused imports in MetricSpaces/ * Remove unused imports in Locales/
1 parent 3422eed commit a997e60

File tree

89 files changed

+11
-428
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

89 files changed

+11
-428
lines changed

‎source/Locales/AdjointFunctorTheoremForFrames.lagda

-2
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Originally part of `ayberkt/formal-topology-in-UF`. Ported to TypeTopology on
1212
{-# OPTIONS --safe --without-K #-}
1313

1414
open import MLTT.Spartan
15-
open import UF.Base
1615
open import UF.FunExt
1716
open import UF.PropTrunc
1817

@@ -27,7 +26,6 @@ open import Locales.Frame pt fe
2726
open import Locales.GaloisConnection pt fe
2827
open import Slice.Family
2928
open import UF.Logic
30-
open import UF.Subsingletons
3129

3230
open AllCombinators pt fe
3331
open PropositionalTruncation pt

‎source/Locales/Adjunctions/Properties-DistributiveLattice.lagda

-2
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ frames.
1414
{-# OPTIONS --safe --without-K #-}
1515

1616
open import MLTT.Spartan
17-
open import UF.Base
1817
open import UF.FunExt
1918
open import UF.PropTrunc
2019

@@ -24,7 +23,6 @@ module Locales.Adjunctions.Properties-DistributiveLattice
2423
where
2524

2625
open import Locales.Adjunctions.Properties pt fe
27-
open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe
2826
open import Locales.DistributiveLattice.Definition fe pt
2927
open import Locales.Frame pt fe
3028
open import Locales.GaloisConnection pt fe

‎source/Locales/Adjunctions/Properties.lagda

-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ to apply them to distributive lattices, generalizing them has become necessary.
2020
{-# OPTIONS --safe --without-K #-}
2121

2222
open import MLTT.Spartan
23-
open import UF.Base
2423
open import UF.FunExt
2524
open import UF.PropTrunc
2625

‎source/Locales/CharacterisationOfContinuity.lagda

-3
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,6 @@ Ayberk Tosun, 11 September 2023
44

55
{-# OPTIONS --safe --without-K #-}
66

7-
open import UF.Base
8-
open import UF.Subsingletons
97
open import UF.PropTrunc
108
open import UF.FunExt
119
open import MLTT.Spartan
@@ -15,7 +13,6 @@ module Locales.CharacterisationOfContinuity (pt : propositional-truncations-exis
1513
(fe : Fun-Ext) where
1614

1715
open import Locales.Frame pt fe
18-
open import Locales.WayBelowRelation.Definition pt fe
1916
open import UF.Logic
2017
open import Slice.Family
2118
open import Locales.Compactness pt fe

‎source/Locales/ClassificationOfScottOpens.lagda

-3
Original file line numberDiff line numberDiff line change
@@ -22,19 +22,16 @@ open Implication fe
2222
open Existential pt
2323
open Conjunction
2424

25-
open import Locales.Frame pt fe
2625
open import DomainTheory.Basics.Dcpo pt fe 𝓤 renaming (⟨_⟩ to ⟨_⟩∙)
2726
open import DomainTheory.Topology.ScottTopology pt fe 𝓤
2827
open import DomainTheory.Basics.Pointed pt fe 𝓤
2928
open import DomainTheory.Lifting.LiftingSet pt fe
3029
open import DomainTheory.Basics.Miscelanea pt fe 𝓤
3130
open import Lifting.Construction 𝓤
32-
open import UF.PropTrunc
3331
open import UF.SubtypeClassifier
3432
open import UF.Subsingletons-Properties
3533
open import Slice.Family
3634
open import UF.Equiv
37-
open import UF.HLevels
3835
open PropositionalTruncation pt
3936

4037
\end{code}

‎source/Locales/Clopen.lagda

-6
Original file line numberDiff line numberDiff line change
@@ -7,17 +7,13 @@ Ayberk Tosun, 11 September 2023
77
open import MLTT.Spartan hiding (𝟚)
88
open import UF.PropTrunc
99
open import UF.FunExt
10-
open import UF.UA-FunExt
1110
open import UF.Size
1211

1312
module Locales.Clopen (pt : propositional-truncations-exist)
1413
(fe : Fun-Ext)
1514
(sr : Set-Replacement pt) where
1615

17-
open import Locales.AdjointFunctorTheoremForFrames
1816
open import Locales.Frame pt fe
19-
open import Locales.WayBelowRelation.Definition pt fe
20-
open import Locales.Compactness pt fe
2117
open import Locales.Complements pt fe
2218
open import Locales.WellInside pt fe sr
2319
open import Slice.Family
@@ -30,9 +26,7 @@ open import UF.Base using (from-Σ-＝)
3026
open AllCombinators pt fe
3127
open PropositionalTruncation pt
3228

33-
open import Locales.GaloisConnection pt fe
3429

35-
open import Locales.InitialFrame pt fe
3630

3731
open Locale
3832

‎source/Locales/CompactRegular.lagda

-2
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,6 @@ open import MLTT.Spartan hiding (𝟚)
1111
open import UF.Base
1212
open import UF.FunExt
1313
open import UF.PropTrunc
14-
open import UF.UA-FunExt
15-
open import UF.Univalence
1614

1715
module Locales.CompactRegular
1816
(pt : propositional-truncations-exist)

‎source/Locales/Compactness.lagda

-2
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,9 @@ will be broken down into smaller modules.
1212

1313
{-# OPTIONS --safe --without-K #-}
1414

15-
open import UF.Base
1615
open import UF.Sets
1716
open import UF.Subsingletons
1817
open import UF.Subsingletons-Properties
19-
open import UF.Subsingletons-FunExt
2018
open import UF.PropTrunc
2119
open import UF.FunExt
2220
open import MLTT.Spartan

‎source/Locales/Complements.lagda

-8
Original file line numberDiff line numberDiff line change
@@ -7,21 +7,13 @@ Ayberk Tosun, 11 September 2023
77
open import MLTT.Spartan hiding (𝟚)
88
open import UF.FunExt
99
open import UF.PropTrunc
10-
open import UF.UA-FunExt
1110

1211
module Locales.Complements (pt : propositional-truncations-exist)
1312
(fe : Fun-Ext) where
1413

15-
open import Locales.AdjointFunctorTheoremForFrames
16-
open import Locales.Compactness pt fe
1714
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
1815
open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe
1916
open import Locales.Frame pt fe
20-
open import Locales.GaloisConnection pt fe
21-
open import Locales.InitialFrame pt fe
22-
open import Locales.WayBelowRelation.Definition pt fe
23-
open import Slice.Family
24-
open import UF.Base using (from-Σ-＝)
2517
open import UF.Logic
2618
open import UF.SubtypeClassifier
2719

‎source/Locales/ContinuousMap/Definition.lagda

-7
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,8 @@ Factored out from the `Locales.Frame` module into this module on 2024-04-10.
1313
{-# OPTIONS --safe --without-K #-}
1414

1515
open import MLTT.Spartan hiding (𝟚; ₀; ₁)
16-
open import UF.Base
1716
open import UF.FunExt
1817
open import UF.PropTrunc
19-
open import MLTT.List hiding ([_])
2018

2119
module Locales.ContinuousMap.Definition
2220
(pt : propositional-truncations-exist)
@@ -26,12 +24,7 @@ module Locales.ContinuousMap.Definition
2624
open import Locales.Frame pt fe
2725
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
2826
open import Slice.Family
29-
open import UF.Equiv
30-
open import UF.Hedberg
3127
open import UF.Logic
32-
open import UF.Sets
33-
open import UF.Subsingletons
34-
open import UF.Subsingletons-FunExt
3528
open import UF.SubtypeClassifier
3629

3730
open AllCombinators pt fe

‎source/Locales/ContinuousMap/FrameHomomorphism-Definition.lagda

-5
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,8 @@ Factored out from the `Locales.Frame` module into this module on 2024-04-10.
1515
{-# OPTIONS --safe --without-K #-}
1616

1717
open import MLTT.Spartan hiding (𝟚; ₀; ₁)
18-
open import UF.Base
1918
open import UF.FunExt
2019
open import UF.PropTrunc
21-
open import MLTT.List hiding ([_])
2220

2321
module Locales.ContinuousMap.FrameHomomorphism-Definition
2422
(pt : propositional-truncations-exist)
@@ -28,11 +26,8 @@ module Locales.ContinuousMap.FrameHomomorphism-Definition
2826
open import Locales.Frame pt fe
2927
open import Slice.Family
3028
open import UF.Equiv
31-
open import UF.Hedberg
3229
open import UF.Logic
3330
open import UF.Sets
34-
open import UF.Subsingletons
35-
open import UF.Subsingletons-FunExt
3631
open import UF.SubtypeClassifier
3732

3833
open AllCombinators pt fe

‎source/Locales/ContinuousMap/FrameHomomorphism-Properties.lagda

-4
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ Factored out from the `Locales.Frame` module on 2024-04-10.
1313

1414
{-# OPTIONS --safe --without-K #-}
1515

16-
open import MLTT.List hiding ([_])
1716
open import MLTT.Spartan hiding (𝟚; ₀; ₁)
1817
open import UF.Base
1918
open import UF.FunExt
@@ -27,11 +26,8 @@ module Locales.ContinuousMap.FrameHomomorphism-Properties
2726
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
2827
open import Locales.Frame pt fe
2928
open import Slice.Family
30-
open import UF.Hedberg
3129
open import UF.Logic
32-
open import UF.Sets
3330
open import UF.Subsingletons
34-
open import UF.Subsingletons-FunExt
3531
open import UF.SubtypeClassifier
3632

3733
open AllCombinators pt fe

‎source/Locales/ContinuousMap/FrameIsomorphism-Definition.lagda

-2
Original file line numberDiff line numberDiff line change
@@ -24,12 +24,10 @@ module Locales.ContinuousMap.FrameIsomorphism-Definition
2424
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
2525
open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe
2626
open import Locales.Frame pt fe
27-
open import Slice.Family
2827
open import UF.Equiv
2928
open import UF.Equiv-FunExt
3029
open import UF.Logic
3130
open import UF.Retracts
32-
open import UF.SIP
3331
open import UF.Subsingletons
3432
open import UF.Subsingletons-FunExt
3533
open import UF.SubtypeClassifier

‎source/Locales/ContinuousMap/Homeomorphism-Definition.lagda

-9
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ their defining frames, however, we give a different name to this notion.
1414
{-# OPTIONS --safe --without-K #-}
1515

1616
open import MLTT.Spartan hiding (𝟚; ₀; ₁)
17-
open import UF.Base
1817
open import UF.FunExt
1918
open import UF.PropTrunc
2019

@@ -23,17 +22,9 @@ module Locales.ContinuousMap.Homeomorphism-Definition
2322
(fe : Fun-Ext)
2423
where
2524

26-
open import Locales.ContinuousMap.Definition pt fe
2725
open import Locales.ContinuousMap.FrameIsomorphism-Definition pt fe
2826
open import Locales.Frame pt fe
29-
open import Slice.Family
30-
open import UF.Equiv
31-
open import UF.Hedberg
3227
open import UF.Logic
33-
open import UF.Sets
34-
open import UF.Subsingletons
35-
open import UF.Subsingletons-FunExt
36-
open import UF.SubtypeClassifier
3728

3829
open AllCombinators pt fe
3930
open Locale

‎source/Locales/ContinuousMap/Homeomorphism-Properties.lagda

-8
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Some properties of locale homeomorphisms.
1111
{-# OPTIONS --safe --without-K #-}
1212

1313
open import MLTT.Spartan hiding (𝟚; ₀; ₁)
14-
open import UF.Base
1514
open import UF.FunExt
1615
open import UF.PropTrunc
1716
open import UF.Size
@@ -32,18 +31,11 @@ private
3231
pe : Prop-Ext
3332
pe {𝓤} = univalence-gives-propext (ua 𝓤)
3433

35-
open import Locales.ContinuousMap.Definition pt fe
3634
open import Locales.ContinuousMap.FrameIsomorphism-Definition pt fe
3735
open import Locales.ContinuousMap.Homeomorphism-Definition pt fe
3836
open import Locales.Frame pt fe
3937
open import Locales.SIP.FrameSIP ua pt sr
40-
open import Slice.Family
41-
open import UF.Equiv
42-
open import UF.Hedberg
4338
open import UF.Logic
44-
open import UF.Sets
45-
open import UF.Subsingletons
46-
open import UF.Subsingletons-FunExt
4739
open import UF.SubtypeClassifier
4840

4941
open AllCombinators pt fe

‎source/Locales/ContinuousMap/Properties.lagda

-10
Original file line numberDiff line numberDiff line change
@@ -11,28 +11,18 @@ Factored out from the `Locales.Frame` module on 2024-04-10.
1111
{-# OPTIONS --safe --without-K #-}
1212

1313
open import MLTT.Spartan hiding (𝟚; ₀; ₁)
14-
open import UF.Base
1514
open import UF.FunExt
1615
open import UF.PropTrunc
17-
open import MLTT.List hiding ([_])
1816

1917
module Locales.ContinuousMap.Properties
2018
(pt : propositional-truncations-exist)
2119
(fe : Fun-Ext)
2220
where
2321

2422
open import Locales.Frame pt fe
25-
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
2623
open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe
2724
open import Locales.ContinuousMap.Definition pt fe
28-
open import Slice.Family
29-
open import UF.Equiv
30-
open import UF.Hedberg
3125
open import UF.Logic
32-
open import UF.Sets
33-
open import UF.Subsingletons
34-
open import UF.Subsingletons-FunExt
35-
open import UF.SubtypeClassifier
3626

3727
open AllCombinators pt fe
3828
open ContinuousMaps

‎source/Locales/DirectedFamily-Poset.lagda

-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ module Locales.DirectedFamily-Poset (pt : propositional-truncations-exist)
2424
open import Locales.Frame pt fe hiding (is-directed)
2525
open import MLTT.Spartan
2626
open import UF.Logic
27-
open import UF.Subsingletons
2827

2928
open AllCombinators pt fe
3029
open PropositionalTruncation pt

‎source/Locales/DirectedFamily.lagda

-3
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ and constructions that involve only the order of a given frame.
1616
open import MLTT.Spartan
1717
open import UF.FunExt
1818
open import UF.PropTrunc
19-
open import UF.Subsingletons
2019
open import UF.SubtypeClassifier
2120

2221
module Locales.DirectedFamily
@@ -26,9 +25,7 @@ module Locales.DirectedFamily
2625
(_≤_ : X → X → Ω 𝓥)
2726
where
2827

29-
open import Locales.Frame pt fe hiding (is-directed)
3028
open import Slice.Family
31-
open import UF.Equiv
3229
open import UF.Logic
3330

3431
open AllCombinators pt fe

‎source/Locales/DiscreteLocale/Definition.lagda

-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ module Locales.DiscreteLocale.Definition
2222
(pt : propositional-truncations-exist)
2323
where
2424

25-
open import Locales.DistributiveLattice.Definition fe pt
2625
open import Locales.Frame pt fe
2726
open import MLTT.Spartan
2827
open import Slice.Family

‎source/Locales/DiscreteLocale/Two-Properties.lagda

-10
Original file line numberDiff line numberDiff line change
@@ -25,22 +25,12 @@ module Locales.DiscreteLocale.Two-Properties
2525
where
2626

2727

28-
open import Locales.DiscreteLocale.Definition fe pe pt
2928
open import Locales.DiscreteLocale.Two fe pe pt
30-
open import Locales.DistributiveLattice.Definition fe pt
3129
open import Locales.Frame pt fe
32-
open import Locales.SmallBasis pt fe sr
33-
open import Locales.Spectrality.SpectralLocale pt fe
34-
open import Locales.Spectrality.SpectralMap pt fe
35-
open import Locales.Sierpinski 𝓤 pe pt fe
36-
open import Locales.Stone pt fe sr
37-
-- open import Locales.PatchProperties pt fe sr
3830
open import Locales.Compactness pt fe
3931
open import Slice.Family
40-
open import UF.DiscreteAndSeparated hiding (𝟚-is-set)
4132
open import UF.Logic
4233
open import UF.Powerset
43-
open import UF.Sets
4434
open import UF.SubtypeClassifier
4535

4636
open AllCombinators pt fe renaming (_∧_ to _∧ₚ_; _∨_ to _∨ₚ_)

‎source/Locales/DiscreteLocale/Two.lagda

-3
Original file line numberDiff line numberDiff line change
@@ -21,16 +21,13 @@ module Locales.DiscreteLocale.Two
2121
(pt : propositional-truncations-exist)
2222
where
2323

24-
open import Locales.DistributiveLattice.Definition fe pt
2524
open import Locales.DiscreteLocale.Definition fe pe pt
2625
open import Locales.Frame pt fe
2726
open import MLTT.Spartan hiding (𝟚)
28-
open import Slice.Family
2927
open import UF.Logic
3028
open import UF.Sets
3129
open import UF.DiscreteAndSeparated hiding (𝟚-is-set)
3230
open import UF.Powerset
33-
open import UF.SubtypeClassifier
3431

3532
open AllCombinators pt fe renaming (_∧_ to _∧ₚ_; _∨_ to _∨ₚ_)
3633
open PropositionalSubsetInclusionNotation fe

‎source/Locales/DistributiveLattice/Definition-SigmaBased.lagda

-4
Original file line numberDiff line numberDiff line change
@@ -20,15 +20,11 @@ module Locales.DistributiveLattice.Definition-SigmaBased
2020
where
2121

2222
open import Locales.DistributiveLattice.Definition fe pt
23-
open import Locales.Frame pt fe
2423
open import MLTT.Spartan
25-
open import UF.Base
2624
open import UF.Equiv
2725
open import UF.Logic
28-
open import UF.Powerset-MultiUniverse
2926
open import UF.Sets-Properties
3027
open import UF.Subsingletons
31-
open import UF.Subsingletons-FunExt
3228
open import UF.Subsingletons-Properties
3329
open import UF.SubtypeClassifier
3430

0 commit comments

Comments
 (0)