Logic.Grothendieck

Description

Synopsis

• data G_basic_spec = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_basic_spec lid basic_spec
• data G_sign = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_sign {
  • gSignLogic :: lid
  • gSign :: ExtSign sign symbol
  • gSignSelfIdx :: SigId
  }
• newtype SigId = SigId Int
• startSigId :: SigId
• isHomSubGsign :: G_sign -> G_sign -> Bool
• isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
• logicOfGsign :: G_sign -> AnyLogic
• symsOfGsign :: G_sign -> Set G_symbol
• data G_symbolmap a = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symbolmap lid (Map symbol a)
• data G_mapofsymbol a = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_mapofsymbol lid (Map a symbol)
• data G_symbol = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symbol lid symbol
• data G_symb_items_list = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symb_items_list lid [symb_items]
• data G_symb_map_items_list = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symb_map_items_list lid [symb_map_items]
• data G_sublogics = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_sublogics lid sublogics
• isSublogic :: G_sublogics -> G_sublogics -> Bool
• isProperSublogic :: G_sublogics -> G_sublogics -> Bool
• joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
• data G_morphism = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_morphism {
  • gMorphismLogic :: lid
  • gMorphism :: morphism
  • gMorphismSelfIdx :: MorId
  }
• newtype MorId = MorId Int
• startMorId :: MorId
• mkG_morphism :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> morphism -> G_morphism
• lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
• data LogicGraph = LogicGraph {
  • logics :: Map String AnyLogic
  • currentLogic :: String
  • currentSyntax :: Maybe IRI
  • currentSublogic :: Maybe G_sublogics
  • currentTargetBase :: Maybe (LibName, String)
  • sublogicBasedTheories :: Map AnyLogic SublogicBasedTheories
  • comorphisms :: Map String AnyComorphism
  • inclusions :: Map (String, String) AnyComorphism
  • unions :: Map (String, String) (AnyComorphism, AnyComorphism)
  • morphisms :: Map String AnyMorphism
  • modifications :: Map String AnyModification
  • squares :: Map (AnyComorphism, AnyComorphism) [Square]
  • qTATranslations :: Map String AnyComorphism
  • prefixes :: Map String IRI
  }
• setCurLogic :: String -> LogicGraph -> LogicGraph
• setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph
• setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph
• emptyLogicGraph :: LogicGraph
• lookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic
• lookupCurrentLogic :: Monad m => String -> LogicGraph -> m AnyLogic
• lookupCurrentSyntax :: Monad m => String -> LogicGraph -> m (AnyLogic, Maybe IRI)
• lookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism
• lookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism
• lookupModification :: Monad m => String -> LogicGraph -> m AnyModification
• data GMorphism = forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 . Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => GMorphism {
  • gMorphismComor :: cid
  • gMorphismSign :: ExtSign sign1 symbol1
  • gMorphismSignIdx :: SigId
  • gMorphismMor :: morphism2
  • gMorphismMorIdx :: MorId
  }
• isHomogeneous :: GMorphism -> Bool
• data Grothendieck = Grothendieck
• gEmbed :: G_morphism -> GMorphism
• gEmbed2 :: G_sign -> G_morphism -> GMorphism
• gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
• homGsigDiff :: G_sign -> G_sign -> Result G_sign
• gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
• gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
• homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
• logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
• logicUnion :: LogicGraph -> AnyLogic -> AnyLogic -> Result (AnyComorphism, AnyComorphism)
• updateMorIndex :: MorId -> GMorphism -> GMorphism
• toG_morphism :: GMorphism -> G_morphism
• gSigCoerce :: LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
• ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
• compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
• findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
• logicGraph2Graph :: LogicGraph -> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
• findComorphism :: Monad m => G_sublogics -> [AnyComorphism] -> m AnyComorphism
• isTransportable :: GMorphism -> Bool
• data Square = Square {
  • leftTriangle :: LaxTriangle
  • rightTriangle :: LaxTriangle
  }
• data LaxTriangle = LaxTriangle {
  • laxModif :: AnyModification
  • laxFst :: AnyComorphism
  • laxSnd :: AnyComorphism
  • laxTarget :: AnyComorphism
  }
• mkIdSquare :: AnyLogic -> Square
• mkDefSquare :: AnyComorphism -> Square
• mirrorSquare :: Square -> Square
• lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]

Documentation