{"entities":{"Q7361308":{"pageid":31519463,"ns":120,"title":"Item:Q7361308","lastrevid":105364850,"modified":"2026-10-07T13:35:30Z","type":"item","id":"Q7361308","labels":{"en":{"language":"en","value":"Optics"}},"descriptions":{"en":{"language":"en","value":"AFP entry Optics"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5963c47c28e155056093315b2fed4afc6524fdac","datavalue":{"value":"https://isa-afp.org/entries/Optics.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361308$E6E72BBA-EAD8-4042-8319-2D4844E7D834","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e40ae189651578b8a662e35a038ee090babfc731","datavalue":{"value":{"time":"+2017-05-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361308$8B9CEDBA-F0A8-4EC7-B056-C9075C17B368","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"c9ddb9cb8edac3e4e3079ad62f4b03206fa5cc4b","datavalue":{"value":"Simon Foster","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361308$5312B361-2AA8-417E-839A-5692D1AE7FFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"d7df1d06e1120896265efed2652366fc829fb7c1","datavalue":{"value":"Christian Pardillo-Laursen","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361308$0700F709-4FD2-4C6E-95B0-63CC76F5E2D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2c5b18ebe11027a9cddf39baebf8dac2c938457c","datavalue":{"value":"Frank Zeyda","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361308$5BCF4FC8-46DE-4185-A564-3E211D967FFA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5991f949ee4a8de8d7f2c39cc568c8ce06e00d98","datavalue":{"value":{"text":"Optics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361308$377EEA7F-059E-417A-A128-D4E3DE33A409","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"eb750ce134382c907f9029c5beadc97087387f59","datavalue":{"value":"Lenses provide an abstract interface for manipulating data types through spatially-separated views. They are defined abstractly in terms of two functions, get , the return a value from the source type, and put that updates the value. We mechanise the underlying theory of lenses, in terms of an algebraic hierarchy of lenses, including well-behaved and very well-behaved lenses, each lens class being characterised by a set of lens laws. We also mechanise a lens algebra in Isabelle that enables their composition and comparison, so as to allow construction of complex lenses. This is accompanied by a large library of algebraic laws. Moreover we also show how the lens classes can be applied by instantiating them with a number of Isabelle data types.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361308$F5CC5C19-6F1C-44D6-A188-8F4DD18B7D2C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"13b2e611a60bbb1cbb1ab23d8301e40dbbe2b3c5","datavalue":{"value":{"entity-type":"item","numeric-id":2915136,"id":"Q2915136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$A8BF51D2-E2F6-47C3-9BC9-D3B42695C0AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cad5dbbae1e8a09daaaad27474e686d1687d9ae4","datavalue":{"value":{"entity-type":"item","numeric-id":5327345,"id":"Q5327345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$15E28C63-9BDE-4E3A-89EC-7AF6144939EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc62f32ebe5f2c566c09500f98ee202c262830a","datavalue":{"value":{"entity-type":"item","numeric-id":736461,"id":"Q736461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$727BFDB1-C09B-4760-848A-4297ECC73A80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79e807f14dcd5f9ad4f6bbeb1f8ea3c4bbb7d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":4396958,"id":"Q4396958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$6E760E2A-47C1-416C-BAE1-847D6000A58B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad5469f72b3d14e0a040a00af8c98b8e5cf4cb2b","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$D3605D17-6ABE-45A3-9881-06BDF69F6184","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42767904ec698e77bf5ad5a5ca09192ebfa305eb","datavalue":{"value":{"entity-type":"item","numeric-id":2941173,"id":"Q2941173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$583D2B79-10BF-4926-A88B-8125133D7716","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42e8700434177609e5f649d1f5a0b31b34ec0771","datavalue":{"value":{"entity-type":"item","numeric-id":3055747,"id":"Q3055747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$B39136AD-F82C-4005-A61B-421AF6EC7DBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"142462e18f1e15f78032d67efb1ec41dac2aece4","datavalue":{"value":{"entity-type":"item","numeric-id":2941176,"id":"Q2941176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$FDB67D05-6B69-465B-9126-A3D8AC110E28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca23da055412797c29f8737a832166566f69c4c4","datavalue":{"value":{"entity-type":"item","numeric-id":3007567,"id":"Q3007567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$28315A07-FD4E-40B8-8E38-0B70FDD083A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ea00f9571a2f3eb35a08ae82329dd711da0dc8b","datavalue":{"value":{"entity-type":"item","numeric-id":2814613,"id":"Q2814613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$DFB8E4AA-45F4-4FF2-AC8A-080D78321D59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5981e1168811f3b1a276d506216532fa05a55595","datavalue":{"value":{"entity-type":"item","numeric-id":3179407,"id":"Q3179407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$3E17A3BE-A402-4A1A-9872-55C0069B3996","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3587daf8b7bb37c28a02a6be9585e6348d1d132","datavalue":{"value":{"entity-type":"item","numeric-id":2971175,"id":"Q2971175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$2E59ECF1-9BF8-4E4E-9642-4FF1C99C67D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e27ad4b2994da46e11c5d31647a6af63a7a804b","datavalue":{"value":{"entity-type":"item","numeric-id":4282663,"id":"Q4282663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$97503E4B-06AC-42FB-899D-E03A807226BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6b0f593aaa3110f1e8f538d98538d65a9ad442a","datavalue":{"value":{"entity-type":"item","numeric-id":3777424,"id":"Q3777424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$96E23D1A-81D9-4D3E-97D1-E4A6FBBD8FCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a51285ecc98c7aa36e85f90f6de1b67d1e1af30","datavalue":{"value":{"entity-type":"item","numeric-id":3766810,"id":"Q3766810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$DF2B7FEF-328F-4825-AF71-25EE309616FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b87b4ed7731028b5ed63e9b6b85380602669d8ad","datavalue":{"value":{"entity-type":"item","numeric-id":5408557,"id":"Q5408557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$D8CC885E-D804-4716-8201-EF4EFC8C9FED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$EC44337F-5278-44C6-B93C-2891AA7790C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$D21F0BF9-14E4-4598-9062-3293E70C7AC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"263b81d6f82aa7bc5c419ca585e86c9e4182e475","datavalue":{"value":{"entity-type":"item","numeric-id":1019016,"id":"Q1019016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$4A78AEC7-94EC-42E9-B004-59BC25640FCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"deb9865b9ec7d75ea6408f7463449ba93e2c161e","datavalue":{"value":{"entity-type":"item","numeric-id":5307478,"id":"Q5307478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$48316C88-5367-4DF3-B0DC-3E0E5CD09823","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4cdd6bade1c3454eda14333c0a2ad28ec83785b4","datavalue":{"value":{"entity-type":"item","numeric-id":5781189,"id":"Q5781189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$F2E393E5-DF43-4FD9-8393-C2C86664466E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6b47545d737298ec8ec51129f8941307ae65dd1","datavalue":{"value":{"entity-type":"item","numeric-id":5616133,"id":"Q5616133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$436EFE6A-2C77-407D-91F0-0EDD038D5F4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23a4f79d5a209fbc2d0b0773de40c58b9c966c61","datavalue":{"value":{"entity-type":"item","numeric-id":2971180,"id":"Q2971180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$4455579F-26FB-499A-AD7A-650565E1FC3C","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$2716E09D-1275-453D-B587-513C200D98B6","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"eff161b7dcf55a20ec4d840b7f18d4148cc115e3","datavalue":{"value":{"entity-type":"item","numeric-id":7360789,"id":"Q7360789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$4AEBEE72-C31F-44AB-8E7B-F0DA8C3F6E9E","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361308$919D4F36-11A4-4446-B8F1-CE6B8425E537","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Optics (AFP entry Optics)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Optics_(AFP_entry_Optics)"}}}}}