Skip to content

Commit

Permalink
add topological to list of imports in Cubical.HITs.Nullification
Browse files Browse the repository at this point in the history
  • Loading branch information
@awswan
awswan committed May 12, 2024
1 parent 16b6861 commit cc2ea4c
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions Cubical/HITs/Nullification.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,3 +4,5 @@ module Cubical.HITs.Nullification where
open import Cubical.HITs.Nullification.Base public

open import Cubical.HITs.Nullification.Properties public

open import Cubical.HITs.Nullification.Topological public

0 comments on commit cc2ea4c

Please sign in to comment.