···

       
4
       
 
       


     

       
5
       
 
       
import Foundation

     

       
6
       
 
       


     

       
7
       
-
       
/// Pterodactyl has two sizes of small things: little and moderate. Beyond these, we have things that are not types but rather “type schemes”.

     

       
8
       
 
       
public enum Size<Universe> {

     

       
9
       
-
       
	/// A “little” thing is something classified by a universe. Universes form a countable hierarchy.

     

       
10
       
 
       
	case little(universe: Universe)

     

       
11
       
 
       
	

     

       
12
       
-
       
	/// A “moderate” type is something classified by `Type`.

     

       
13
       
-
       
	case moderate

     

       
14
       
 
       
}

     

       
15
       
 
       


     

       
16
       
 
       


     
···

       
20
       
 
       
	public static func == (lhs: Size<Universe>, rhs: Size<Universe>) -> Bool {

     

       
21
       
 
       
		switch (lhs, rhs) {

     

       
22
       
 
       
		case (.little, .little): true

     

       
23
       
-
       
		case (.moderate, .moderate): true

     

       
24
       
 
       
		default: false

     

       
25
       
 
       
		}

     

       
26
       
 
       
	}

     
···

       
30
       
 
       
	func map<U>(_ f: (Universe) -> U) -> Size<U> {

     

       
31
       
 
       
		switch self {

     

       
32
       
 
       
		case let .little(universe: universe): .little(universe: f(universe))

     

       
33
       
-
       
		case .moderate: .moderate

     

       
34
       
 
       
		}

     

       
35
       
 
       
	}

     

       
36
       
 
       
}

     

···

       
4
       
 
       


     

       
5
       
 
       
import Foundation

     

       
6
       
 
       


     

       
7
       
+
       
/// Pterodactyl has two sizes of small things: ``little(universe:)`` and ``big``. Beyond these, we have things that are not types but rather “type schemes”.

     

       
8
       
 
       
public enum Size<Universe> {

     

       
9
       
+
       
	/// A “little” type is something classified by a universe. Universes form a countable hierarchy.

     

       
10
       
 
       
	case little(universe: Universe)

     

       
11
       
 
       
	

     

       
12
       
+
       
	/// A “big” type is something classified by `Type`.

     

       
13
       
+
       
	case big

     

       
14
       
 
       
}

     

       
15
       
 
       


     

       
16
       
 
       


     
···

       
20
       
 
       
	public static func == (lhs: Size<Universe>, rhs: Size<Universe>) -> Bool {

     

       
21
       
 
       
		switch (lhs, rhs) {

     

       
22
       
 
       
		case (.little, .little): true

     

       
23
       
+
       
		case (.big, .big): true

     

       
24
       
 
       
		default: false

     

       
25
       
 
       
		}

     

       
26
       
 
       
	}

     
···

       
30
       
 
       
	func map<U>(_ f: (Universe) -> U) -> Size<U> {

     

       
31
       
 
       
		switch self {

     

       
32
       
 
       
		case let .little(universe: universe): .little(universe: f(universe))

     

       
33
       
+
       
		case .big: .big

     

       
34
       
 
       
		}

     

       
35
       
 
       
	}

     

       
36
       
 
       
}

     

···

       
11
       
 
       
		switch await type.whnf() {

     

       
12
       
 
       


     

       
13
       
 
       
		// In principle the type of universes could be small, but I am worried about about the strictness of the semilattice operations. I know how to interpret them if universeType is exoNat as in 2LTT, but in that case universeType probably should not be fibrant.

     

       
14
       
-
       
		case .universeType, .universeCodes(size: .moderate):

     

       
15
       
 
       
			throw SizeError()

     

       
16
       
 
       


     

       
17
       
 
       
		case let .universeCodes(size: .little(universe: littleUniverse)):

     
···

       
48
       
 
       


     

       
49
       
 
       
	func assertLeq(size1: Size<Value>, size2: Size<Value>) async throws {

     

       
50
       
 
       
		switch (size1, size2) {

     

       
51
       
-
       
		case (_, .moderate): ()

     

       
52
       
 
       
		case let (.little(universe: universe1), .little(universe: universe2)):

     

       
53
       
 
       
			try await assertLeq(universe1: universe1, universe2: universe2)

     

       
54
       
 
       
		default:

     

···

       
11
       
 
       
		switch await type.whnf() {

     

       
12
       
 
       


     

       
13
       
 
       
		// In principle the type of universes could be small, but I am worried about about the strictness of the semilattice operations. I know how to interpret them if universeType is exoNat as in 2LTT, but in that case universeType probably should not be fibrant.

     

       
14
       
+
       
		case .universeType, .universeCodes(size: .big):

     

       
15
       
 
       
			throw SizeError()

     

       
16
       
 
       


     

       
17
       
 
       
		case let .universeCodes(size: .little(universe: littleUniverse)):

     
···

       
48
       
 
       


     

       
49
       
 
       
	func assertLeq(size1: Size<Value>, size2: Size<Value>) async throws {

     

       
50
       
 
       
		switch (size1, size2) {

     

       
51
       
+
       
		case (_, .big): ()

     

       
52
       
 
       
		case let (.little(universe: universe1), .little(universe: universe2)):

     

       
53
       
 
       
			try await assertLeq(universe1: universe1, universe2: universe2)

     

       
54
       
 
       
		default:

     

···

       
10
       
 
       
		let analysis = LocalAnalysis()

     

       
11
       
 
       
		

     

       
12
       
 
       
		await #expect(throws: Never.self) {

     

       
13
       
-
       
			try await analysis.assertLeq(size1: .moderate, size2: .moderate)

     

       
14
       
 
       
		}

     

       
15
       
 
       
	}

     

       
16
       
 
       
	

     
···

       
18
       
 
       
		let analysis = LocalAnalysis()

     

       
19
       
 
       
		

     

       
20
       
 
       
		await #expect(throws: LocalAnalysis.SizeError.self) {

     

       
21
       
-
       
			try await analysis.assertLeq(size1: .moderate, size2: .little(universe: .universeZero))

     

       
22
       
 
       
		}

     

       
23
       
 
       
	}

     

       
24
       
 
       
	

     

···

       
10
       
 
       
		let analysis = LocalAnalysis()

     

       
11
       
 
       
		

     

       
12
       
 
       
		await #expect(throws: Never.self) {

     

       
13
       
+
       
			try await analysis.assertLeq(size1: .big, size2: .big)

     

       
14
       
 
       
		}

     

       
15
       
 
       
	}

     

       
16
       
 
       
	

     
···

       
18
       
 
       
		let analysis = LocalAnalysis()

     

       
19
       
 
       
		

     

       
20
       
 
       
		await #expect(throws: LocalAnalysis.SizeError.self) {

     

       
21
       
+
       
			try await analysis.assertLeq(size1: .big, size2: .little(universe: .universeZero))

     

       
22
       
 
       
		}

     

       
23
       
 
       
	}

     

       
24